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