CIS 552

Nick will give an interactive exercise on the LiquidHaskell tool.

To prepare, watch this video presented by Ranjit Jhala at the LambdaConf conference. In particular, pay close attention to the section from 15:00 to 46:00, which covers parts 2 and 3 of the presentation distributed here.

To run the code in this lecture, use the online LiquidHaskell demo using the hs version of this file.

> module LiquidHaskell where
> import Language.Haskell.Liquid.ProofCombinators

> main :: IO ()
> main = print "Remember, no class Wednesday! Happy thanksgiving!"

For each of the following problems, fill in the missing LiquidHaskell type with one strong enough to enforce the given specification. Make sure that LH accepts the function given the type you have chosen!

> -- (a)

> -- fact should return a value greater than or equal to both `1` and `n`
> 
> fact :: Int -> Int
> fact 0 = 1
> fact n = fact (n - 1) * n

> -- (b)

> -- `OrderedList a` represents an increasing list of elements of type `a`
> data OrderedList a =
>    Nil
>  | Cons { hd :: a, tl :: OrderedList a }

> {-@
> data OrderedList a =
>    Nil
> | Cons { hd :: a, tl :: <<FILL IN HERE>> }
> @-}

> insert :: (Ord a) => a -> OrderedList a -> OrderedList a
> insert x Nil = Cons x Nil
> insert x (Cons y ys)
>   | x <= y = Cons x (Cons y ys)
>   | otherwise = Cons y (insert x ys)

Proving Program Properties

Using LiquidHaskell, we can manually prove stronger properties than we've seen so far. We will show a couple short proofs of properties of the fib function below. To state these properties, we need to add ("reflect") the fib function to LH's logic, which allows us to use it inside of a LH refinement type.

> {-@ reflect fib @-}
> {-@ fib :: Nat -> Nat @-}
> fib :: Int -> Int
> fib n | n == 0    = 0
>       | n == 1    = 1
>       | otherwise = fib (n-1) + fib (n-2)

The type of fib2_1 states the property that fib 2 is equal to 1. Think of the type { fib 2 = 1 } as merely shorthand for { _:() | fib 2 = 1 }. Of course, LH will only accept a value of this type if it has been convinced that fib 2 = 1.

The ==. combinator lets us give a step-by-step proof of this property using equational reasoning. LH will not automatically unfold the recursive calls in the definition of fib while typechecking, so it is crucial that our proof do so. *** QED simply marks the end of the proof.

> fib2_1     :: () -> Proof
> {-@ fib2_1 :: () -> { fib 2 = 1 } @-}
> fib2_1 _
>   =   fib 2
>   ==. fib 1 + fib 0  -- unfold fib once
>   ==. 1              -- unfold fib two more times
>   *** QED

We can use previously proven facts as lemmas within our proofs using the ? "because" combinator.

> fib3_2     :: () -> Proof
> {-@ fib3_2 :: () -> { fib 3 = 2 } @-}
> fib3_2 _
>   =   fib 3
>   ==. fib 2 + fib 1
>   ==. 2              ? (fib2_1 ())
>   *** QED

We'll shift our attention to proving the functor laws for the List and Maybe monads (redefined here along with the identity function for technical reasons).

> -- IMPORTANT: be sure to include these flags with your code
> {-@ LIQUID "--exact-data-cons" @-}
> {-@ LIQUID "--higherorder"@-}
> 
> -- Some basic built-in Haskell functions that we need to redefine in order to reflect
> {-@ reflect id' @-}
> id' :: a -> a
> id' x = x
> 
> {-@ reflect compose @-}
> compose :: (b -> c) -> (a -> b) -> (a -> c)
> compose f g x = f (g x)
> 
> -- Redefined Maybe, with map
> data Option a = N | J a
> 
> {-@ reflect optMap @-}
> optMap :: (a -> b) -> Option a -> Option b
> optMap f N = N
> optMap f (J x) = J $ f x
> 
> -- Redefined List, with map
> data List a = E | C a (List a)
> 
> {-@ reflect listMap @-}
> listMap :: (a -> b) -> List a -> List b
> listMap f E = E
> listMap f (C x xs) = C (f x) (listMap f xs)

Finish the proof of the first functor law for Option. Note the use of case analysis in this proof. Hint: Just unfold the definition of optMap.

> {-@ propOptMapFuncId :: x:(Option a) -> {optMap id' x = x} @-}
> propOptMapFuncId :: Option a -> Proof
> propOptMapFuncId N = optMap id' N ==. N *** QED
> propOptMapFuncId (J x)
>     =   optMap id' (J x)
> -- <<FILL IN>>
>     ==. J x
>     *** QED

Most of the first functor law for lists is proven for you below. Fill in the missing piece. Note that that the proof of the law, propListMapFuncId, needs to call itself recursively. This is a proof by induction.

> {-@ propListMapFuncId :: xs:(List a) -> {listMap id' xs = xs} @-}
> propListMapFuncId :: List a -> Proof
> propListMapFuncId E = listMap id' E ==. E *** QED
> propListMapFuncId (C x xs)
>     =   listMap id' (C x xs)
>     -- <<FILL IN>>
>     ==. C x xs                     ? propListMapFuncId xs
>     *** QED

> {-@ propOptMapFuncComp :: f:_ -> g:_ -> o:(Option a) -> { optMap f (optMap g o) = optMap (compose f g) o } @-}
> propOptMapFuncComp :: (b -> c) -> (a -> b) -> Option a -> Proof
> propOptMapFuncComp f g N
>     =   optMap f (optMap g N)
>     ==. optMap (compose f g) N *** QED
> propOptMapFuncComp f g (J x)
>     =   optMap f (optMap g (J x))
> -- <<FILL IN>>
>     ==. optMap (compose f g) (J x)
>     *** QED

> 
> {-@ propListMapFuncComp :: f:_ -> g:_ -> l:(List a) -> { listMap f (listMap g l) = listMap (compose f g) l } @-}
> propListMapFuncComp :: (b -> c) -> (a -> b) -> List a -> Proof
> propListMapFuncComp = undefined

Challenge: Monad Laws

State and prove the monad laws for your favorite monad.

Acknowledgements: this exercise heavily borrows from materials available on the LiquidHaskell website.

CIS 552: Advanced Programming

Fall 2019

Refinement Types

Proving Program Properties

Challenge: Monad Laws