# Data Types

{-# LANGUAGE TupleSections #-} {-@ LIQUID "--no-termination" @-} module DataTypes where import Prelude hiding (length, sum, take)

# Example: Lists

Lets define our own List data type:

data List a = Emp | (:::) a (List a) deriving (Eq, Ord, Show) infixr 9 :::

# Specifying the Length of a List

Measure

Haskell function with a single equation per constructor

{-@ measure length @-} {-@ length :: List a -> Nat @-} length :: List a -> Int length Emp = 0 length (_:::xs) = 1 + length xs

# Specifying the Length of a List

Measure: Strengthens type of data constructor

data List a where

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

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


# Example: Partial Functions

Fear head and tail no more!

{-@ head :: List a -> a @-} head (x:::_) = x head _ = impossible "head" {-@ tail :: List a -> List a @-} tail (_:::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

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

Partial Functions are automatically detected!

# 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

Q: Use measures to specify a good type for take

{-@ take :: i:Int -> xs:List a -> List a @-} take 0 Emp = Emp take i (x:::xs) = if i == 0 then Emp else x:::(take (i-1) xs) take i Emp = 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
• 4. Case Study: Insert Sort