Programming with Refinement Types

Key Idea

Abstract The Property Away to make the specification Modular!

Then, instantiate the property back to get your specification.

Ordered Lists

Previously we saw how to refine the list data definition to get ordered lists:

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

Just abstract the property away!

Abstract Refinements on Data Structures

data List a = Emp | (:::) { hd :: a , tl :: List a } {-@ data List a < p :: a -> a -> Bool > = Emp | (:::) { hd :: a , tl :: List < p > a< p hd > } @-} -- a < p hd > stands for {v:a | p hd v}

Every element of the tail recursively satisfies p on the head!

Instantiation of Refinements

Unrefined Lists

{-@ type TList a = List <{\x v -> true }> a @-}

Increasing Lists

{-@ type OList a = List <{\x v -> x <= v}> a @-}

Decreasing Lists

{-@ type DList a = List <{\x v -> v <= x}> a @-}

Unique Lists

{-@ type UList a = List <{\x v -> x /= v}> a @-}

Using Abstract Refinements

Use increasing lists

{-@ type OList a = List <{\x v -> x <= v}> a @-}

to specify insertion sort, as before!

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

Haskell's list

Haskell build-in list comes parameterized for you!

You can just instantiate the abstract refinement!

{-@ type IList a = [a]<{\x v -> (x <= v)}> @-}

And prove recursive list properties!

{-@ sort :: (Ord a) => [a] -> IList a @-} sort :: (Ord a) => [a] -> [a] sort = mergeAll . sequences where sequences (a:b:xs) | a `compare` b == GT = descending b [a] xs | otherwise = ascending b (a:) xs sequences [x] = [[x]] sequences [] = [[]] {- descending :: x:a -> IList {v:a | x < v} -> [a] -> [IList a] @-} descending a as (b:bs) | a `compare` b == GT = descending b (a:as) bs descending a as bs = (a:as): sequences bs {- ascending :: x:a -> (IList {v:a|v>=x} -> IList a) -> [a] -> [IList a] @-} ascending a as (b:bs) | a `compare` b /= GT = ascending b (\ys -> as (a:ys)) bs ascending a as bs = as [a]: sequences bs mergeAll [x] = x mergeAll xs = mergeAll (mergePairs xs) mergePairs (a:b:xs) = merge1 a b: mergePairs xs mergePairs [x] = [x] mergePairs [] = []

{-@ descending :: x:a -> IList {v:a | x < v} -> [a] -> [IList a] @-}
{-@ ascending :: x:a -> (IList {v:a|v>=x} -> IList a) -> [a] -> [IList a] @-}

merge1 (a:as) (b:bs) | a `compare` b == GT = b:merge1 (a:as) bs | otherwise = a:merge1 as (b:bs) merge1 [] bs = bs merge1 as [] = as

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Specify Properties of Data
Abstract Refinements: Decouple properties from code

Next:Bounded Refinements