**1.**Introduction**1.1.**Well-Typed Programs Do Go Wrong**1.2.**Refinement Types**1.3.**Audience**1.4.**Getting Started**1.5.**Sample Code**2.**Logic & SMT**2.1.**Syntax**2.2.**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**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**3.8.**Putting It All Together**3.9.**Recap**4.**Polymorphism**4.1.**Specification: Vector Bounds**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**4.6.**Recap**5.**Refined Datatypes**6.**Boolean Measures**7.**Numeric Measures**7.1.**Wholemeal Programming**7.2.**Specifying List Dimensions**7.3.**Lists: Size Preserving API**7.4.**Lists: Size Reducing API**7.5.**Dimension Safe Vector API**7.6.**Dimension Safe Matrix API**7.7.**Recap**8.**Elemental Measures**8.1.**Talking about Sets**8.2.**Proving QuickCheck Style Properties**8.3.**Content-Aware List API**8.4.**Permutations**8.5.**Uniqueness**8.6.**Unique Zippers**8.7.**Recap**9.**Case Study: Okasaki's Lazy Queues**10.**Case Study: Associative Maps**10.1.**Specifying Maps**10.2.**Using Maps: Well Scoped Expressions**10.3.**Implementing Maps: Binary Search Trees**10.4.**Recap**11.**Case Study: Pointers & Bytes**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.**Recap: Types Against Overflows**12.**Case Study: AVL Trees

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
module Intro where
import Prelude hiding (abs)
divide :: Int -> Int -> Int
zero'''' :: Int
die :: String -> a

**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 = one'
where
{-@ one' :: Zero @-}
one' = 1 :: Int

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

**Subtyping and Implication** `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 contradition, LiquidHaskell deduces that the first equation is *dead code* and hence `die`

will not be called at run-time.

**Establishing Pre-conditions** 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.↩