liquidhaskell-0.8.2.0: docs/slides/plpv14/lhs/08_Recursive.lhs.markdown
Decouple Invariants From Data {#recursive}
==========================================
Recursive Structures
--------------------
<div class="fragment">
Lets see another example of decoupling...
</div>
<div class="hidden">
<pre><span class=hs-linenum>13: </span><span class='hs-comment'>{-# LANGUAGE NoMonomorphismRestriction #-}</span>
<span class=hs-linenum>14: </span>
<span class=hs-linenum>15: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>List</span> <span class='hs-layout'>(</span><span class='hs-varid'>insertSort</span><span class='hs-layout'>)</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>16: </span>
<span class=hs-linenum>17: </span><span class='hs-keyword'>{-@</span> <span class='hs-conid'>LIQUID</span> <span class='hs-str'>"--no-termination"</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>18: </span>
<span class=hs-linenum>19: </span><span class='hs-definition'>mergeSort</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span>
<span class=hs-linenum>20: </span><span class='hs-definition'>insertSort</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span>
<span class=hs-linenum>21: </span><span class='hs-definition'>slist</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>22: </span><span class='hs-definition'>slist'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-conid'>Int</span>
<span class=hs-linenum>23: </span><span class='hs-definition'>iGoUp</span><span class='hs-layout'>,</span> <span class='hs-varid'>iGoDn</span><span class='hs-layout'>,</span> <span class='hs-varid'>iDiff</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Int</span><span class='hs-keyglyph'>]</span>
<span class=hs-linenum>24: </span><span class='hs-keyword'>infixr</span> <span class='hs-varop'>`C`</span>
</pre>
</div>
Decouple Invariants From Recursive Data
=======================================
Recall: Lists
-------------
<pre><span class=hs-linenum>35: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span>
<span class=hs-linenum>36: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-varid'>a</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span>
</pre>
Recall: Refined Constructors
----------------------------
Define *increasing* Lists with strengthened constructors:
<br>
<pre><span class=hs-linenum>46: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>47: </span> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span>
<span class=hs-linenum>48: </span> <span class='hs-conid'>C</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>hd</span><span class='hs-conop'>:</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>tl</span><span class='hs-conop'>:</span> <span class='hs-conid'>L</span> <span class='hs-layout'>{</span><span class='hs-varid'>v</span><span class='hs-conop'>:</span><span class='hs-varid'>a</span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>hd</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span>
</pre>
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!
-------------------------
<pre><span class=hs-linenum>67: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>data</span> <span class='hs-conid'>L</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>></span>
<span class=hs-linenum>68: </span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>N</span>
<span class=hs-linenum>69: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>C</span> <span class='hs-layout'>(</span><span class='hs-varid'>hd</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>tl</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>hd</span><span class='hs-varop'>></span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span>
</pre>
<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
<br>
<pre><span class=hs-linenum>86: </span><span class='hs-definition'>x1</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>x2</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>x3</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>rest</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span>
</pre>
Example: Unfold Once
--------------------
<br>
<pre><span class=hs-linenum>93: </span><span class='hs-definition'>x1</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span>
<span class=hs-linenum>94: </span><span class='hs-definition'>x2</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>x3</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>rest</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span><span class='hs-varop'>></span>
</pre>
Example: Unfold Twice
---------------------
<br>
<pre><span class=hs-linenum>101: </span><span class='hs-definition'>x1</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span>
<span class=hs-linenum>102: </span><span class='hs-definition'>x2</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span><span class='hs-varop'>></span>
<span class=hs-linenum>103: </span><span class='hs-definition'>x3</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>rest</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span> <span class='hs-varop'>&&</span> <span class='hs-varid'>p</span> <span class='hs-varid'>x2</span><span class='hs-varop'>></span>
</pre>
Example: Unfold Thrice
----------------------
<br>
<pre><span class=hs-linenum>110: </span><span class='hs-definition'>x1</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span>
<span class=hs-linenum>111: </span><span class='hs-definition'>x2</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span><span class='hs-varop'>></span>
<span class=hs-linenum>112: </span><span class='hs-definition'>x3</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span> <span class='hs-varop'>&&</span> <span class='hs-varid'>p</span> <span class='hs-varid'>x2</span><span class='hs-varop'>></span>
<span class=hs-linenum>113: </span><span class='hs-definition'>rest</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>x1</span> <span class='hs-varop'>&&</span> <span class='hs-varid'>p</span> <span class='hs-varid'>x2</span> <span class='hs-varop'>&&</span> <span class='hs-varid'>p</span> <span class='hs-varid'>x3</span><span class='hs-varop'>></span>
</pre>
<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>
<pre><span class=hs-linenum>140: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>IncL</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>L</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>hd</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>hd</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
</pre>
<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...
<pre><span class=hs-linenum>155: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>slist</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>IncL</span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>156: </span><a class=annot href="#"><span class=annottext>(L <\hd2 VV -> (hd2 <= VV)> (Int))</span><span class='hs-definition'>slist</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a> <a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (6 : int))}</span><span class='hs-num'>6</span></a> <a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (12 : int))}</span><span class='hs-num'>12</span></a> <a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>(L <\_ VV -> false> {x3 : (Int) | false})</span><span class='hs-conid'>N</span></a>
</pre>
<br>
<div class="fragment">
... and protests that `slist'` is not:
<pre><span class=hs-linenum>166: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>slist'</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>IncL</span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>167: </span><a class=annot href="#"><span class=annottext>(L <\hd2 VV -> (hd2 <= VV)> (Int))</span><span class='hs-definition'>slist'</span></a> <span class='hs-keyglyph'>=</span> <span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (6 : int))}</span><span class='hs-num'>6</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (12 : int))}</span><span class='hs-num'>12</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{x10 : (Int) | (x10 > 0)}
-> (L <p> {x10 : (Int)<p x1> | (x10 > 0)})
-> (L <p> {x10 : (Int) | (x10 > 0)})</span><span class='hs-varop'>`C`</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>(L <\_ VV -> false> {x3 : (Int) | false})</span><span class='hs-conid'>N</span></a></span>
</pre>
</div>
Insertion Sort
--------------
<pre><span class=hs-linenum>175: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>insertSort</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>IncL</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>176: </span><a class=annot href="#"><span class=annottext>forall a. (Ord a) => [a] -> (L <\hd2 VV -> (hd2 <= VV)> a)</span><span class='hs-definition'>insertSort</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>(a
-> (L <\x11 VV -> (VV >= x11)> a)
-> (L <\x11 VV -> (VV >= x11)> a))
-> (L <\x11 VV -> (VV >= x11)> a)
-> [a]
-> (L <\x11 VV -> (VV >= x11)> a)</span><span class='hs-varid'>foldr</span></a> <a class=annot href="#"><span class=annottext>a -> (L <\x4 VV -> (VV >= x4)> a) -> (L <\x2 VV -> (VV >= x2)> a)</span><span class='hs-varid'>insert</span></a> <a class=annot href="#"><span class=annottext>(L <\_ VV -> false> {VV : a | false})</span><span class='hs-conid'>N</span></a>
<span class=hs-linenum>177: </span>
<span class=hs-linenum>178: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)</span><span class='hs-definition'>insert</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>y</span></a> <span class='hs-conid'>N</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV == y)}
-> (L <p> {VV : a<p x1> | (VV == y)})
-> (L <p> {VV : a | (VV == y)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>(L <\_ VV -> false> {VV : a | false})</span><span class='hs-conid'>N</span></a>
<span class=hs-linenum>179: </span><span class='hs-definition'>insert</span> <span class='hs-varid'>y</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span> <span class='hs-varop'>`C`</span> <span class='hs-varid'>xs</span><span class='hs-layout'>)</span>
<span class=hs-linenum>180: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= y)}
-> (L <p> {VV : a<p x1> | (VV >= y)})
-> (L <p> {VV : a | (VV >= y)})</span><span class='hs-varop'>`C`</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > y) && (VV >= x)}
-> (L <p> {VV : a<p x1> | (VV > y) && (VV >= x)})
-> (L <p> {VV : a | (VV > y) && (VV >= x)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>181: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= x)}
-> (L <p> {VV : a<p x1> | (VV >= x)})
-> (L <p> {VV : a | (VV >= x)})</span><span class='hs-varop'>`C`</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)</span><span class='hs-varid'>insert</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>{x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}</span><span class='hs-varid'>xs</span></a>
</pre>
<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:
<br>
<pre><span class=hs-linenum>195: </span><span class='hs-keyword'>data</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span><span class='hs-varop'>></span>
<span class=hs-linenum>196: </span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>[]</span>
<span class=hs-linenum>197: </span> <span class='hs-keyglyph'>|</span> <span class='hs-layout'>(</span><span class='hs-conop'>:</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>h</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>tl</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-varop'><</span><span class='hs-varid'>p</span> <span class='hs-varid'>h</span><span class='hs-varop'>></span><span class='hs-keyglyph'>]</span><span class='hs-varop'><</span><span class='hs-varid'>p</span><span class='hs-varop'>></span><span class='hs-layout'>)</span><span class='hs-layout'>)</span>
</pre>
Checking GHC Lists
------------------
Increasing Lists
<br>
<pre><span class=hs-linenum>208: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Incs</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span><span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>h</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>h</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>209: </span>
<span class=hs-linenum>210: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>iGoUp</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Incs</span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>211: </span><a class=annot href="#"><span class=annottext>[(Int)]<\h6 VV -> (h6 <= VV)></span><span class='hs-definition'>iGoUp</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : [{x14 : (Int) | (x14 > 0)}]<\x11 VV -> (x11 /= x12) && (x12 > 0) && (x12 > x11) && (x11 <= x12)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a><span class='hs-keyglyph'>]</span>
</pre>
Checking GHC Lists
------------------
Decreasing Lists
<br>
<pre><span class=hs-linenum>222: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Decs</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span><span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>h</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>h</span> <span class='hs-varop'>>=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>223: </span>
<span class=hs-linenum>224: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>iGoDn</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Decs</span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>225: </span><a class=annot href="#"><span class=annottext>[(Int)]<\h8 VV -> (h8 >= VV)></span><span class='hs-definition'>iGoDn</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : [{x15 : (Int) | (x15 > 0)}]<\x13 VV -> (x12 == 1) && (x13 /= x12) && (x12 > 0) && (x13 >= x12) && (x12 < x13)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-keyglyph'>]</span>
</pre>
Checking GHC Lists
------------------
Duplicate-free Lists
<br>
<pre><span class=hs-linenum>237: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>Difs</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span><span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>h</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>h</span> <span class='hs-varop'>/=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>238: </span>
<span class=hs-linenum>239: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>iDiff</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Difs</span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>240: </span><a class=annot href="#"><span class=annottext>[(Int)]<\h10 VV -> (h10 /= VV)></span><span class='hs-definition'>iDiff</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : [{x14 : (Int) | (x14 > 0)}]<\x12 VV -> (x12 /= x11) && (x11 > 0) && (x12 >= x11) && (x11 < x12)> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (1 : int))}</span><span class='hs-num'>1</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (3 : int))}</span><span class='hs-num'>3</span></a><span class='hs-layout'>,</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2 : int))}</span><span class='hs-num'>2</span></a><span class='hs-keyglyph'>]</span>
</pre>
Checking GHC Lists
------------------
Now we can check all the usual list sorting algorithms
Example: `mergeSort` [1/2]
--------------------------
<pre><span class=hs-linenum>252: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>mergeSort</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Incs</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>253: </span><a class=annot href="#"><span class=annottext>forall a. (Ord a) => [a] -> [a]<\h6 VV -> (h6 <= VV)></span><span class='hs-definition'>mergeSort</span></a> <span class='hs-conid'>[]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
{x4 : [{VV : a | false}]<p> | (((null x4)) <=> true) && ((len x4) == 0) && ((sumLens x4) == 0)}</span><span class='hs-conid'>[]</span></a>
<span class=hs-linenum>254: </span><span class='hs-definition'>mergeSort</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>x</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a><span class='hs-keyglyph'>]</span>
<span class=hs-linenum>255: </span><span class='hs-definition'>mergeSort</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x10 : [a]<\x11 VV -> (VV >= x11)> | ((len x10) >= 0)}
-> x2:{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | ((len x4) >= 0) && ((len x4) >= (len x1)) && ((len x4) >= (len x2))}</span><span class='hs-varid'>merge</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == xs1') && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs1'</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == xs2') && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs2'</span></a>
<span class=hs-linenum>256: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>257: </span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : [a] | (VV == xs1) && ((len VV) == (len xs1)) && ((len VV) >= 0) && ((len VV) >= (len xs2))}</span><span class='hs-varid'>xs1</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{VV : [a] | (VV == xs2) && ((len VV) == (len xs2)) && ((len VV) >= 0) && ((len VV) <= (len xs1)) && ((len VV) <= (len xs1))}</span><span class='hs-varid'>xs2</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x14 : [a] | ((len x14) > 0)}
-> ({x9 : [a] | ((len x9) >= 0) && ((len x9) <= (len x1))}, {x12 : [a] | ((len x12) >= 0) && ((len x12) <= (len x1))})<\x5 VV -> ((len x6) >= 0) && ((len x6) <= (len x5)) && ((len x6) <= (len x1))></span><span class='hs-varid'>split</span></a> <a class=annot href="#"><span class=annottext>{x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>xs</span></a>
<span class=hs-linenum>258: </span> <a class=annot href="#"><span class=annottext>[a]<\x2 VV -> (x2 <= VV)></span><span class='hs-varid'>xs1'</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>[a] -> [a]<\x2 VV -> (x2 <= VV)></span><span class='hs-varid'>mergeSort</span></a> <a class=annot href="#"><span class=annottext>{x7 : [a] | (x7 == xs1) && (x7 == xs1) && ((len x7) == (len xs1)) && ((len x7) >= 0) && ((len x7) >= (len xs2)) && ((sumLens x7) >= 0)}</span><span class='hs-varid'>xs1</span></a>
<span class=hs-linenum>259: </span> <a class=annot href="#"><span class=annottext>[a]<\x2 VV -> (x2 <= VV)></span><span class='hs-varid'>xs2'</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>[a] -> [a]<\x2 VV -> (x2 <= VV)></span><span class='hs-varid'>mergeSort</span></a> <a class=annot href="#"><span class=annottext>{x8 : [a] | (x8 == xs2) && (x8 == xs2) && ((len x8) == (len xs2)) && ((len x8) >= 0) && ((sumLens x8) >= 0) && ((len x8) <= (len xs1)) && ((len x8) <= (len xs1))}</span><span class='hs-varid'>xs2</span></a>
</pre>
Example: `mergeSort` [1/2]
--------------------------
<pre><span class=hs-linenum>266: </span><a class=annot href="#"><span class=annottext>forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x1 VV -> ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x1))></span><span class='hs-definition'>split</span></a> <span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-varid'>y</span><span class='hs-conop'>:</span><span class='hs-varid'>zs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x4 : [a]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x8 : [a] | (x8 == xs) && (x8 == xs) && ((len x8) == (len xs)) && ((len x8) >= 0) && ((len x8) >= (len ys)) && ((sumLens x8) >= 0) && ((len x8) <= (len zs))}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:a
-> x2:[{VV : a<p x1> | true}]<p>
-> {x4 : [a]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x9 : [a] | (x9 == ys) && (x9 == ys) && ((len x9) == (len ys)) && ((len x9) >= 0) && ((sumLens x9) >= 0) && ((len x9) <= (len xs)) && ((len x9) <= (len xs)) && ((len x9) <= (len zs))}</span><span class='hs-varid'>ys</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>267: </span> <span class='hs-keyword'>where</span>
<span class=hs-linenum>268: </span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : [a] | (VV == xs) && ((len VV) == (len xs)) && ((len VV) >= 0) && ((len VV) >= (len ys)) && ((len VV) <= (len zs))}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{VV : [a] | (VV == ys) && ((len VV) == (len ys)) && ((len VV) >= 0) && ((len VV) <= (len xs)) && ((len VV) <= (len xs)) && ((len VV) <= (len zs))}</span><span class='hs-varid'>ys</span></a><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
x1:{VV : [a] | ((len VV) >= 0)}
-> ({VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))}, {VV : [a] | ((len VV) >= 0) && ((len VV) <= (len x1))})<\x1 VV -> ((len VV) >= 0) && ((len VV) <= (len x1)) && ((len VV) <= (len x1))></span><span class='hs-varid'>split</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == zs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>zs</span></a>
<span class=hs-linenum>269: </span><span class='hs-definition'>split</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}</span><span class='hs-layout'>(</span></a><a class=annot href="#"><span class=annottext>{x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>,</span> <a class=annot href="#"><span class=annottext>{x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-conid'>[]</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>270: </span>
<span class=hs-linenum>271: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}</span><span class='hs-definition'>merge</span></a> <a class=annot href="#"><span class=annottext>{VV : [a]<\x1 VV -> (VV >= x1)> | ((len VV) >= 0)}</span><span class='hs-varid'>xs</span></a> <span class='hs-conid'>[]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
<span class=hs-linenum>272: </span><span class='hs-definition'>merge</span> <span class='hs-conid'>[]</span> <span class='hs-varid'>ys</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x3 : [a]<\x4 VV -> (VV >= x4)> | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>ys</span></a>
<span class=hs-linenum>273: </span><span class='hs-definition'>merge</span> <span class='hs-layout'>(</span><span class='hs-varid'>x</span><span class='hs-conop'>:</span><span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>y</span><span class='hs-conop'>:</span><span class='hs-varid'>ys</span><span class='hs-layout'>)</span>
<span class=hs-linenum>274: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>x1:a -> x2:a -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}</span><span class='hs-varop'><=</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV)}
-> x2:[{VV : a<p x1> | (x <= VV)}]<p>
-> {x4 : [{VV : a | (x <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}</span><span class='hs-varid'>merge</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV >= x)}]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV) && (y <= VV)}
-> x2:[{VV : a<p x1> | (x <= VV) && (y <= VV)}]<p>
-> {x4 : [{VV : a | (x <= VV) && (y <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV >= y)}]<\x5 VV -> (VV >= x5)> | (x4 == ys) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>ys</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>275: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == y)}</span><span class='hs-varid'>y</span></a> <a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= y)}
-> x2:[{VV : a<p x1> | (VV >= y)}]<p>
-> {x4 : [{VV : a | (VV >= y)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
xs:{VV : [a]<\x3 VV -> (VV >= x3)> | ((len VV) >= 0)}
-> x1:{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0) && ((len VV) >= (len x1)) && ((len VV) >= (len xs))}</span><span class='hs-varid'>merge</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == x)}</span><span class='hs-varid'>x</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > y)}
-> x2:[{VV : a<p x1> | (VV > y)}]<p>
-> {x4 : [{VV : a | (VV > y)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV >= x)}]<\x5 VV -> (VV >= x5)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV >= y)}]<\x5 VV -> (VV >= x5)> | (x4 == ys) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>ys</span></a>
</pre>
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>
<pre><span class=hs-linenum>294: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>sort</span> <span class='hs-keyglyph'>::</span> <span class='hs-layout'>(</span><span class='hs-conid'>Ord</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=></span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>a</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Incs</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
<span class=hs-linenum>295: </span><a class=annot href="#"><span class=annottext>forall a. (Ord a) => [a] -> [a]<\h6 VV -> (h6 <= VV)></span><span class='hs-definition'>sort</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x5 : [{x9 : [a]<\x10 VV -> (x10 <= VV)> | ((len x9) >= 0)}]<\_ VV -> ((len x7) >= 0)> | ((len x5) > 0)}
-> {x2 : [a]<\x3 VV -> (x3 <= VV)> | ((len x2) >= 0)}</span><span class='hs-varid'>mergeAll</span></a> <a class=annot href="#"><span class=annottext>forall <q :: [a]-> [[a]]-> Bool, p :: [[a]]-> [a]-> Bool>.
(x:{x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)> | ((len x26) > 0)}
-> {x23 : [a]<\x24 VV -> (x24 <= VV)><p x> | ((len x23) >= 0)})
-> (y:[a]
-> {x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)><q y> | ((len x26) > 0)})
-> x3:[a]
-> exists [z:{x26 : [{x30 : [a]<\x31 VV -> (x31 <= VV)> | ((len x30) >= 0)}]<\_ VV -> ((len x28) >= 0)><q x3> | ((len x26) > 0)}].{x23 : [a]<\x24 VV -> (x24 <= VV)><p z> | ((len x23) >= 0)}</span><span class='hs-varop'>.</span></a> <a class=annot href="#"><span class=annottext>[a]
-> {x2 : [{x6 : [a]<\x7 VV -> (x7 <= VV)> | ((len x6) >= 0)}]<\_ VV -> ((len x4) >= 0)> | ((len x2) > 0)}</span><span class='hs-varid'>sequences</span></a>
<span class=hs-linenum>296: </span>
<span class=hs-linenum>297: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-definition'>sequences</span></a> <span class='hs-layout'>(</span><span class='hs-varid'>a</span><span class='hs-conop'>:</span><span class='hs-varid'>b</span><span class='hs-conop'>:</span><span class='hs-varid'>xs</span><span class='hs-layout'>)</span>
<span class=hs-linenum>298: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}</span><span class='hs-varop'>`compare`</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}</span><span class='hs-varop'>==</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}</span><span class='hs-conid'>GT</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>descending</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><span class='hs-keyglyph'>]</span> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
<span class=hs-linenum>299: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>ascending</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {x4 : [{VV : a | (a <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
<span class=hs-linenum>300: </span><span class='hs-definition'>sequences</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>x</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV == a)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>x</span></a><span class='hs-keyglyph'>]</span><span class='hs-keyglyph'>]</span>
<span class=hs-linenum>301: </span><span class='hs-definition'>sequences</span> <span class='hs-conid'>[]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x6 : [{VV : a | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-conid'>[]</span></a><span class='hs-keyglyph'>]</span>
</pre>
Ex: `Data.List.sort` [2/4]
--------------------------
Juggling lists of increasing & decreasing lists
<br>
<pre><span class=hs-linenum>312: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-definition'>descending</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{VV : [{VV : a | (VV > a)}]<\x1 VV -> (VV > a) && (VV > x1)> | ((len VV) > 0)}</span><span class='hs-keyword'>as</span></a> <span class='hs-layout'>(</span><span class='hs-varid'>b</span><span class='hs-conop'>:</span><span class='hs-varid'>bs</span><span class='hs-layout'>)</span>
<span class=hs-linenum>313: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}</span><span class='hs-varop'>`compare`</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}</span><span class='hs-varop'>==</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}</span><span class='hs-conid'>GT</span></a>
<span class=hs-linenum>314: </span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> {VV : [{VV : a | (VV > a)}]<\x2 VV -> (VV > a) && (VV > x2)> | ((len VV) > 0)}
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>descending</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > b)}
-> x2:[{VV : a<p x1> | (VV > b)}]<p>
-> {x4 : [{VV : a | (VV > b)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x5 : [{VV : a | (VV > a)}]<\x6 VV -> (VV > a) && (VV > x6)> | (x5 == as) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}</span><span class='hs-keyword'>as</span></a><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == bs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>bs</span></a>
<span class=hs-linenum>315: </span><span class='hs-definition'>descending</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>as</span> <span class='hs-varid'>bs</span>
<span class=hs-linenum>316: </span> <span class='hs-keyglyph'>=</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (a <= VV)}
-> x2:[{VV : a<p x1> | (a <= VV)}]<p>
-> {x4 : [{VV : a | (a <= VV)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x5 : [{VV : a | (VV > a)}]<\x6 VV -> (VV > a) && (VV > x6)> | (x5 == as) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}</span><span class='hs-keyword'>as</span></a><span class='hs-layout'>)</span><a class=annot href="#"><span class=annottext>forall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (x16 <= VV)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>sequences</span></a> <a class=annot href="#"><span class=annottext>{x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>bs</span></a>
</pre>
Ex: `Data.List.sort` [3/4]
--------------------------
Juggling lists of increasing & decreasing lists
<br>
<pre><span class=hs-linenum>328: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-definition'>ascending</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:{VV : [{VV : a | (VV >= a)}]<\x2 VV -> (a <= VV) && (x2 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))}</span><span class='hs-keyword'>as</span></a> <span class='hs-layout'>(</span><span class='hs-varid'>b</span><span class='hs-conop'>:</span><span class='hs-varid'>bs</span><span class='hs-layout'>)</span>
<span class=hs-linenum>329: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>x1:a
-> x2:a
-> {x4 : (Ordering) | ((x4 == GHC.Types.EQ) <=> (x1 == x2)) && ((x4 == GHC.Types.GT) <=> (x1 > x2)) && ((x4 == GHC.Types.LT) <=> (x1 < x2))}</span><span class='hs-varop'>`compare`</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <a class=annot href="#"><span class=annottext>x1:(Ordering)
-> x2:(Ordering) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 /= x2))}</span><span class='hs-varop'>/=</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Ordering) | (x3 == GHC.Types.GT) && ((cmp x3) == GHC.Types.GT)}</span><span class='hs-conid'>GT</span></a>
<span class=hs-linenum>330: </span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
a:a
-> (x1:{VV : [{VV : a | (VV >= a)}]<\x3 VV -> (a <= VV) && (x3 <= VV)> | ((len VV) > 0)}
-> {VV : [a]<\x2 VV -> (x2 <= VV)> | (VV /= x1) && ((len VV) > 0) && ((len VV) > (len x1))})
-> {VV : [a] | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>ascending</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == b)}</span><span class='hs-varid'>b</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:{x7 : [{VV : a | (VV >= a) && (VV >= b)}]<\x8 VV -> (a <= VV) && (b <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}</span><span class='hs-keyglyph'>\</span></a><a class=annot href="#"><span class=annottext>{VV : [{VV : a | (VV >= a) && (VV >= b)}]<\x1 VV -> (a <= VV) && (b <= VV) && (x1 <= VV)> | ((len VV) > 0)}</span><span class='hs-varid'>ys</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}</span><span class='hs-keyword'>as</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><a class=annot href="#"><span class=annottext>forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV >= a)}
-> x2:[{VV : a<p x1> | (VV >= a)}]<p>
-> {x4 : [{VV : a | (VV >= a)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a><a class=annot href="#"><span class=annottext>{x5 : [{VV : a | (VV >= a) && (VV >= b)}]<\x6 VV -> (a <= VV) && (b <= VV) && (x6 <= VV)> | (x5 == ys) && ((len x5) > 0) && ((len x5) >= 0) && ((sumLens x5) >= 0)}</span><span class='hs-varid'>ys</span></a><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <a class=annot href="#"><span class=annottext>{x4 : [a] | (x4 == bs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>bs</span></a>
<span class=hs-linenum>331: </span><span class='hs-definition'>ascending</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>as</span> <span class='hs-varid'>bs</span>
<span class=hs-linenum>332: </span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x7 : [{VV : a | (VV >= a)}]<\x8 VV -> (a <= VV) && (x8 <= VV)> | ((len x7) > 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 /= x1) && ((len x4) > 0) && ((len x4) > (len x1))}</span><span class='hs-keyword'>as</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{VV : a | (VV == a) && (VV > b)}]<\_ VV -> false> | (((null x4)) <=> false) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{VV : a | (VV == a)}</span><span class='hs-varid'>a</span></a><span class='hs-keyglyph'>]</span><a class=annot href="#"><span class=annottext>forall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (x16 <= VV)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (x16 <= VV)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
[a]
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) > 0)}</span><span class='hs-varid'>sequences</span></a> <a class=annot href="#"><span class=annottext>{x3 : [a] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>bs</span></a>
</pre>
Ex: `Data.List.sort` [4/4]
--------------------------
Juggling lists of increasing & decreasing lists
<br>
<pre><span class=hs-linenum>343: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}</span><span class='hs-definition'>mergeAll</span></a> <span class='hs-keyglyph'>[</span><span class='hs-varid'>x</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (x5 <= VV)> | (x4 == x) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>x</span></a>
<span class=hs-linenum>344: </span><span class='hs-definition'>mergeAll</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
{VV : [{VV : [a]<\x2 VV -> (x2 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}</span><span class='hs-varid'>mergeAll</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:{x10 : [{x14 : [a]<\x15 VV -> (VV >= x15)> | ((len x14) >= 0)}]<\_ VV -> ((len x12) >= 0)> | ((len x10) >= 0)}
-> {x3 : [{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | ((len x3) >= 0) && ((len x3) <= (len x1))}</span><span class='hs-varid'>mergePairs</span></a> <a class=annot href="#"><span class=annottext>{x3 : [{x7 : [a]<\x8 VV -> (x8 <= VV)> | ((len x7) >= 0)}]<\_ VV -> ((len x5) >= 0)> | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-varid'>xs</span></a><span class='hs-layout'>)</span>
<span class=hs-linenum>345: </span>
<span class=hs-linenum>346: </span><a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}</span><span class='hs-definition'>mergePairs</span></a> <span class='hs-layout'>(</span><span class='hs-varid'>a</span><span class='hs-conop'>:</span><span class='hs-varid'>b</span><span class='hs-conop'>:</span><span class='hs-varid'>xs</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x10 : [a]<\x11 VV -> (VV >= x11)> | ((len x10) >= 0)}
-> x2:{x7 : [a]<\x8 VV -> (VV >= x8)> | ((len x7) >= 0)}
-> {x4 : [a]<\x5 VV -> (x5 <= VV)> | ((len x4) >= 0) && ((len x4) >= (len x1)) && ((len x4) >= (len x2))}</span><span class='hs-varid'>merge</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == a) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>a</span></a> <a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == b) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>b</span></a><a class=annot href="#"><span class=annottext>forall <p :: [a]-> [a]-> Bool>.
x1:{x15 : [a]<\x16 VV -> (VV >= x16)> | ((len x15) >= 0)}
-> x2:[{x15 : [a]<\x16 VV -> (VV >= x16)><p x1> | ((len x15) >= 0)}]<p>
-> {x4 : [{x15 : [a]<\x16 VV -> (VV >= x16)> | ((len x15) >= 0)}]<p> | (((null x4)) <=> false) && ((len x4) == (1 + (len x2))) && ((sumLens x4) == ((len x1) + (sumLens x2)))}</span><span class='hs-conop'>:</span></a> <a class=annot href="#"><span class=annottext>forall a.
(Ord a) =>
x1:{VV : [{VV : [a]<\x2 VV -> (VV >= x2)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0)}
-> {VV : [{VV : [a]<\x1 VV -> (x1 <= VV)> | ((len VV) >= 0)}]<\_ VV -> ((len VV) >= 0)> | ((len VV) >= 0) && ((len VV) <= (len x1))}</span><span class='hs-varid'>mergePairs</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{x8 : [a]<\x9 VV -> (VV >= x9)> | ((len x8) >= 0)}]<\_ VV -> ((len x6) >= 0)> | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a>
<span class=hs-linenum>347: </span><span class='hs-definition'>mergePairs</span> <span class='hs-keyglyph'>[</span><span class='hs-varid'>x</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x6 : [{x8 : [{VV : a | false}]<\_ VV -> false> | false}]<\_ VV -> false> | (((null x6)) <=> true) && ((len x6) == 0) && ((sumLens x6) == 0) && ((len x6) >= 0) && ((sumLens x6) >= 0)}</span><span class='hs-keyglyph'>[</span></a><a class=annot href="#"><span class=annottext>{x4 : [a]<\x5 VV -> (VV >= x5)> | (x4 == a) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>x</span></a><span class='hs-keyglyph'>]</span>
<span class=hs-linenum>348: </span><span class='hs-definition'>mergePairs</span> <span class='hs-conid'>[]</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>forall <p :: [a]-> [a]-> Bool>.
{x4 : [{x6 : [{VV : a | false}]<\_ VV -> false> | false}]<p> | (((null x4)) <=> true) && ((len x4) == 0) && ((sumLens x4) == 0)}</span><span class='hs-conid'>[]</span></a>
</pre>
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>
<pre><span class=hs-linenum>371: </span><span class='hs-keyword'>data</span> <span class='hs-conid'>Map</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Tip</span>
<span class=hs-linenum>372: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>Bin</span> <span class='hs-conid'>Size</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-layout'>(</span><span class='hs-conid'>Map</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-conid'>Map</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span>
<span class=hs-linenum>373: </span>
<span class=hs-linenum>374: </span><span class='hs-keyword'>type</span> <span class='hs-conid'>Size</span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Int</span>
</pre>
</div>
Two Abstract Refinements
------------------------
- `l` : relates root `key` with `left`-subtree keys
- `r` : relates root `key` with `right`-subtree keys
<pre><span class=hs-linenum>385: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>data</span> <span class='hs-conid'>Map</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-varop'><</span> <span class='hs-varid'>l</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>k</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>k</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span>
<span class=hs-linenum>386: </span> <span class='hs-layout'>,</span> <span class='hs-varid'>r</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>k</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>k</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Prop</span> <span class='hs-varop'>></span>
<span class=hs-linenum>387: </span> <span class='hs-keyglyph'>=</span> <span class='hs-conid'>Tip</span>
<span class=hs-linenum>388: </span> <span class='hs-keyglyph'>|</span> <span class='hs-conid'>Bin</span> <span class='hs-layout'>(</span><span class='hs-varid'>sz</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Size</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>key</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>k</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>val</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span>
<span class=hs-linenum>389: </span> <span class='hs-layout'>(</span><span class='hs-varid'>left</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Map</span> <span class='hs-varop'><</span><span class='hs-varid'>l</span><span class='hs-layout'>,</span><span class='hs-varid'>r</span><span class='hs-varop'>></span> <span class='hs-layout'>(</span><span class='hs-varid'>k</span><span class='hs-varop'><</span><span class='hs-varid'>l</span> <span class='hs-varid'>key</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span>
<span class=hs-linenum>390: </span> <span class='hs-layout'>(</span><span class='hs-varid'>right</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Map</span> <span class='hs-varop'><</span><span class='hs-varid'>l</span><span class='hs-layout'>,</span><span class='hs-varid'>r</span><span class='hs-varop'>></span> <span class='hs-layout'>(</span><span class='hs-varid'>k</span><span class='hs-varop'><</span><span class='hs-varid'>r</span> <span class='hs-varid'>key</span><span class='hs-varop'>></span><span class='hs-layout'>)</span> <span class='hs-varid'>a</span><span class='hs-layout'>)</span> <span class='hs-keyword'>@-}</span>
</pre>
Ex: Binary Search Trees
-----------------------
Keys are *Binary-Search* Ordered
<br>
<pre><span class=hs-linenum>402: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>BST</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span>
<span class=hs-linenum>403: </span> <span class='hs-conid'>Map</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>v</span> <span class='hs-varop'><</span> <span class='hs-varid'>r</span> <span class='hs-layout'>}</span><span class='hs-layout'>,</span>
<span class=hs-linenum>404: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>v</span> <span class='hs-varop'>></span> <span class='hs-varid'>r</span> <span class='hs-layout'>}</span><span class='hs-varop'>></span>
<span class=hs-linenum>405: </span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
</pre>
Ex: Minimum Heaps
-----------------
Root contains *minimum* value
<br>
<pre><span class=hs-linenum>416: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>MinHeap</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span>
<span class=hs-linenum>417: </span> <span class='hs-conid'>Map</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>r</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span>
<span class=hs-linenum>418: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>r</span> <span class='hs-varop'><=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span>
<span class=hs-linenum>419: </span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
</pre>
Ex: Maximum Heaps
-----------------
Root contains *maximum* value
<br>
<pre><span class=hs-linenum>430: </span><span class='hs-keyword'>{-@</span> <span class='hs-keyword'>type</span> <span class='hs-conid'>MaxHeap</span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyglyph'>=</span>
<span class=hs-linenum>431: </span> <span class='hs-conid'>Map</span> <span class='hs-varop'><</span><span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>r</span> <span class='hs-varop'>>=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-layout'>,</span>
<span class=hs-linenum>432: </span> <span class='hs-layout'>{</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>r</span> <span class='hs-varid'>v</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>r</span> <span class='hs-varop'>>=</span> <span class='hs-varid'>v</span><span class='hs-layout'>}</span><span class='hs-varop'>></span>
<span class=hs-linenum>433: </span> <span class='hs-varid'>k</span> <span class='hs-varid'>a</span> <span class='hs-keyword'>@-}</span>
</pre>
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>