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