# Abstract Refinements

## Key Idea

Abstract Your Property Away to make the specification Modular!

## Monomorphic 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:

maxEven :: Even
maxEven = max 40 42


## Refining max type (III)

If max gets two Prime numbers:

max     :: Prime -> Prime -> Prime


Then it returns a Prime number:

maxPrime :: Prime
maxPrime = max 7 13


## Refining max type

So, what is the primal 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 on Int,
• if max takes two inputs that satisfy p,
• then 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     = max 3 5


## 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 -> Prop > = Emp | (:::) { hd :: a , tl :: List < p > a< p hd > } @-}

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 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:Bounded Refinements