Data Types



















Example: Lists


Lets define our own List data type:


data List a = N             -- Nil
            | C a (List a)  -- Cons
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













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"
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 < length v} @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX













Totality Checking in Liquid Haskell


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



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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


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













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


... HeartBleed cannot happen!

safeTake   = takeWord16 2  (pack "Niki")
unsafeTake = takeWord16 10 (pack "Niki")
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
















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