Case Study: Sorting Lists (Revisited)


Recall our datatype for Ordered Lists

(Each) head-value oHd no bigger than each tail-value in oTl

{-@ data OList a = Emp | (:<) {oHd :: a, oTl :: OList {v:a|oHd<=v}} @-} okList :: OList Int okList = 1 :< 2 :< 3 :< Emp -- legal badList :: OList Int badList = 1 :< 3 :< 2 :< Emp -- illegal

Lets use it to implement Insertion Sort and Merge-Sort

Exercise: Insertion Sort actually Sorts


Update our code to verify that the output is sorted

{- isort :: (Ord a) => [a] -> OList a isort [] = Emp isort (x:xs) = insert x (isort xs) insert :: (Ord a) => a -> OList a -> OList a insert x (y:ys) | x <= y = y : x : ys | otherwise = y : insert x ys insert x [] = [x] -}

Exercise: Yikes, so much red. Can you fix it?

Exercise: Merge Sort actually Sorts

Exercise: Update our code to verify that the output is sorted

msort :: (Ord a) => [a] -> OList a msort [] = Emp msort [x] = x :< Emp msort xs = let (xs1, xs2) = split xs in merge (msort xs1) (msort xs2) split :: [a] -> ([a], [a]) split (x:y:zs) = let (xs, ys) = split zs in (x:xs, y:ys) split xs = (xs, []) merge :: (Ord a) => OList a -> OList a -> OList a merge xs Emp = xs merge Emp ys = ys merge (x :< xs) (y :< ys) | x <= y = x :< merge xs (y :< ys) | otherwise = y :< merge (x :< xs) ys

Invariants In Constructors





Make illegal values unrepresentable!


But tedious to have multiple list types ...

Abstracting Refinements





Parameterize refinements over types

i.e. decouple the invariant from the data structure

Abstracting Refinements


Parameterize refinements over types

                   data [a]<rel :: a -> a -> Bool> where
                     = []
                     | (:) { hd :: a
                           , tl :: [{v:a | rel hd v}]}

Abstracting Refinements


Parameterize refinements over types

                   data [a]<rel :: a -> a -> Bool> where
                     = []
                     | (:) { hd :: a
                           , tl :: [{v:a | rel hd v}]}

Refinement says rel hd v holds for every value v in tl

rel is <= means list is increasing

rel is >= means list is increasing

rel is != means list is all-unique

Abstracting Refinements


Instantiate refinements to get different invariants!

{-@ type Incrs a = [a]<{\x y -> x <= y}> @-} {-@ incList :: Incrs Int @-} incList = [1,2,3] {-@ type Decrs a = [a]<{\x y -> x >= y}> @-} {-@ decList :: Decrs Int @-} decList = [1,2,3] {-@ type Diffs a = [a]<{\x y -> x != y}> @-} {-@ diffList :: Diffs Int @-} diffList = [3,1,1]

Abstract Refinements: Insertion Sort


Inference FTW!

{- {-@ isort' :: (Ord a) => [a] -> Incrs a @-} isort' :: (Ord a) => [a] -> [a] isort' [] = [] isort' (x:xs) = insert' x (isort' xs) insert' :: (Ord a) => a -> [a] -> [a] insert' x (y:ys) | x <= y = x : y : ys | otherwise = y : insert' x ys insert' x [] = [x] -}

Abstract Refinements: Merge Sort

Inference FTW!

{- {-@ msort' :: (Ord a) => [a] -> Incrs a @-} msort' :: (Ord a) => [a] -> [a] msort' [] = [] msort' xs = let (xs1, xs2) = split' xs in merge' (msort' xs1) (msort' xs2) split' :: [a] -> ([a], [a]) split' (x:y:zs) = let (xs, ys) = split' zs in (x:xs, y:ys) split' xs = (xs, []) merge' :: (Ord a) => [a] -> [a] -> [a] merge' xs [] = xs merge' [] ys = ys merge' (x:xs) (y:ys) | x <= y = x : merge' xs (y:ys) | otherwise = y : merge' (x:xs) ys -}

Recap: Invariant via Refined Constructors




             Emp  :: OList a
             (:<) :: oHd:a -> OList {v:a |oHd < v} -> OList a

Invariant Checked at Construction and Instantiated at Pattern-Matching

Simply by applying and un-applying refined constructor type!