{-# LANGUAGE TupleSections #-}
{-@ LIQUID "--no-warnings" @-}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--no-termination" @-}
{- LIQUID "--totality" @-} -- totality does not play well with record selectors
{-@ LIQUID "--diff" @-}
module DataTypes where
-- import qualified Data.Text as T
-- import qualified Data.Text.Unsafe as T
import Prelude hiding (length, sum, take)
import qualified Data.Set as S -- hiding (elems, insert)
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 N = 0
sum (C x xs) = x + sum xs
{-@ data List [length] a = N | C {hd :: a, tl :: List a } @-}
{-@ 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

Lets define our own `List`

data type:

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

**Measure**

Haskell function with *a single equation per constructor*

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

**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}
```

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`

.

A convenient *type alias*

{-@ type ListNE a = {v:List a| 0 < length v} @-}

{-@ 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!

`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.

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

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

... HeartBleed **cannot** happen!

safeTake = takeWord16 2 (pack "hat")
unsafeTake = takeWord16 10 (pack "hat")

**Refinements:**Types + Predicates**Automation:**SMT Implication**Measures:**Specify Properties of Data

What properties can be expressed in the logic?

Linear Arithmetic, Booleans, Uninterpreted Functions, ... (SMT logic)

Terminating Haskell functions.

**Next:** Termination

**Next:** Refinement Reflection