One of the great things about Haskell is its brainy type system that
allows one to enforce a variety of invariants at compile time, thereby
nipping a large swathe of run-time errors in the bud. Refinement types
allow us to use modern logic solvers (*aka* SAT and SMT engines) to
dramatically extend the scope of invariants that can be statically
verified.

## What is a Refinement Type?

In a nutshell,

Refinement Types = Types + Logical Predicates

That is, refinement types allow us to decorate types with
*logical predicates* (think *boolean-valued* Haskell expressions)
which constrain the set of values described by the type, and hence
allow us to specify sophisticated invariants of the underlying values.

Say what?

(Btw, *click the title* to demo LiquidHaskell on the code in this article)

42: module Intro where 43: 44: import Language.Haskell.Liquid.Prelude (liquidAssert)

Let us jump right in with a simple example, the number `0 :: Int`

.
As far as Haskell is concerned, the number is simply an `Int`

(lets not
worry about things like `Num`

for the moment). So are `2`

, `7`

, and
`904`

. With refinements we can dress up these values so that they
stand apart. For example, consider the binder

54: zero' :: Int 55: {VV : (GHC.Types.Int) | (0 <= VV)}zero' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0

We can ascribe to the variable `zero'`

the refinement type

61: {-@ zero' :: {v: Int | 0 <= v} @-}

which is simply the basic type `Int`

dressed up with a predicate.
The binder `v`

is called the *value variable*, and so the above denotes
the set of `Int`

values which are greater than `0`

. Of course, we can
attach other predicates to the above value, for example

**Note:** We will use `@`

-marked comments to write refinement type
annotations the Haskell source file, making these types, quite literally,
machine-checked comments!

75: {-@ zero'' :: {v: Int | (0 <= v && v < 100) } @-} 76: zero'' :: Int 77: {VV : (GHC.Types.Int) | (VV < 100),(0 <= VV)}zero'' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0

which states that the number is in the range `0`

to `100`

, or

83: {-@ zero''' :: {v: Int | ((v mod 2) = 0) } @-} 84: zero''' :: Int 85: {VV : (GHC.Types.Int) | ((VV mod 2) = 0)}zero''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0

where `mod`

is the *modulus* operator in the refinement logic. Thus, the type
above states that zero is an *even* number.

We can also use a singleton type that precisely describes the constant

94: {-@ zero'''' :: {v: Int | v = 0 } @-} 95: zero'''' :: Int 96: {VV : (GHC.Types.Int) | (VV = 0)}zero'''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0

(Aside: we use a different names `zero'`

, `zero''`

etc. for a silly technical
reason – LiquidHaskell requires that we ascribe a single refinement type to
a top-level name.)

Finally, we could write a single type that captures all the properties above:

106: {-@ zero :: {v: Int | ((0 <= v) && ((v mod 2) = 0) && (v < 100)) } @-} 107: zero :: Int 108: {VV : (GHC.Types.Int) | ((VV mod 2) = 0),(VV < 100),(0 <= VV)}zero = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0

The key points are:

- A refinement type is just a type
*decorated*with logical predicates. - A value can have
*different*refinement types that describe different properties. - If we
*erase*the green bits (i.e. the logical predicates) we get back*exactly*the usual Haskell types that we know and love. - A vanilla Haskell type, say
`Int`

has the trivial refinement`true`

i.e. is really`{v: Int | true}`

.

We have built a refinement type-based verifier called LiquidHaskell. Lets see how we can use refinement types to specify and verify interesting program invariants in LiquidHaskell.

## Writing Safety Specifications

We can use refinement types to write various kinds of more interesting safety specifications.

First, we can write a wrapper around the usual `error`

function

133: {-@ error' :: {v: String | false } -> a @-} 134: error' :: String -> a 135: {VV : [(GHC.Types.Char)] | false} -> aerror' = [(GHC.Types.Char)] -> aerror

The interesting thing about the type signature for `error'`

is that the
input type has the refinement `false`

. That is, the function must only be
called with `String`

s that satisfy the predicate `false`

. Of course, there
are *no* such values. Thus, a program containing the above function
typechecks *exactly* when LiquidHaskell can prove that the function
`error'`

is *never called*.

Next, we can use refinements to encode arbitrary programmer-specified
**assertions** by defining a function

149: {-@ lAssert :: {v:Bool | (Prop v)} -> a -> a @-} 150: lAssert :: Bool -> a -> a 151: {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> a -> alAssert True ax = {VV : a | (VV = x)}x 152: lAssert False _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"lAssert failure"

In the refinement, `(Prop v)`

denotes the Haskell `Bool`

value `v`

interpreted as a logical predicate. In other words, the input type for
this function specifies that the function must *only* be called with
the value `True`

.

## Refining Function Types : Preconditions

Lets use the above to write a *divide* function that *only accepts* non-zero
denominators.

168: divide :: Int -> Int -> Int 169: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)divide (GHC.Types.Int)n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero" 170: divide n d = {VV : (GHC.Types.Int) | (VV = n)}n x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | (VV != 0)}d

We can specify that the non-zero denominator *precondition* with a suitable
refinement on the *input* component of the function’s type

177: {-@ divide :: Int -> {v: Int | v != 0 } -> Int @-}

How *does* LiquidHaskell verify the above function?

The key step is that LiquidHaskell deduces that the expression
`"divide by zero"`

is not merely of type `String`

, but in fact
has the the refined type `{v:String | false}`

*in the context*
in which the call to `error'`

occurs.

LiquidHaskell arrives at this conclusion by using the fact that
in the first equation for `divide`

the *denominator* parameter
is in fact `0 :: {v: Int | v = 0}`

which *contradicts* the
precondition (i.e. input) type.

In other words, LiquidHaskell deduces by contradiction, that
the first equation is **dead code** and hence `error'`

will
not be called at run-time.

If you are paranoid, you can put in an explicit assertion

199: divide' :: Int -> Int -> Int 200: {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}divide' {VV : (GHC.Types.Int) | false}n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero" 201: divide' n d = {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}lAssert ({VV : (GHC.Types.Int) | false}d x:{VV : (GHC.Types.Int) | false} -> y:{VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0 : int))}0) ({VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}) -> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}$ {VV : (GHC.Types.Int) | false}n x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | false}d

and LiquidHaskell will verify the assertion (by verifying the call to
`lAssert`

) for you.

## Refining Function Types : Postconditions

Next, lets see how we can use refinements to describe the *outputs* of a
function. Consider the following simple *absolute value* function

214: abz :: Int -> Int 215: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz (GHC.Types.Int)n | {VV : (GHC.Types.Int) | (VV = (0 : int))}0 x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV = n)}n = {VV : (GHC.Types.Int) | (VV = n)}n 216: | otherwise = {VV : (GHC.Types.Int) | (VV = (0 : int))}0 x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}- {VV : (GHC.Types.Int) | (VV = n)}n

We can use a refinement on the output type to specify that the function returns non-negative values

223: {-@ abz :: Int -> {v: Int | 0 <= v } @-}

LiquidHaskell *verifies* that `abz`

indeed enjoys the above type by
deducing that `n`

is trivially non-negative when `0 < n`

and that in
the `otherwise`

case, i.e. when `not (0 < n)`

the value `0 - n`

is
indeed non-negative (lets not worry about underflows for the moment.)
LiquidHaskell is able to automatically make these arithmetic deductions
by using an SMT solver which has decision
built-in procedures for arithmetic, to reason about the logical
refinements.

## Putting It All Together

Lets wrap up this introduction with a simple `truncate`

function
that connects all the dots.

244: {-@ truncate :: Int -> Int -> Int @-} 245: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate (GHC.Types.Int)i (GHC.Types.Int)max 246: | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i 247: | otherwise = {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i') 248: where {VV : (GHC.Types.Int) | (0 <= VV)}i' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i 249: {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

`truncate i n`

simply returns `i`

if its absolute value is less the
upper bound `max`

, and otherwise *truncates* the value at the maximum.
LiquidHaskell verifies that the use of `divide`

is safe by inferring that
at the call site

`i' > max'`

from the branch condition.`0 <= i'`

from the`abz`

postcondition (hover mouse over`i'`

).`0 <= max'`

from the`abz`

postcondition (hover mouse over`max'`

).

From the above, LiquidHaskell infers that `i' != 0`

. That is, at the
call site `i' :: {v: Int | v != 0}`

, thereby satisfying the
precondition for `divide`

and verifying that the program has no pesky
divide-by-zero errors. Again, if you *really* want to make sure, put
in an assertion

268: {-@ truncate' :: Int -> Int -> Int @-} 269: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate' (GHC.Types.Int)i (GHC.Types.Int)max 270: | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i 271: | otherwise = {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> (GHC.Types.Int) -> (GHC.Types.Int)lAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0), (VV >= zero''''), (0 <= VV), (VV <= i')} -> y:{VV : (GHC.Types.Int) | (VV >= 0), (VV >= zero''''), (0 <= VV), (VV <= i')} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0 : int))}0) ((GHC.Types.Int) -> (GHC.Types.Int)) -> (GHC.Types.Int) -> (GHC.Types.Int)$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i') 272: where {VV : (GHC.Types.Int) | (0 <= VV)}i' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i 273: {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

and *lo!* LiquidHaskell will verify it for you.

## Modular Verification

Incidentally, note the `import`

statement at the top. Rather than rolling
our own `lAssert`

we can import and use a pre-defined version `liquidAssert`

defined in an external module

286: {-@ truncate'' :: Int -> Int -> Int @-} 287: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate'' (GHC.Types.Int)i (GHC.Types.Int)max 288: | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i 289: | otherwise = {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> (GHC.Types.Int) -> (GHC.Types.Int)liquidAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0), (VV >= zero''''), (0 <= VV), (VV <= i')} -> y:{VV : (GHC.Types.Int) | (VV >= 0), (VV >= zero''''), (0 <= VV), (VV <= i')} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0 : int))}0) ((GHC.Types.Int) -> (GHC.Types.Int)) -> (GHC.Types.Int) -> (GHC.Types.Int)$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i') 290: where {VV : (GHC.Types.Int) | (0 <= VV)}i' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i 291: {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

In fact, LiquidHaskell comes equipped with suitable refinements for standard functions and it is easy to add refinements as we shall demonstrate in subsequent articles.

## Conclusion

This concludes our quick introduction to Refinement Types and LiquidHaskell. Hopefully you have some sense of how to

**Specify**fine-grained properties of values by decorating their types with logical predicates.**Encode**assertions, preconditions, and postconditions with suitable function types.**Verify**semantic properties of code by using automatic logic engines (SMT solvers) to track and establish the key relationships between program values.