Abstract Refinements
























Key Idea


Abstract Your Property Away to make the specification Modular!












Ordered Lists


We saw how to define ordered lists:


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


We can get ordered lists as an instanse of an abstractly refined list type.





















Polymorphic Max Function


Consinder a monomorphic max function: 

max     :: Int -> Int -> Int
max x y = if x >= y then x else y


How can we refine the type of max?



















Refining max type (I)


If max gets two Odd numbers: 

max     :: Odd -> Odd -> Odd



Then it returns an Odd number: 
maxOdd :: Odd
maxOdd = max 3 7










Refining max type (II)


If max gets two Even numbers: 

max     :: Even -> Even -> Even



Then it returns an Even number: 
maxOdd :: Even
maxOdd = max 40 42










Refining max type (III)


If max gets two Prime numbers: 
max     :: Prime -> Prime -> Prime



Then it returns an Prime number: 
maxOdd :: Prime
maxOdd = max 7 13










Refining max type


So, what is the type of max? 

max     :: Odd   -> Odd   -> Odd
max     :: Even  -> Even  -> Even
max     :: Prime -> Prime -> Prime










Polymorphism via Parametric Invariants

max returns one of its two inputs x and y.

  • If both inputs satisfy a property
  • Then output must satisfy that property

This holds, regardless of what that property was!

  • That is, we can abstract over refinements
  • Or, parameterize a type over its refinements.










Parametric Invariants

{-@ max :: forall <p :: Int -> Prop>. 
            Int<p> -> Int<p> -> Int<p> @-}
max     :: Int -> Int -> Int
max x y = if x <= y then y else x

Where

Int<p> is just an abbreviation for {v:Int | (p v)}

This type states explicitly:

  • For any property p, that is a property of Int,
  • max takes two inputs that satisfy p,
  • max returns an output that satisfies p.










Using Abstract Refinements


  • If we call max with two arguments with the same concrete refinement,
  • Then the p will be automagically instantiated with that concrete refinement,
  • The output of the call will also enjoy the concrete refinement. 
{-@ type Odd = {v:Int | (v mod 2) = 1} @-}

{-@ maxOdd :: Odd @-}
maxOdd     :: Int
maxOdd     = max 3 5










Key Idea



Abstract Your 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

a -> Prop> = Emp | (:::) { hd :: a , tl :: List a} @-}


Q: Use abstract refinements to refine the above list data declaration to describe ordered lists.














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


Given increasing lists 

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


We use them 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 -> OList a @-} insert x (y ::: ys) | x <= y = y ::: x ::: ys | otherwise = y ::: insert x ys insert x _ = x ::: Emp














The build in list


Haskell build-in list comes parameterized for you!

You can just instantiate the abstract refinement!

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



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 [] = []



















Recap



  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Specify Properties of Data
  4. Abstract Refinements:Decouple properties from code


Next: Application