Sets

Liquid Haskell comes with a number of useful specifications for standard libraries. One such example is that it comes with specifications for Data.Set.

import qualified Data.Set as S

If you import a module and a .spec file exists, it is automatically brought into scope by Liquid Haskell. Such .spec files contain just Liquid Haskell directives, without any code.

Uninterpreted functions

Liquid Haskell allows us to give refined interfaces to trusted libraries without verifying them completely.

Here is an example:

{-@ measure checked :: [Int] -> Bool @-} {-@ assume check :: xs : [Int] -> { b : Bool | b <=> checked xs } @-} check :: [Int] -> Bool check xs = sum xs == 0

The function checked is an uninterpreted function. Such a function can be introduced using a measure directive with just a type signature, and no actual definition in the code.

We can still teach Liquid Haskell facts about the behaviour of such a function.

The assume directive assumes a type without verifying it. Here, we say if and only if check succeeds, it establishes the checked predicate for the checked list.

Using an uninterpreted function

We can go on to work with checked lists.

{-@ type CheckedList = { xs : [Int] | checked xs } @-} {-@ assume combine :: CheckedList -> CheckedList -> CheckedList @-} combine :: [Int] -> [Int] -> [Int] combine xs ys = xs ++ ys

And this is rejected:

test :: IO () test = do xs <- readLn ys <- readLn print $ combine xs ys

Can you fix it?

Sets

The specification for sets introduces a number of uninterpreted functions, equips the functions from the Data.Set library with refined types mentioning these functions, and then maps these functions to SMT solver primitives being able to reason about sets (ok, that makes them no longer entirely uninterpreted):

{-@ setTest :: { x : S.Set Int | S.member 2 x && not (S.member 4 x) } @-} setTest :: S.Set Int setTest = (set1 `S.union` set2) `S.difference` set3 where set1 = S.fromList [1,2,3] set2 = S.fromList [2,4,6] set3 = S.fromList [3,4,5]

We can use sets in refinements ...

Lookup tables

Let's consider a primitive lookup table:

data Table key val = Empty | Bind key val (Table key val)

As for lists, we start by defining a termination measure:

{-@ measure size @-} {-@ size :: Table key val -> Nat @-} size :: Table key val -> Int size Empty = 0 size (Bind _ _ t) = 1 + size t {-@ data Table [size] @-}

Another measure on maps

{-@ measure keys @-} keys :: Ord key => Table key val -> S.Set key keys Empty = S.empty keys (Bind k _ t) = S.union (S.singleton k) (keys t)

If we have multiple measures on a datatype (here Table), then the constructor types are refined by all of them, e.g.:

Empty :: { t : Table key val | size t == 0 && keys t == S.empty }

A safe lookup function

lookup :: Ord key => key -> Table key val -> val lookup _ Empty = impossible "lookup: Empty" lookup k (Bind k' v r) | k == k' = v | otherwise = lookup k r

Can you provide a type signature for lookup that makes it check?

Let's test:

lookupTest1 :: Int lookupTest1 = lookup "y" (Bind "x" 23 (Bind "y" 45 (Bind "z" 56 Empty))) -- ok lookupTest2 :: Int lookupTest2 = lookup "p" (Bind "x" 23 (Bind "y" 45 (Bind "z" 56 Empty))) -- should fail

Removing bindings

delete :: Ord key => key -> Table key val -> Table key val delete _ Empty = Empty delete k (Bind k' v r) | k == k' = delete k r | otherwise = Bind k' v (delete k r)

Can you provide a refined type signature for delete? Could / should we replace anything with impossible here?