Data Types



















Example: Lists


Lets define our own List data type:


data List a = N -- Nil | C 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 N = 0 length (C _ xs) = 1 + length xs













Specifying the Length of a List


Measure

Strengthens type of data constructor


data List a where

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

  C :: x:a -> xs:List a
    -> {v:List a | length v = 1 + length xs}













Using Measures
















Example: Partial Functions


Fear head and tail no more!

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



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













Back to average


{-@ avg :: List Int -> Int @-} avg xs = safeDiv total n where total = sum xs n = length xs -- returns a Nat


Q: Write type for avg that verifies safe division.













In bounds take

Use measures to specify take

{-@ take :: i:Int -> xs:List a -> List a @-} take 0 N = N take i (C x xs) = if i == 0 then N else x `C` (take (i-1) xs) take i N = impossible "Out of bounds indexing!"













Catch the The Heartbleed Bug!

Assuming the library Text types...


{-@ measure tlen :: Text -> Int @-} {-@ assume pack :: i:String -> {o:Text | len i == tlen o } @-} {-@ assume takeWord16 :: i:Nat -> {v:Text | i <= tlen v} -> Text @-}


... HeartBleed cannot happen!

safeTake = takeWord16 2 (pack "hat") unsafeTake = takeWord16 10 (pack "hat")
















Recap



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


What properties can be expressed in the logic?

  • Linear Arithmetic, Booleans, Uninterpreted Functions, ... (SMT logic)

  • Terminating Haskell functions.


Next: Termination
Next: Refinement Reflection