04_AbstractRefinements.lhs

  {#abstractrefinements}
========================

<div class="hidden">

\begin{code}
module AbstractRefinements where

import Prelude 
import Language.Haskell.Liquid.Prelude
{-@ LIQUID "--no-termination" @-}

o, no        :: Int
maxInt       :: Int -> Int -> Int
\end{code}
</div>



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



Abstract Refinements
====================

Two Problems
------------

<div class="fragment">

**Problem 1:** 

How do we specify *both* [increasing and decreasing lists](http://web.cecs.pdx.edu/~sheard/Code/QSort.html)?

</div>

<br>

<div class="fragment">

**Problem 2:** 

How do we specify *iteration-dependence* in higher-order functions?

</div>


Problem Is Pervasive
--------------------

Lets distill it to a simple example...

<div class="fragment">

<br>

(First, a few aliases)

<br>

\begin{code}
{-@ type Odd  = {v:Int | (v mod 2) = 1} @-}
{-@ type Even = {v:Int | (v mod 2) = 0} @-}
\end{code}

</div>


Example: `maxInt` 
-----------------

Compute the larger of two `Int`s:

\begin{code} <br> 
maxInt     :: Int -> Int -> Int 
maxInt x y = if y <= x then x else y
\end{code}



Example: `maxInt` 
-----------------

Has *many incomparable* refinement types

\begin{code}<br>
maxInt :: Nat  -> Nat  -> Nat
maxInt :: Even -> Even -> Even
maxInt :: Odd  -> Odd  -> Odd 
\end{code}

<br>

<div class="fragment">Yikes. **Which** one should we use?</div>


Refinement Polymorphism 
-----------------------

`maxInt` returns *one of* its two inputs `x` and `y` 

<div align="center">

<br>

---------   ---   -------------------------------------------
   **If**    :    the *inputs* satisfy a property  

 **Then**    :    the *output* satisfies that property
---------   ---   -------------------------------------------

<br>

</div>

<div class="fragment">Above holds *for all* properties!</div>

<br>

<div class="fragment"> 

**Need to abstract refinements over types**

</div>


By Type Polymorphism?
---------------------

\begin{code} <br> 
max     :: α -> α -> α 
max x y = if y <= x then x else y
\end{code}

<div class="fragment"> 

Instantiate `α` at callsites

\begin{code}
{-@ o :: Odd  @-}
o = maxInt 3 7     -- α := Odd

{-@ e :: Even @-}
e = maxInt 2 8     -- α := Even
\end{code}

</div>

By Type Polymorphism?
---------------------

\begin{code} <br> 
max     :: α -> α -> α 
max x y = if y <= x then x else y
\end{code}

<br>

But there is a fly in the ointment ...

Polymorphic `max` in Haskell
----------------------------

\begin{code} In Haskell the type of max is
max :: (Ord α) => α -> α -> α
\end{code}

<br>

\begin{code} Could *ignore* the class constraints, instantiate as before...
{-@ o :: Odd @-}
o     = max 3 7  -- α := Odd 
\end{code}


Polymorphic `(+)` in Haskell
----------------------------

\begin{code} ... but this is *unsound*!
max :: (Ord α) => α -> α -> α
(+) :: (Num α) => α -> α -> α
\end{code}

<br>

<div class="fragment">

*Ignoring* class constraints would let us "prove":

\begin{code}
{-@ no :: Odd @-}
no     = 3 + 7    -- α := Odd !
\end{code}

</div>

Type Polymorphism? No.
----------------------

<div class="fragment">Need to try a bit harder...</div>

By Parametric Refinements!
--------------------------

That is, enable *quantification over refinements*...

Parametric Refinements 
----------------------

\begin{code}
{-@ maxInt :: forall <p :: Int -> Prop>. 
                Int<p> -> Int<p> -> Int<p>  @-}

maxInt x y = if x <= y then y else x 
\end{code}

<br>


<div class="fragment">Type says: **for any** `p` that is a property of `Int`, </div>

- <div class="fragment">`max` **takes** two `Int`s that satisfy `p`,</div>

- <div class="fragment">`max` **returns** an `Int` that satisfies `p`.</div>

Parametric Refinements 
----------------------

\begin{code}<br>
{-@ maxInt :: forall <p :: Int -> Prop>. 
                Int<p> -> Int<p> -> Int<p>  @-}

maxInt x y = if x <= y then y else x 
\end{code}

<br>

[Key idea: ](http://goto.ucsd.edu/~rjhala/papers/abstract_refinement_types.html) `Int<p>` is `{v:Int | (p v)}`

<br>

<div class="fragment">So, Abstract Refinement is an *uninterpreted function* in SMT logic</div>

Parametric Refinements 
----------------------

\begin{code}<br>
{-@ maxInt :: forall <p :: Int -> Prop>. 
                Int<p> -> Int<p> -> Int<p>  @-}

maxInt x y = if x <= y then y else x 
\end{code}

<br>

**Check** and **Instantiate** type using *SMT & predicate abstraction*

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

- <div class="fragment">**When** we call `maxInt` with args with some refinement,</div>

- <div class="fragment">**Then** `p` instantiated with *same* refinement,</div>

- <div class="fragment">**Result** of call will also have concrete refinement.</div>

<div class="fragment">

\begin{code}
{-@ o' :: Odd  @-}
o' = maxInt 3 7     -- p := \v -> Odd v 

{-@ e' :: Even @-}
e' = maxInt 2 8     -- p := \v -> Even v 
\end{code}

</div>

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

Or any other property 

<br>

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

{-@ rgb :: RGB @-}
rgb = maxInt 56 8
\end{code}


Recap
-----

1. **Refinements:** Types + Predicates
2. **Subtyping:** SMT Implication
3. **Measures:** Strengthened Constructors
4. <div class="fragment">**Abstract:** Refinements over Type Signatures</div>