05_Composition.lhs

Abstract Refinements {#composition}
===================================

Very General Mechanism 
----------------------

**Next:** Lets add parameters...

<div class="hidden">
\begin{code}
module Composition where

import Prelude hiding ((.))

plus     :: Int -> Int -> Int
plus3'   :: Int -> Int
\end{code}
</div>


Example: `plus`
---------------

\begin{code}
{-@ plus :: x:_ -> y:_ -> {v:_ | v=x+y} @-}
plus x y = x + y
\end{code}


Example: `plus 3` 
-----------------

<br>

\begin{code}
{-@ plus3' :: x:Int -> {v:Int | v = x + 3} @-}
plus3'     = plus 3
\end{code}

<br>

Easily verified by LiquidHaskell

A Composed Variant
------------------

Lets define `plus3` by *composition*

A Composition Operator 
----------------------

\begin{code}
(#) :: (b -> c) -> (a -> b) -> a -> c
(#) f g x = f (g x)
\end{code}


`plus3` By Composition
-----------------------

\begin{code}
{-@ plus3'' :: x:Int -> {v:Int | v = x + 3} @-}
plus3''     = plus 1 # plus 2
\end{code}

<br>

Yikes! Verification *fails*. But why?

<br>

<div class="fragment">(Hover mouse over `#` for a clue)</div>

How to type compose (#) ? 
-------------------------

This specification is *too weak* <br>

\begin{spec} <br>
(#) :: (b -> c) -> (a -> b) -> (a -> c)
\end{spec}

<br>

Output type does not *relate* `c` with `a`!

How to type compose (.) ?
-------------------------

Write specification with abstract refinement type:

<br>

\begin{code}
{-@ (.) :: forall <p :: b->c->Prop, 
                   q :: a->b->Prop>.
             f:(x:b -> c<p x>) 
          -> g:(x:a -> b<q x>) 
          -> y:a -> exists[z:b<q y>].c<p z>
 @-}
(.) f g y = f (g y)
\end{code}

Using (.) Operator 
------------------

<br>

\begin{code}
{-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
plus3     = plus 1 . plus 2
\end{code}

<br>

<div class="fragment">*Verifies!*</div>


Using (.) Operator 
------------------

\begin{spec} <br>
{-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
plus3     = plus 1 . plus 2
\end{spec}

<br>

LiquidHaskell *instantiates*

- `p` with `\x -> v = x + 1`
- `q` with `\x -> v = x + 2`

Using (.) Operator 
------------------

\begin{spec} <br>
{-@ plus3 :: x:Int -> {v:Int | v = x + 3} @-}
plus3     = plus 1 . plus 2
\end{spec}

<br> To *infer* that output of `plus3` has type: 

`exists [z:{v = y + 2}].{v = z + 1}`

<div class="fragment">

`<:`

`{v:Int|v=3}`
</div>


Recap
-----

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