Lists

Goal

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.

Our own list type

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

Termination

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.

Measures

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.

Mapping

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?

Interleaving two lists

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?

Disabling termination checking

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.

Totality

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?

Impossible cases

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"

Exercises

Taking elements out of a list

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?

Dropping elements from a list

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

Computing s sublist

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

Replicating an element

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)

Computing a range of numbers

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

Safe indexing

Implement a safe list indexing operation.

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

Bonus exercises

Finding equal elements

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?

Grouping elements

{-@ 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 @-}

Run-length encoding

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?