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>