**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 "--exact-data-cons" @-}
module Sets where
import Prelude hiding (lookup)
import Language.Haskell.Liquid.ProofCombinators

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.

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.

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?

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 ...

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

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

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

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

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?