Data Types


Example: Lists


Lets define our own List data type:


data List a = Emp -- Nil | (:::) a (List a) -- Cons

Specifying the size of a List


Measure

Haskell function with a single equation per constructor

{-@ measure size @-} size :: List a -> Int size Emp = 0 size (_ ::: xs) = 1 + size xs

Specifying the size of a List

Measure

Strengthens type of data constructor

data List a where
  Emp   :: {v:List a | size v = 0}
  (:::) :: x:a -> xs:List a -> {v:List a|size v = 1 + size xs}

Using Measures


Exercise: Partial Functions


Fear head and tail no more!

{-@ head :: List a -> a @-} head (x ::: _) = x head _ = impossible "head" {-@ tail :: List a -> List a @-} tail (_ ::: xs) = xs tail _ = impossible "tail"

Q: Write types for head and tail that verify impossible.

Naming Non-Empty Lists


A convenient type alias


{-@ type ListNE a = {v:List a| 0 < size v} @-}



A Useful Partial Function: Fold / Reduce


Fold or Reduce f over any list using seed acc


foldr :: (a -> b -> b) -> b -> List a -> b foldr _ acc Emp = acc foldr f acc (x ::: xs) = f x (foldr f acc xs)


A Useful Partial Function: Fold / Reduce


Fold or Reduce f over non-empty list using first element as seed


{-@ foldr1 :: (a -> a -> a) -> List a -> a @-} foldr1 f (x ::: xs) = foldr f x xs foldr1 _ _ = impossible "foldr1"


Q: How shall we fix foldr1?

Exercise: average


{-@ average' :: List Int -> Int @-} average' xs = total `div` n where total = foldr1 (+) xs n = size xs


Q: What is a safe input type for average'?


Refining Data Types



    Make illegal states unrepresentable


Example: Year is 12 Months


data Year a = Year (List a)


Legal Values: Lists of 12 elements, e.g.


"jan" ::: "feb" ::: ... ::: "dec" ::: Emp"


Example: Year is 12 Months


Refine Type to Legal Values

{-@ data Year a = Year (ListN a 12) @-}

Lists Of A Given Size

{-@ type ListN a N = {v: List a | size v == N} @-}

Make illegal states unrepresentable

badYear = Year (1 ::: Emp)

Exercise: map


{-@ map :: (a -> b) -> xs:List a -> List b @-} map _ Emp = Emp map f (x ::: xs) = f x ::: map f xs

Q: Can you fix map to verify tempAverage?

data Weather = W { temp :: Int, rain :: Int } tempAverage :: Year Weather -> Int tempAverage (Year ms) = average months where months = map temp ms

Exercise: init


{-@ init :: (Int -> a) -> Nat -> List a @-} init _ 0 = Emp init f n = f n ::: init f (n-1)


Q: Can you fix the type of init so that sanDiegoTemp is accepted?

sanDiegoTemp :: Year Int sanDiegoTemp = Year (init (const 72) 12)

Exercise: init'


{-@ init' :: (Int -> a) -> n:Nat -> List a @-} init' f n = go 0 where go i | i < n = f i ::: go (i+1) | otherwise = Emp

Q: For bonus points, fix init' so sanDiegoTemp'is accepted?

sanDiegoTemp' :: Year Int sanDiegoTemp' = Year (init' (const 72) 12)

Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping
Measures: Specify Properties of Data


Case Study: Insertion Sort