Data Types

Example: Lists

Lets define our own List data type:

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

Specifying the Length of a List

Measure

Haskell function with a single equation per constructor

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

Specifying the Length of a List

Measure

Automagically Strengthens type of data constructor

data List a where

Emp   :: {v:List a | length v = 0}

(:::) :: x:a -> xs:List a
-> {v:List a | length v = 1 + length 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 < length v} @-}

A Useful Partial Function foldr1

Fold f over list initially using first element:

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

Exercise: average

{-@ average' :: List Int -> Int @-} average' xs = total div n where total = foldr1 (+) xs n = length 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 | length v == N} @-}

Make illegal states unrepresentable

badYear = Year (1 ::: Emp)

Refine Data Constructors

Refine Type to Legal Values

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

Automagically strengthens type of data constructor

data Year a where
Year :: ListN a 12 -> Year a

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

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data

Next: Case Study