**1.**Introduction**1.1.**What is Liquid Haskell?**1.2.**More precise types**1.3.**An extension of Haskell**1.4.**Refinement types**1.5.**Type synonyms**1.6.**Refinement types must refine**1.7.**One expression, many types**1.8.**Refinement types and functions**1.9.**Preconditions vs. postconditions**1.10.**Integer arithmetic**1.11.**Exercises**2.**Lists**2.1.**Goal**2.2.**Our own list type**2.3.**Termination**2.4.**Measures**2.5.**Mapping**2.6.**Interleaving two lists**2.7.**Disabling termination checking**2.8.**Totality**2.9.**Impossible cases**2.10.**Exercises**2.11.**Taking elements out of a list**2.12.**Dropping elements from a list**2.13.**Computing s sublist**2.14.**Replicating an element**2.15.**Computing a range of numbers**2.16.**Safe indexing**2.17.**Bonus exercises**2.18.**Finding equal elements**2.19.**Grouping elements**2.20.**Run-length encoding**3.**Sets**3.1.**Uninterpreted functions**3.2.**Using an uninterpreted function**3.3.**Sets**3.4.**Lookup tables**3.5.**Another measure on maps**3.6.**A safe lookup function**3.7.**Removing bindings**4.**Proofs**4.1.**Tables again**4.2.**Reflecting functions**4.3.**Proving a simple property**4.4.**And a slightly more complicated one ...**4.5.**A property on lists**5.**Conclusions

{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--prune-unsorted" @-}
module Lists where
import Prelude hiding (length, take, map, repeat, replicate, head, drop, (!!))

In order to see some more interesting examples of refinements, let's look at a data structure we're all familiar with: lists.

Let's look at some typical functions on lists and see how their type can be improved.

Built-in lists and the functions on these already have a lot of predefined features in Liquid Haskell. To better understand how to define datatypes in Liquid Haskell and establish properties on them, let us work with our own lists:

data List a = Nil | Cons a (List a)
deriving (Show)
infixr 5 `Cons`

In principle, we can use these lists immediately in Liquid Haskell:

list1 :: List Int
list1 = 1 `Cons` 2 `Cons` 3 `Cons` Nil

And we can even use them with refinement types:

{-@ list2 :: List Nat @-}
list2 :: List Int
list2 = 1 `Cons` 2 `Cons` 3 `Cons` Nil -- ok
{-@ list3 :: List Nat @-}
list3 :: List Int
list3 = -1 `Cons` 2 `Cons` 3 `Cons` Nil -- not ok

However, if we try to define even a very simple recursive function over lists, we get an error:

{-@ length :: List a -> Nat @-}
length :: List a -> Int
length Nil = 0
length (x `Cons` xs) = 1 + length xs

Liquid Haskell tried to prove **termination** of all functions, but for user-defined datatypes, we have to teach it how to do this.

We can declare `length`

to be a **measure** by saying

-- {-@ measure length @-} -- uncomment this

and then declaring that `length`

is the **termination measure** to use for the `List`

type:

-- {-@ data List [length] @-} -- uncomment this

A measure is a single-argument function with one case per constructor. Measures are lifted into the types of the constructors of the function, and can then also be used in refinements.

```
Nil :: { ys : List a | length ys == 0 }
Cons :: a -> xs : List a -> { ys : List a | length ys == 1 + length xs }
```

With these declarations in place, `length`

now type- and termination-checks.

The following definition of `map`

now also termination-checks, because Liquid Haskell will assume that the function decreases the termination measure of its first "structured" argument:

map :: (a -> b) -> List a -> List b
map _ Nil = Nil
map f (x `Cons` xs) = f x `Cons` map f xs

Can you add a type signature that captures that `map`

does not change the length of the input list?

Termination is less obvious for `interleave`

:

interleave :: List a -> List a -> List a
interleave Nil ys = ys
interleave xs Nil = xs
interleave (x `Cons` xs) ys = x `Cons` interleave ys xs

In the recursive call, it is not clear that `ys`

is shorter than `x : xs`

.

In such a situation, we can specify a termination measure for a function ourselves:

-- {-@ interleave :: xs : List a -> ys : List a -> List a / [length xs + length ys] @-}

Can you further refine the type signature such that we track the length of the resulting list?

Termination checking can be disabled for a whole file using the `--no-termination`

option.

Termination checking can be disabled for an individual function by using the `lazy`

directive.

repeat :: a -> List a
repeat x = x `Cons` repeat x
{-@ lazy repeat @-}

Disabling termination checking can be a useful test, because quite often, termination errors are not easily recognisable as termination errors.

Liquid Haskell also checks totality, i.e., if a function covers all possible cases:

head :: List a -> a
head (Cons x xs) = x

Can you provide a refinement type such that this function passes the totality check?

The definition of `head`

above has the disadvantage that it still triggers a warning in Haskell.

We can fix this by defining:

{-@ impossible :: { s : String | False } -> a @-}
impossible :: String -> a
impossible msg = error msg

The precondition of `impossible`

is indeed impossible. So Liquid Haskell will verify that it cannot be called.

Fix this definition that now passes the totality check, but fails due to the Liquid Haskell type of `impossible`

:

tail :: List a -> List a
tail (Cons x xs) = xs
tail Nil = impossible "tail: Nil"

Why does the following definition of `take`

not typecheck? Can you fix it?

{-@ take :: i : Nat -> List a -> { ys : List a | length ys == i } @-}
take :: Int -> List a -> List a
take _ Nil = Nil
take 0 _ = Nil
take i (Cons x xs) =
x `Cons` take (i - 1) xs

Could you use `impossible`

in the definition of `take`

?

Also provide a proper refinement type for `drop`

:

drop :: Int -> List a -> List a
drop _ Nil = Nil
drop 0 xs = xs
drop i (Cons _ xs) =
drop (i - 1) xs

And now for `sublist`

:

sublist :: Int -> Int -> List a -> List a
sublist s l xs = take l (drop s xs)

Let's test that this works:

testSublist1 :: List Int
testSublist1 = sublist 1 2 (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` Nil) -- ok

testSublist2 :: List Int
testSublist2 = sublist 2 3 (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` Nil) -- should fail

Provide a suitable refinement type for `replicate`

:

replicate :: Int -> a -> List a
replicate i x
| i == 0 = Nil
| otherwise = x `Cons` replicate (i - 1) x

With your refined type, this should typecheck:

test1 :: Int
test1 = head (replicate 3 3)

And does this typecheck?

test2 :: List Int
test2 = take (head (replicate 3 3)) (1 `Cons` 2 `Cons` 3 `Cons` 4 `Cons` Nil)

The function `range`

is supposed to take a lower and an upper bound and produce an ascending list of all the numbers that are greater than or equal to the lower bound and stricly smaller than the upper bound.

Try first to find a termination measure for this function so that it termination-checks.

Then try if you can refine the type further.

range :: Int -> Int -> List Int
range i j
| i == j = Nil
| otherwise = i `Cons` range (i + 1) j

Implement a safe list indexing operation.

(!!) :: List a -> Int -> a
(!!) = undefined

This is a simplified version of `span`

:

span' :: Eq a => a -> List a -> (List a, List a)
span' w Nil = ( Nil, Nil)
span' w (x `Cons` xs)
| w == x = (x `Cons` ys, zs)
| otherwise = ( Nil, x `Cons` xs)
where
(ys, zs) = span' w xs

Can you find a better type?

{-@ group :: Eq a -> List a -> List (Group a) @-}
group :: Eq a => List a -> List (List a)
group Nil = Nil
group (x `Cons` xs) = (x `Cons` ys) `Cons` group zs
where
(ys, zs) = span' x xs

But of course, we also want to capture that each of the groups is non-empty, and made up of equal elements (hint: you can use `head`

in refinements).

{-@ type Group a = List a @-}

Ideally, the call to `head`

in the definition of `encode`

should be safe now:

encode :: Eq a => List a -> List (Int, a)
encode xs =
map
(\ ys -> (length ys, head ys))
(group xs)

Can you nevertheless refine the type signature further?