**1.**Introduction {#intro}**1.1.**Well-Typed Programs Do Go Wrong {#gowrong}**1.2.**Refinement Types**1.3.**Audience**1.4.**Getting Started**2.**Logic & SMT**2.1.**Syntax**2.2.**Semantics {#semantics}**2.3.**Verification Conditions**2.4.**Examples: Propositions**2.5.**Examples: Arithmetic**2.6.**Examples: Uninterpreted Function**2.7.**Recap**3.**Refinement Types**3.1.**Defining Types {#definetype}**3.2.**Errors**3.3.**Subtyping**3.4.**Writing Specifications**3.5.**Refining Function Types: Pre-conditions**3.6.**Refining Function Types: Post-conditions**3.7.**Testing Values: Booleans and Propositions {#propositions}**3.8.**Putting It All Together**3.9.**Recap**4.**Polymorphism {#polymorphism}**4.1.**Specification: Vector Bounds {#vectorbounds}**4.2.**Verification: Vector Lookup**4.3.**Inference: Our First Recursive Function**4.4.**Higher-Order Functions: Bottling Recursion in a`loop`

**4.5.**Refinements and Polymorphism {#sparsetype}**4.6.**Recap**5.**Refined Datatypes {#refineddatatypes}**5.1.**Sparse Vectors Revisited {#autosmart}**5.2.**Ordered Lists {#orderedlists}**5.3.**Ordered Trees {#binarysearchtree}**5.4.**Recap**6.**Boolean Measures {#boolmeasures}**6.1.**Partial Functions**6.2.**Lifting Functions to Measures {#usingmeasures}**6.3.**A Safe List API**6.4.**Recap**7.**Numeric Measures {#numericmeasure}**7.1.**Wholemeal Programming**7.2.**Specifying List Dimensions**7.3.**Lists: Size Preserving API**7.4.**Lists: Size Reducing API {#listreducing}**7.5.**Dimension Safe Vector API**7.6.**Dimension Safe Matrix API**7.7.**Recap**8.**Elemental Measures {#setmeasure}**8.1.**Talking about Sets**8.2.**Proving QuickCheck Style Properties {#quickcheck}**8.3.**Content-Aware List API {#listelems}**8.4.**Permutations**8.5.**Uniqueness**8.6.**Unique Zippers**8.7.**Recap**9.**Case Study: Okasaki's Lazy Queues {#lazyqueue}**10.**Case Study: Associative Maps**10.1.**Specifying Maps {#mapapi}**10.2.**Using Maps: Well Scoped Expressions**10.3.**Implementing Maps: Binary Search Trees {#lemmas}**10.4.**Recap**11.**Case Study: Pointers & Bytes {#case-study-pointers}**11.1.**HeartBleeds in Haskell**11.2.**Low-level Pointer API**11.3.**A Refined Pointer API**11.4.**Assumptions vs Guarantees**11.5.**ByteString API**11.6.**Application API**11.7.**Nested ByteStrings**11.8.**Recap: Types Against Overflows**12.**Case Study: AVL Trees {#case-study-avltree}

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
module Tutorial_03_Basic where
import Prelude hiding (abs)
divide :: Int -> Int -> Int
die :: String -> a
-- {-@ fail nonsense @-}
-- {-@ fail canDie @-}
-- {-@ fail divide' @-}
-- {-@ fail avg @-}
-- {-@ ignore lAssert @-}

**What is a Refinement Type?** In a nutshell,

Refinement Types=Types+Predicates

That is, refinement types allow us to decorate types with
*logical predicates*, which you can think of as
*boolean-valued* Haskell expressions, that constrain the set of
values described by the type. This lets us specify sophisticated
invariants of the underlying values.

Let us define some refinement types:^{1}

{-@ type Zero = {v:Int | v == 0} @-}
{-@ type NonZero = {v:Int | v /= 0} @-}

**The Value Variable** `v`

denotes the set of
valid inhabitants of each refinement type. Hence, `Zero`

describes the *set of* `Int`

values that are equal to
`0`

, that is, the singleton set containing just
`0`

, and `NonZero`

describes the set of
`Int`

values that are *not* equal to `0`

,
that is, the set `{1, -1, 2, -2, ...}`

and so on. ^{2}

**To use** these types we can write:

{-@ zero :: Zero @-}
zero = 0 :: Int
{-@ one, two, three :: NonZero @-}
one = 1 :: Int
two = 2 :: Int
three = 3 :: Int

If we try to say nonsensical things like:

nonsense :: Int
nonsense = one'
where
{-@ one' :: Zero @-}
one' = 1

LiquidHaskell will complain with an error message:

```
../liquidhaskell-tutorial/src/03-basic.lhs:72:3-6: Error: Liquid Type Mismatch
72 | one' = 1 :: Int
^^^^
Inferred type
VV : {VV : Int | VV == (1 : int)}
not a subtype of Required type
VV : {VV : Int | VV == 0}
```

The message says that the expression `1 :: Int`

has the
type

`{v:Int | v == 1} `

which is *not* (a subtype of) the *required* type

`{v:Int | v == 0} `

as `1`

is not equal to `0`

.

What is this business of *subtyping*? Suppose we have some
more refinements of `Int`

{-@ type Nat = {v:Int | 0 <= v} @-}
{-@ type Even = {v:Int | v mod 2 == 0 } @-}
{-@ type Lt100 = {v:Int | v < 100} @-}

**What is the type of** `zero`

?
`Zero`

of course, but also `Nat`

:

{-@ zero' :: Nat @-}
zero' = zero

and also `Even`

:

{-@ zero'' :: Even @-}
zero'' = zero

and also any other satisfactory refinement, such as ^{3}

{-@ zero''' :: Lt100 @-}
zero''' = zero

`Zero`

is the most precise type for `0::Int`

,
as it is a *subtype* of `Nat`

, `Even`

and
`Lt100`

. This is because the set of values defined by
`Zero`

is a *subset* of the values defined by
`Nat`

, `Even`

and `Lt100`

, as the
following *logical implications* are valid:

- \(v = 0 \Rightarrow 0 \leq v\)
- \(v = 0 \Rightarrow v \ \mbox{mod}\ 2 = 0\)
- \(v = 0 \Rightarrow v < 100\)

**In Summary** the key points about refinement types
are:

- A refinement type is just a type
*decorated*with logical predicates. - A term can have
*different*refinements for different properties. - When we
*erase*the predicates we get the standard Haskell types.^{4}

Let’s write some more interesting specifications.

**Typing Dead Code** We can wrap the usual
`error`

function in a function `die`

with the
type:

{-@ die :: {v:String | false} -> a @-}
die msg = error msg

The interesting thing about `die`

is that the input type
has the refinement `false`

, meaning the function must only be
called with `String`

s that satisfy the predicate
`false`

. This seems bizarre; isn’t it *impossible* to
satisfy `false`

? Indeed! Thus, a program containing
`die`

typechecks *only* when LiquidHaskell can prove
that `die`

is *never called*. For example,
LiquidHaskell will *accept*

cannotDie = if 1 + 1 == 3
then die "horrible death"
else ()

by inferring that the branch condition is always `False`

and so `die`

cannot be called. However, LiquidHaskell will
*reject*

canDie = if 1 + 1 == 2
then die "horrible death"
else ()

as the branch may (will!) be `True`

and so
`die`

can be called.

Let’s use `die`

to write a *safe division* function
that *only accepts* non-zero denominators.

divide' :: Int -> Int -> Int
divide' n 0 = die "divide by zero"
divide' n d = n `div` d

From the above, it is clear to *us* that `div`

is
only called with non-zero divisors. However, LiquidHaskell reports an
error at the call to `"die"`

because, what if
`divide'`

is actually invoked with a `0`

divisor?

We can specify that will not happen, with a *pre-condition*
that says that the second argument is non-zero:

{-@ divide :: Int -> NonZero -> Int @-}
divide _ 0 = die "divide by zero"
divide n d = n `div` d

**To Verify** that `divide`

never calls
`die`

, LiquidHaskell infers that
`"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 `die`

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

the *denominator* is in
fact

`0 :: {v: Int | v == 0} `

which *contradicts* the pre-condition (i.e. input) type.
Thus, by contradiction, LiquidHaskell deduces that the first equation is
*dead code* and hence `die`

will not be called at
run-time.

The above signature forces us to ensure that that when we
*use* `divide`

, we only supply provably
`NonZero`

arguments. Hence, these two uses of
`divide`

are fine:

avg2 x y = divide (x + y) 2
avg3 x y z = divide (x + y + z) 3

**Exercise: (List Average): **Consider the function
`avg`

:

- Why does LiquidHaskell flag an error at
`n`

? - How can you change the code so LiquidHaskell verifies it?

avg :: [Int] -> Int
avg xs = divide total n
where
total = sum xs
n = length xs

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

abs :: Int -> Int
abs n
| 0 < n = n
| otherwise = 0 - n

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

{-@ abs :: Int -> Nat @-}

LiquidHaskell *verifies* that `abs`

indeed enjoys
the above type by deducing that `n`

is trivially non-negative
when `0 < n`

and that in the `otherwise`

case,
the value `0 - n`

is indeed non-negative. ^{5}

In the above example, we *compute* a value that is guaranteed
to be a `Nat`

. Sometimes, we need to *test* if a value
satisfies some property, e.g., is `NonZero`

. For example,
let’s write a command-line *calculator*:

calc = do putStrLn "Enter numerator"
n <- readLn
putStrLn "Enter denominator"
d <- readLn
putStrLn (result n d)
calc

which takes two numbers and divides them. The function
`result`

checks if `d`

is strictly positive (and
hence, non-zero), and does the division, or otherwise complains to the
user:

result n d
| isPositive d = "Result = " ++ show (n `divide` d)
| otherwise = "Humph, please enter positive denominator!"

Finally, `isPositive`

is a test that returns a
`True`

if its input is strictly greater than `0`

or `False`

otherwise:

isPositive :: Int -> Bool
isPositive x = x > 0

**To verify** the call to `divide`

inside
`result`

we need to tell LiquidHaskell that the division only
happens with a `NonZero`

value `d`

. However, the
non-zero-ness is established via the *test* that occurs inside
the guard `isPositive d`

. Hence, we require a
*post-condition* that states that `isPositive`

only
returns `True`

when the argument is positive:

{-@ isPositive :: x:Int -> {v:Bool | v <=> x > 0} @-}

In the above signature, the output type (post-condition) states that
`isPositive x`

returns `True`

if and only if
`x`

was in fact strictly greater than `0`

. In
other words, we can write post-conditions for plain-old
`Bool`

-valued *tests* to establish that user-supplied
values satisfy some desirable property (here, `Pos`

and hence
`NonZero`

) in order to then safely perform some computation
on it.

**Exercise: (Propositions): **What happens if you
*delete* the type for `isPositive`

? Can you
*change* the type for `isPositive`

(i.e. write some
other type) while preserving safety?

**Exercise: (Assertions): **Consider the following assert
function, and two use sites. Write a suitable refinement type signature
for `lAssert`

so that `lAssert`

and
`yes`

are accepted but `no`

is rejected.

{-@ lAssert :: Bool -> a -> a @-}
lAssert True x = x
lAssert False _ = die "yikes, assertion fails!"
yes = lAssert (1 + 1 == 2) ()
no = lAssert (1 + 1 == 3) ()

**Hint: **You need a pre-condition that
`lAssert`

is only called with `True`

.

Let’s wrap up this introduction with a simple `truncate`

function that connects all the dots.

truncate :: Int -> Int -> Int
truncate i max
| i' <= max' = i
| otherwise = max' * (i `divide` i')
where
i' = abs i
max' = abs max

The expression `truncate i n`

evaluates to `i`

when the absolute value of `i`

is less than the upper bound
`max`

, and otherwise *truncates* the value at the
maximum `n`

. LiquidHaskell verifies that the use of
`divide`

is safe by inferring that:

`max' < i'`

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

from the`abs`

post-condition, and`0 <= max'`

from the`abs`

post-condition.

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

. That
is, at the call site `i' :: NonZero`

, thereby satisfying the
pre-condition for `divide`

and verifying that the program has
no pesky divide-by-zero errors.

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, pre-conditions, and post-conditions 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.

You can read the type of

`Zero`

as: “`v`

is an`Int`

*such that*`v`

equals`0`

” and`NonZero`

as : “`v`

is an`Int`

*such that*`v`

does not equal`0`

”↩︎We will use

`@`

-marked comments to write refinement type annotations in the Haskell source file, making these types, quite literally, machine-checked comments!↩︎We use a different names

`zero'`

,`zero''`

etc. as (currently) LiquidHaskell supports*at most*one refinement type for each top-level name.↩︎Dually, a standard Haskell type has the trivial refinement

`true`

. For example,`Int`

is equivalent to`{v:Int|true}`

.↩︎LiquidHaskell is able to automatically make these arithmetic deductions by using an SMT solver which has built-in decision procedures for arithmetic, to reason about the logical refinements.↩︎