Data Types


Example: Lists


Lets define our own List data type:


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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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



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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: How shall we fix foldr1?

Exercise: average


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


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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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) @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Lists Of A Given Size

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

Make illegal states unrepresentable

badYear = Year (1 ::: Emp)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Exercise: map


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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Exercise: init


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


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

sanDiegoTemp :: Year Int
sanDiegoTemp = Year (init (const 7212)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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

sanDiegoTemp' :: Year Int
sanDiegoTemp' = Year (init' (const 7212)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Recap


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


Case Study: Insertion Sort