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.













Naming Non-Empty Lists


A convenient type alias


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













Totality Checking in Liquid Haskell


{-@ LIQUID "--totality" @-} {-@ headt :: List a -> a @-} headt (C x _) = x {-@ tailt :: ListNE a -> List a @-} tailt (C _ xs) = xs



Partial Functions are automatically detected when totality check is on!













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 "Niki") unsafeTake = takeWord16 10 (pack "Niki")
















Recap



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


What properties can be expressed in the logic?

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

  • Terminating Reflected Haskell functions.


Next: Termination

Next: Refinement Reflection