Decouple Invariants From Data {#recursive} 
==========================================

Recursive Structures 
--------------------

<div class="fragment">
Lets see another example of decoupling...
</div>

<div class="hidden">
\begin{code}
{-# LANGUAGE NoMonomorphismRestriction #-}

module List (insertSort) where

{-@ LIQUID "--no-termination" @-}

mergeSort     :: Ord a => [a] -> [a]
insertSort :: (Ord a) => [a] -> L a 
slist :: L Int
slist' :: L Int
iGoUp, iGoDn, iDiff :: [Int]
infixr `C`
\end{code}
</div>

Decouple Invariants From Recursive Data
=======================================

Recall: Lists
-------------

\begin{code}
data L a = N 
         | C a (L a)
\end{code}


Recall: Refined Constructors 
----------------------------

Define *increasing* Lists with strengthened constructors:

\begin{code} <br>
data L a where
  N :: L a
  C :: hd:a -> tl: L {v:a | hd <= v} -> L a
\end{code}

Problem: Decreasing Lists?
--------------------------

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

<br>

<div class="fragment">
*Separate* types are tedious...
</div>


Abstract That Refinement!
-------------------------

\begin{code}
{-@ data L a <p :: a -> a -> Prop>
      = N 
      | C (hd :: a) (tl :: (L <p> a<p hd>)) @-}
\end{code}

<br>

- <div class="fragment"> `p` is a *binary* relation between two `a` values</div>

- <div class="fragment"> Definition relates `hd` with *all* the elements of `tl`</div>

- <div class="fragment"> Recursive: `p` holds for *every pair* of elements!</div>

Example
-------

Consider a list with *three* or more elements 

\begin{code} <br>
x1 `C` x2 `C` x3 `C` rest :: L <p> a 
\end{code}

Example: Unfold Once
--------------------

\begin{code} <br> 
x1                 :: a
x2 `C` x3 `C` rest :: L <p> a<p x1> 
\end{code}

Example: Unfold Twice
---------------------

\begin{code} <br> 
x1          :: a
x2          :: a<p x1>  
x3 `C` rest :: L <p> a<p x1 && p x2> 
\end{code}

Example: Unfold Thrice
----------------------

\begin{code} <br> 
x1   :: a
x2   :: a<p x1>  
x3   :: a<p x1 && p x2>  
rest :: L <p> a<p x1 && p x2 && p x3> 
\end{code}

<br>

<div class="fragment">
Note how `p` holds between **every pair** of elements in the list. 
</div>

A Concrete Example
------------------

That was a rather *abstract*!

<br>

How can we *use* fact that `p` holds between *every pair* ?


Example: Increasing Lists
-------------------------

*Instantiate* `p` with a *concrete* refinement

<br>

\begin{code}
{-@ type IncL a = L <{\hd v -> hd <= v}> a @-}
\end{code}

<br>

- <div class="fragment"> Refinement says `hd` less than each tail element `v`,</div>

- <div class="fragment"> Thus, `IncL` denotes *increaing* lists. </div>

Example: Increasing Lists
-------------------------

LiquidHaskell verifies that `slist` is indeed increasing...

\begin{code}
{-@ slist :: IncL Int @-}
slist     = 1 `C` 6 `C` 12 `C` N
\end{code}

<br> 

<div class="fragment">

... and protests that `slist'` is not: 

\begin{code}
{-@ slist' :: IncL Int @-}
slist' = 6 `C` 1 `C` 12 `C` N
\end{code}
</div>

Insertion Sort
--------------

\begin{code}
{-@ insertSort :: (Ord a) => [a] -> IncL a @-}
insertSort     = foldr insert N

insert y N          = y `C` N
insert y (x `C` xs) 
  | y < x           = y `C` (x `C` xs)
  | otherwise       = x `C` insert y xs
\end{code}

<br>

(*Hover* over `insert'` to see inferred type.)

Checking GHC Lists
------------------

<a href="http://goto.ucsd.edu:8090/index.html#?demo=Order.hs" target= "_blank">Demo:</a> 
Above applies to GHC's List definition:

\begin{code} <br> 
data [a] <p :: a -> a -> Prop>
  = [] 
  | (:) (h :: a) (tl :: ([a<p h>]<p>))
\end{code}

Checking GHC Lists
------------------

Increasing Lists

<br>

\begin{code}
{-@ type Incs a = [a]<{\h v -> h <= v}> @-}

{-@ iGoUp :: Incs Int @-}
iGoUp     = [1,2,3]
\end{code}

Checking GHC Lists
------------------

Decreasing Lists

<br>

\begin{code}
{-@ type Decs a = [a]<{\h v -> h >= v}> @-}

{-@ iGoDn :: Decs Int @-}
iGoDn     = [3,2,1]
\end{code}


Checking GHC Lists
------------------

Duplicate-free Lists

<br>

\begin{code}
{-@ type Difs a = [a]<{\h v -> h /= v}> @-}

{-@ iDiff :: Difs Int @-}
iDiff     = [1,3,2]
\end{code}

Checking GHC Lists
------------------

Now we can check all the usual list sorting algorithms 

Example: `mergeSort` [1/2]
--------------------------

\begin{code}
{-@ mergeSort  :: (Ord a) => [a] -> Incs a @-}
mergeSort []   = []
mergeSort [x]  = [x]
mergeSort xs   = merge xs1' xs2' 
  where 
   (xs1, xs2)  = split xs
   xs1'        = mergeSort xs1
   xs2'        = mergeSort xs2
\end{code}

Example: `mergeSort` [1/2]
--------------------------

\begin{code}
split (x:y:zs) = (x:xs, y:ys) 
  where 
    (xs, ys)   = split zs
split xs       = (xs, [])

merge xs []    = xs
merge [] ys    = ys
merge (x:xs) (y:ys) 
  | x <= y     = x : merge xs (y:ys)
  | otherwise  = y : merge (x:xs) ys
\end{code}

Example: `Data.List.sort` 
-------------------------

GHC's "official" list sorting routine

Juggling lists of increasing & decreasing lists


Ex: `Data.List.sort` [1/4]
--------------------------

Juggling lists of increasing & decreasing lists

<br>

\begin{code}
{-@ sort :: (Ord a) => [a] -> Incs a  @-}
sort = mergeAll . sequences

sequences (a:b:xs)
  | a `compare` b == GT = descending b [a]  xs
  | otherwise           = ascending  b (a:) xs
sequences [x]           = [[x]]
sequences []            = [[]]
\end{code}

Ex: `Data.List.sort` [2/4]
--------------------------

Juggling lists of increasing & decreasing lists

<br>

\begin{code}
descending a as (b:bs)
  | a `compare` b == GT 
  = descending b (a:as) bs
descending a as bs      
  = (a:as): sequences bs
\end{code}

Ex: `Data.List.sort` [3/4]
--------------------------

Juggling lists of increasing & decreasing lists

<br>


\begin{code}
ascending a as (b:bs)
  | a `compare` b /= GT 
  = ascending b (\ys -> as (a:ys)) bs
ascending a as bs      
  = as [a]: sequences bs
\end{code}

Ex: `Data.List.sort` [4/4]
--------------------------

Juggling lists of increasing & decreasing lists

<br>

\begin{code}
mergeAll [x]        = x
mergeAll xs         = mergeAll (mergePairs xs)

mergePairs (a:b:xs) = merge a b: mergePairs xs
mergePairs [x]      = [x]
mergePairs []       = []
\end{code}

Phew!
-----

Lets see one last example...


Example: Binary Trees
---------------------

... `Map` from keys of type `k` to values of type `a` 

<br>

<div class="fragment">

Implemented, in `Data.Map` as a binary tree:

<br>

\begin{code}
data Map k a = Tip
             | Bin Size k a (Map k a) (Map k a)

type Size    = Int
\end{code}
</div>

Two Abstract Refinements
------------------------

- `l` : relates root `key` with `left`-subtree keys
- `r` : relates root `key` with `right`-subtree keys

\begin{code}
{-@ data Map k a < l :: k -> k -> Prop
                 , r :: k -> k -> Prop >
    = Tip
    | Bin (sz :: Size) (key :: k) (val :: a)
          (left  :: Map <l,r> (k<l key>) a)
          (right :: Map <l,r> (k<r key>) a) @-}
\end{code}


Ex: Binary Search Trees
-----------------------

Keys are *Binary-Search* Ordered

<br>

\begin{code}
{-@ type BST k a = 
      Map <{\r v -> v < r }, 
           {\r v -> v > r }> 
          k a                   @-}
\end{code}

Ex: Minimum Heaps 
-----------------

Root contains *minimum* value

<br>

\begin{code}
{-@ type MinHeap k a = 
      Map <{\r v -> r <= v}, 
           {\r v -> r <= v}> 
           k a               @-}
\end{code}

Ex: Maximum Heaps 
-----------------

Root contains *maximum* value

<br>

\begin{code}
{-@ type MaxHeap k a = 
      Map <{\r v -> r >= v}, 
           {\r v -> r >= v}> 
           k a               @-}
\end{code}


Example: Data.Map
-----------------

Standard Key-Value container

- <div class="fragment">1300+ non-comment lines</div>

- <div class="fragment">`insert`, `split`, `merge`,...</div>

- <div class="fragment">Rotation, Rebalance,...</div>

<div class="fragment">
SMT & inference crucial for [verification](https://github.com/ucsd-progsys/liquidhaskell/blob/master/benchmarks/esop2013-submission/Base.hs)
</div>

<br>

<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=Map.hs" target="_blank">Demo:</a>Try online!
</div>

Recap: Abstract Refinements
---------------------------

<div class="fragment">

Decouple invariants from *functions*

+ `max`
+ `loop`
+ `foldr`

</div>

<div class="fragment">
Decouple invariants from *data*

+ `Vector`
+ `List`
+ `Tree`

</div>


Recap
-----

1. **Refinements:** Types + Predicates
2. **Subtyping:** SMT Implication
3. **Measures:** Strengthened Constructors
4. **Abstract Refinements:* Decouple Invariants 
5. <div class="fragment">Er, what of *lazy evaluation*?</div>