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