AbstractRefinements.lhs

% Abstract Refinements

Abstract Refinements
--------------------

\begin{code}
module AbstractRefinements where
\end{code}


Abstract Refinements
--------------------

<br>

\begin{code} Consider the following function 
maxInt     :: Int -> Int -> Int 
maxInt x y = if x <= y then y else x 
\end{code}

<br>

\begin{code} We can give `maxInt` many (incomparable) refinement types:
maxInt :: Nat -> Nat -> Nat

maxInt :: Even -> Even -> Even

maxInt :: Prime -> Prime -> Prime
\end{code}

But **which** is the **right** type?


Parametric Invariants 
---------------------

`maxInt` 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
--------------------- 

\begin{code}
{-@ maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p> @-}
maxInt     :: Int -> Int -> Int 
maxInt x y = if x <= y then y else x 
\end{code}



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`, 

- `maxInt` takes two **inputs** of which satisfy `p`,

- `maxInt` returns an **output** that satisfies `p`. 


Parametric Invariants via Abstract Refinements
---------------------------------------------- 

\begin{code} We type `maxInt` as
maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p> 
\end{code}

We call `p` an an **abstract refinement** <br>


In the refinement logic,

- abstract refinements are **uninterpreted function symbols**

- which (only) satisfy the *congruence axiom*: forall x, y. x = y => (p x) = (p y)



Using Abstract Refinements
--------------------------

- **If** we call `maxInt` with two `Int`s with the same concrete refinement,

- **Then** the `p` will be instantiated with that concrete refinement,

- **The output** of the call will also enjoy the concrete refinement.

For example, the refinement is instantiated with `\v -> v >= 0` <br>

\begin{code}
{-@ maxNat :: Nat @-}
maxNat     :: Int
maxNat     = maxInt 2 5
\end{code}

Using Abstract Refinements
--------------------------

- **If** we call `maxInt` with two `Int`s with the same concrete refinement,

- **Then** the `p` will be instantiated with that concrete refinement,

- **The output** of the call will also enjoy the concrete refinement.

Or any other property <br>

\begin{code}
{-@ type RGB = {v: Int | ((0 <= v) && (v < 256)) } @-}
\end{code}

<br> to verify <br>

\begin{code}
{-@ maxRGB :: RGB @-}
maxRGB     :: Int
maxRGB     = maxInt 56 8
\end{code}