# 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 :: T.Text -> Int @-} {-@ assume T.pack :: i:String -> {o:T.Text | len i == tlen o } @-} {-@ assume T.takeWord16 :: i:Nat -> {v:T.Text | i <= tlen v} -> T.Text @-}

... HeartBleed cannot happen!

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