Since the inception of the Haskell language, the community around it has
steadily innovated with language extensions and abstractions. To mention
a few, we had the `IO`

monad, all flavors of type classes and constraints,
Template Haskell, generalized algebraic data types (GADTs), data kinds, etc.
Then we had to deal with the programs resulting from all this innovation,
which eventually sprang feelings that ranged from sticking to
Simple Haskell to supporting full motion towards
Dependent Haskell.

There seems to be two design goals at conflict in current discussions. On the one hand, we want our programs to be easy to maintain. For instance, changes to one part of the code shouldn’t propagate to many others, and the meaning of a piece of code should remain reasonably deducible from the text.

On the other hand, we want our programs to do what we mean, and we want assistance from the computer to help us achieve this goal. Our human brains can only deal with a limited amount of complexity, and industrial-scale software has largely exceeded our capacity in the last several decades. But can we prove the correctness of our programs with a type-system that doesn’t make them hard to read or change?

In this post, I’m arguing that Liquid Haskell offers an alternative angle to approach this question. Liquid Haskell is a tool that can analyse a program and calculate proof obligations that would ensure that the program meets some specification (not unlike Dafny, Why3, or F*). The specification is included in the program as a special comment inserted by the programmer. The compiler ignores this comment, but Liquid Haskell can find it. Once the proof obligations are identified, they are given to a theorem prover (an SMT solver specifically) in an attempt to save the programmer the trouble of writing a proof.

The conjecture that I pose is that many of the properties that would usually require dependent types to ensure at compile time, can be described in Liquid Haskell specifications. The point is not so much that proofs are easier with Liquid Haskell, but rather that we are in front of an approach that integrates well with a programming language as is, and yet it leverages the power of tools specialized to reason about logic when verifying programs.

## Verifying functions

Let us consider an indexing function for lists.

```
elemAt :: [a] -> Int -> a
elemAt (x : _) 0 = x
elemAt (_ : xs) i = elemAt xs (i-1)
```

This function can fail at runtime if the index is negative or greater or equal to the length of the list. If we wanted to do indexing safely, a formulation with dependent types could change the type of the function. The list type is replaced with the type of lists with a given length, and the integer type is replaced with the type of natural numbers smaller than the length.

```
elemAt1 :: Vec a n -> Fin n -> a
elemAt1 xs i = case (i, xs) of
(FZ, x :> _) -> x
(FS i, _ :> xs) -> elemAt1 xs i
-- Vec a n = lists of length n
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Zero
(:>) :: a -> Vec a n -> Vec a (Succ n)
-- Fin n = natural numbers smaller than n
data Fin :: Nat -> Type where
FZ :: Fin (Succ n)
FS :: Fin n -> Fin (Succ n)
data Nat = Zero | Succ Nat
```

We include the types of `Vec`

and `Fin`

to illustrate some of the
complexity that needs to be introduced to work with dependent types,
but we are not overly concerned with their details. A gentle
presentation of these and the following examples with dependent types
can be found in this tutorial.

The original function has been rewritten to be total. The types of the
arguments have been changed to exclude from the domain the invalid
indices. Being a total function, it can no longer fail at runtime.
Moreover, the new types force all invocations to provide a valid index.
In the transformation, though, we lost the original simplicity. The
list type is no longer the standard list type for which many functions
are offered in the standard libraries, and the efficient `Int`

type has
been replaced by a representation that counts sticks.
To avoid conversions between the standard types and the new `Vec`

and
`Fin`

types, we could be tempted to use these types in code that needs
list indexing, which then would make this change less local than we
could wish for.

With Liquid Haskell, instead, we could get our safety guarantees by writing a specification of the original function expressed with predicate logic. We use a refinement type on the index argument to state its validity.

```
-- specifications go between special comments `{-@ ... @-}`
{-@ elemAt :: xs:[a] -> { i:Int | 0 <= i && i < len xs } -> a @-}
elemAt :: [a] -> Int -> a
elemAt (x : _) 0 = x
elemAt (_ : xs) i = elemAt xs (i-1)
```

A refinement type denotes a subtype of another type,
characterized by a given predicate. In our example, `{ i:Int | 0 <= i && i < len xs }`

is a subtype of `Int`

, whose values `i`

satisfy the predicate
`0 <= i && i < len xs`

. The specifications allow us to name the arguments
of functions and to refer to them in the predicates, such as
the list argument named `xs`

.
The language used to describe a predicate is not Haskell, but a separate
language with functions and logical connectives. When predicates need to
refer to Haskell functions, the functions can be translated to the logic.

The function `elemAt`

continues to be partial in Haskell, but it
is total according to its specification. And Liquid Haskell is powerful
enough to check that `elemAt`

meets the
specification, i.e. given a valid index, the function won’t fail.
It is a choice of the user to use Liquid Haskell to ensure that the
invocations meet the specification as well, or to leave
the invocations unverified. The
solution not only leaves the original function untouched, which dependent
types could also achieve, but it is remarkably economical in the way of
expressing the property we care about.

## Beyond bounds checking

Bounds checking is useful enough, but given the ability of Liquid Haskell to translate pure Haskell functions into the logic, we can aspire to verify other kinds of properties too. The following example is a datatype that can be used to represent untyped lambda expressions. It has constructors for variables, lambda abstractions, and applications.

```
-- | Unchecked expression, indexed by a bound of the allowed free variables
data UExp (n :: Nat)
= UVar (Fin n) -- ^ de Bruijn index for a variable
| ULam (UExp (Succ n))
| UApp (UExp n) (UExp n)
deriving Show
```

Variables are represented with a de Bruijn index. That is, the variable
`UVar i`

refers to the variable bound by the i-th lambda abstraction surrounding
the variable occurrence. Thus, `ULam (ULam (UVar FZ))`

stands for the lambda expression
`\x . \y . y`

, and `ULam (ULam (UVar (FS FZ)))`

stands for `\x. \y. x`

.

The type index of `UExp`

allows us to refer conveniently to closed expressions as
`UExp Zero`

. In a closed expression, all variables have a matching lambda
abstraction. Thus, `ULam (UVar FZ) :: UExp Zero`

type checks, but
`UVar FZ :: UExp Zero`

wouldn’t typecheck
because there is no lambda abstraction to bind `UVar FZ`

and it has type
`forall n. UExp (Succ n)`

.

Besides the fact that we are still counting sticks to identify variables, the type index needs to be carried around everywhere we deal with these expressions regardless of the task at hand. The Liquid Haskell counterpart looks as follows.

```
{-@
data UExp
= UVar ({i:Int | 0 <= i}) // indices are specified to be non-negative
| ULam UExp
| UApp UExp UExp
@-}
data UExp
= UVar Int
| ULam UExp
| UApp UExp UExp
-- | Computes an upper bound of the variables that appear free
-- in an expression.
{-@ reflect freeVarBound @-}
{-@ freeVarBound :: UExp -> { i:Int | 0 <= i } @-}
freeVarBound :: UExp -> Int
freeVarBound (UVar v) = v + 1
freeVarBound (ULam body) = max 0 (freeVarBound body - 1)
freeVarBound (UApp e1 e2) = max (freeVarBound e1) (freeVarBound e2)
```

With these definitions we can mimic the original indexed type with the following type synonyms.

```
-- Type synonym parameters starting with an upper case letter stand
-- for variables that are substituted with term-level expressions
-- instead of types.
{-@ type UExpN N = { e:UExp | freeVarBound e <= N } @-}
{-@ type ClosedUExp = UExpN 0 @-}
```

One feature of the Liquid Haskell way is that we don’t need to use a type index in the Haskell datatypes. We are only concerned with the ability to express the type of closed expressions in specifications, not in the actual program.

Another feature is that we are using a simple Haskell function to
express what the bound of free variables is for a particular expression,
and then we are using this function in the logic to say that an
expression is closed. The `reflect`

keyword in the
specification of `freeVarBound`

is directing Liquid Haskell to translate
the function to the logic language.

Now we can test our type specifications with example expressions, and this is possible without a single GADT or a promoted data constructor.

```
{-@ e0 :: ClosedUExp @-}
e0 :: UExp
e0 = ULam (UVar 0)
{-@ e1 :: ClosedUExp @-} -- Fails verification
{-@ e1 :: UExpN 1 @-} -- Passes verification
e1 :: UExp
e1 = UVar 0
```

## Beyond closed expressions

As a final example, let us consider a juicier Haskell datatype to
represent typed lambda expressions. These expressions are functions
manipulating values of some opaque type `T`

.

```
-- | @Exp ctx ty@ is a well-typed expression of type @ty@ in context
-- @ctx@. Note that a context is a list of types, where a type's index
-- in the list indicates the de Bruijn index of the associated term-level
-- variable.
data Exp :: forall n. Vec Ty n -> Ty -> Type where
Var :: Elem ctx ty -> Exp ctx ty
Lam :: Exp (arg :> ctx) res -> Exp ctx (arg :-> res)
App :: Exp ctx (arg :-> res) -> Exp ctx arg -> Exp ctx res
-- | A type encoding types. @T@ is the atom while @:->@ refers to
-- the type arrow '->'.
data Ty = T | Ty :-> Ty
-- | @Elem xs x@ is evidence that @x@ is in the vector @xs@.
-- @EZ :: Elem xs x@ is evidence that @x@ is the first element of @xs@.
-- @ES ev :: Elem xs x@ is evidence that @x@ is one position later in
-- @xs@ than is indicated in @ev@
data Elem :: forall a n. Vec a n -> a -> Type where
EZ :: Elem (x :> xs) x
ES :: Elem xs x -> Elem (y :> xs)
```

The `Exp`

datatype still tracks whether variables are in scope, this time
with an `Elem`

type that stands for a proof that a variable is in the
typing context. Additionally, the datatype ensures that the expressions
are well typed.

In Liquid Haskell we start with untyped expressions as before, with the
novelty that the `ULam`

constructor now has an extra argument to
indicate the type of the binding. The extra argument is necessary to
implement a type inference function named `inferType`

.

```
data UExp
= UVar Int
| ULam Ty UExp
| UApp UExp UExp
deriving Show
{-@ reflect elemAt @-}
{-@ reflect inferType @-}
{-@ inferType :: ctx:[Ty] -> UExpN (len ctx) -> Maybe Ty @-}
inferType :: [Ty] -> UExp -> Maybe Ty
inferType ctx (UVar i) = Just (elemAt ctx i)
inferType ctx (ULam t body) =
case inferType (t : ctx) body of
Just r -> Just (t :-> r)
Nothing -> Nothing
inferType ctx (UApp e0 e1) =
case inferType ctx e0 of
Just (a :-> r) -> case inferType ctx e1 of
Just t -> if a == t then Just r else Nothing
Nothing -> Nothing
_ -> Nothing
```

Liquid Haskell verifies that the list indexing in the first equation of
`inferType`

is safe, thanks to the refinement type of the
expression that ensures that the index is within the bounds of the list.
The same refinement type ensures that we don’t forget to grow the context
when we infer the type for the body of a lambda expression. And we also
get the assurance that `inferType`

terminates on inputs that meet the
specification.
In order to express well-typed terms, we only need now a type synonym.

```
{-@ type WellTypedExp CTX TY = { e:UExp | freeVarBound e <= len CTX && inferType CTX e == Just TY } @-}
{-@ e2 :: WellTypedExp [T] T @-}
e2 :: UExp
e2 = UVar 0
{-@ e3 :: WellTypedExp [] (T :-> T) @-}
e3 :: UExp
e3 = ULam T (UVar 0)
```

The specification of well-typed terms borrows the function `inferType`

from Haskell, which has been translated to the logic. This allows to
reuse the understanding that the user has of `inferType`

to express
what being well-typed means. When verifying `e2`

and `e3`

, Liquid
Haskell relies on the the SMT solver and other reasoning mechanisms
of its own.

## Summing up

The examples in this post that use Liquid Haskell can be found here. If you would like to see more substantial use of Liquid Haskell, there are two implementations of an interpreter for lambda expressions that can be compared side by side. The first implementation relies on emulating dependent types in Haskell and was implemented by fellow Tweager Richard Eisenberg. The second implementation is my reimplementation of Richard’s using Liquid Haskell.

In this post I have presented some examples where Liquid Haskell is expressive enough to deal with properties that are typically associated with the need of a dependently-typed language. Yet, unlike dependent types, Liquid Haskell allows us to keep programs to verify unchanged from the perspective of the compiler, and the trouble of discharging proof obligations is addressed in cooperation with theorem provers.

The downside of this way is that we now have to deal with the complexities of the integration. We need to orchestrate the communication between the different tools, translate our programs into the logics of the theorem provers, and translate the errors back to terms that the user can relate to the program being verified. There are more opportunities to make mistakes in the seams between the tools, while dependently-typed languages are often built on a single compiler with a possibly smaller trusted core.

On the user side, though, we can turn Liquid Haskell into a philosophy for approaching verification. We are not necessarily doomed to build a behemoth language-implementation capable of verifying it all. Instead, we can separate our verification from our programming needs and tackle each group with dedicated tools in order to better reuse code and techniques on both fronts.