# Data Types

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

head :: List a -> a
tail :: List a -> List a
headt :: List a -> a
tailt :: List a -> List a
impossible :: String -> a
avg :: List Int -> Int
take :: Int -> List a -> List a
sum :: List Int -> Int
sum Emp = 0
sum (x ::: xs) = x + sum xs
{-@ data List [length] @-}
{-@ invariant {v: List a | 0 <= length v} @-}
{-@ type Nat = {v:Int | v >= 0} @-}
{-@ type Pos = {v:Int | v > 0} @-}
{-@ impossible :: {v:_ | false} -> a @-}
impossible = error
{-@ safeDiv :: Int -> {v:Int | v /= 0} -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv _ 0 = impossible "divide-by-zero"
safeDiv x n = x `div` n

# 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 Overflow Bug!

Assuming the library `Text`

types...

data Text
pack :: String -> Text
takeWord16 :: Int -> Text -> Text
pack = undefined
takeWord16 = undefined

{-@ measure tlen :: Text -> Int @-}
{-@ assume pack :: i:String -> {o:Text | len i == tlen o } @-}
{-@ assume takeWord16 :: i:Nat -> {v:Text | i <= tlen v} -> Text @-}

... Overflows **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
- 5. Termination