List Sorting

Example: Lists

Lets define our own List data type:

data List a = Emp -- Nil | (:::) a (List a) -- Cons

Specifying the Length of a List

Measure

Haskell function with a single equation per constructor

{-@ measure length @-} 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}

Multiple Measures

Hence, we can write Set-valued measures

Using the Data.Set API for convenience

import qualified Data.Set as S

Specifying A Lists Elements

{-@ measure elems @-} elems :: (Ord a) => List a -> S.Set a elems Emp = S.empty elems (x:::xs) = addElem x xs {-@ inline addElem @-} addElem :: (Ord a) => a -> List a -> S.Set a addElem x xs = S.union (S.singleton x) (elems xs)

inline lets us reuse Haskell terms in refinements.

Multiple Measures

Strengthens type of data constructor

data List a where

Emp   :: {v:List a | length v == 0
&& elems v == S.empty}

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

Example : Inserting Elements

{-@ insert :: x:a -> xs:List a -> {v : List a | length v == length xs + 1 && elems v == addElem x xs } @-} insert x Emp = x ::: Emp insert x (y ::: ys) | x <= y = x ::: y ::: ys | otherwise = y ::: insert x ys

Can we specify sortedness?

Refining Data Types

Make illegal states unrepresentable

Example: Sorted Lists

Lets define a type for ordered lists

data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList a }

Ordered Lists

Lets refine the type to enforce order

{-@ data OList a = OEmp | (:<:) { oHd :: a , oTl :: OList {v:a | oHd <= v}} @-}

Head oHd is smaller than every value v in tail oTl

Ordered Lists

Illegal values unrepresentable

okList :: OList Int okList = 1 :<: 2 :<: 3 :<: OEmp badList :: OList Int badList = 1 :<: 3 :<: 2 :<: OEmp

Exercise: Insertion Sort

Q: Oops. There's a problem! Can you fix it?

{-@ sortO :: xs:List a -> OList a @-} sortO Emp = OEmp sortO (x:::xs) = insertO x (sortO xs) {-@ insertO :: x:a -> xs:_ -> OList a @-} insertO x (y :<: ys) | x <= y = y :<: x :<: ys | otherwise = y :<: insertO x ys insertO x _ = x :<: OEmp

Refinements vs. Full Dependent Types

• Limited to decidable logics but ...

• Offer massive amounts of automation

Compare with insertionSort in:

Problem: How to reason about elems and lenght of an OList?

Solution: Make OList an instance of List using Abstract Refinements!

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data

Next: Abstract Refinements