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