{#hofs} ========= <div class="hidden"> <pre><span class=hs-linenum> 6: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Loop</span> <span class='hs-layout'>(</span> <span class=hs-linenum> 7: </span> <span class='hs-varid'>listSum</span> <span class=hs-linenum> 8: </span> <span class='hs-layout'>,</span> <span class='hs-varid'>listNatSum</span> <span class=hs-linenum> 9: </span> <span class='hs-layout'>)</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>10: </span> <span class=hs-linenum>11: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Prelude</span> <span class=hs-linenum>12: </span> <span class=hs-linenum>13: </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>14: </span><span class='hs-definition'>listNatSum</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-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class=hs-linenum>15: </span><span class='hs-definition'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> </pre> </div> Higher-Order Specifications --------------------------- Types scale to *Higher-Order* Specifications <br> <div class="fragment"> + map + fold + visitors + callbacks + ... </div> <br> <div class="fragment">Very difficult with *first-order program logics*</div> Higher Order Specifications =========================== Example: Higher Order Loop -------------------------- <pre><span class=hs-linenum>48: </span><span class='hs-definition'>loop</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span><span class='hs-layout'>)</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>α</span> <span class=hs-linenum>49: </span><a class=annot href="#"><span class=annottext>forall a. lo:{VV : (Int) | (VV == 0) && (VV >= 0)} -> hi:{VV : (Int) | (VV >= 0) && (VV >= lo)} -> a -> ({VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a) -> a</span><span class='hs-definition'>loop</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == 0) && (VV >= 0)}</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo)}</span><span class='hs-varid'>hi</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>base</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a</span><span class='hs-varid'>f</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == 0) && (x4 == lo) && (x4 >= 0)}</span><span class='hs-varid'>lo</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == base)}</span><span class='hs-varid'>base</span></a> <span class=hs-linenum>50: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>51: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>acc</span></a> <span class=hs-linenum>52: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)} -> x2:{x12 : (Int) | (x12 >= 0) && (x12 >= i) && (x12 >= lo) && (x12 <= hi)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}</span><span class='hs-varop'><</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == hi) && (x4 >= 0) && (x4 >= lo)}</span><span class='hs-varid'>hi</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> a</span><span class='hs-varid'>go</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</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> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 >= 0) && (x4 >= lo) && (x4 < hi)} -> a -> a</span><span class='hs-varid'>f</span></a> <a class=annot href="#"><span class=annottext>{x5 : (Int) | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : a | (VV == acc)}</span><span class='hs-varid'>acc</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>53: </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 == acc)}</span><span class='hs-varid'>acc</span></a> </pre> <br> LiquidHaskell infers `f` called with values `(Btwn lo hi)` Example: Summing Lists ---------------------- <pre><span class=hs-linenum>65: </span><a class=annot href="#"><span class=annottext>forall a. (Num a) => [a] -> a</span><span class='hs-definition'>listSum</span></a> <a class=annot href="#"><span class=annottext>[a]</span><span class='hs-varid'>xs</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x12 : (Int) | (x12 == 0) && (x12 >= 0)} -> x2:{x9 : (Int) | (x9 >= 0) && (x9 >= x1)} -> a -> ({x6 : (Int) | (x6 >= 0) && (x6 >= x1) && (x6 < x2)} -> a -> a) -> a</span><span class='hs-varid'>loop</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 == (len xs))}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 >= 0) && (x3 < n)} -> a -> a</span><span class='hs-varid'>body</span></a> <span class=hs-linenum>66: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>67: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)} -> a -> a</span><span class='hs-varid'>body</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>a</span><span class='hs-varid'>acc</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{VV : a | (VV == acc)}</span><span class='hs-varid'>acc</span></a> <a class=annot href="#"><span class=annottext>x1:a -> x2:a -> {VV : a | (VV == (x1 + x2))}</span><span class='hs-varop'>+</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> <a class=annot href="#"><span class=annottext>x1:[a] -> {x3 : (Int) | (x3 < (len x1)) && (0 <= x3)} -> a</span><span class='hs-varop'>!!</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>68: </span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (len xs))}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:[a] -> {x2 : (Int) | (x2 == (len x1))}</span><span class='hs-varid'>length</span></a> <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> </pre> <br> - <div class="fragment">*Function subtyping:* `body` called on `i :: Btwn 0 (llen xs)`</div> - <div class="fragment">Hence, indexing with `!!` is safe.</div> <div class="fragment"> <a href="http://goto.ucsd.edu:8090/index.html#?demo=Loop.hs" target= "_blank">Demo:</a> Tweak `loop` exit condition? </div> Example: Summing `Nat`s ----------------------- <br> <pre><span class=hs-linenum>87: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>88: </span><a class=annot href="#"><span class=annottext>[{VV : (Int) | (VV >= 0)}] -> {VV : (Int) | (VV >= 0)}</span><span class='hs-definition'>listNatSum</span></a> <a class=annot href="#"><span class=annottext>[{VV : (Int) | (VV >= 0)}]</span><span class='hs-varid'>xs</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x20 : (Int) | (x20 == 0) && (x20 >= 0)} -> x2:{x17 : (Int) | (x17 >= 0) && (x17 >= x1)} -> {x14 : (Int) | (x14 >= 0)} -> ({x12 : (Int) | (x12 >= 0) && (x12 >= x1) && (x12 < x2)} -> {x14 : (Int) | (x14 >= 0)} -> {x14 : (Int) | (x14 >= 0)}) -> {x14 : (Int) | (x14 >= 0)}</span><span class='hs-varid'>loop</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 == (len xs))}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <a class=annot href="#"><span class=annottext>{x8 : (Int) | (x8 >= 0) && (x8 < n)} -> x2:{x5 : (Int) | (x5 >= 0)} -> {x3 : (Int) | (x3 >= 0) && (x3 >= x2)}</span><span class='hs-varid'>body</span></a> <span class=hs-linenum>89: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>90: </span> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)} -> acc:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0) && (VV >= acc)}</span><span class='hs-varid'>body</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-varid'>i</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>acc</span></a> <span class='hs-keyglyph'>-></span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == acc) && (x3 >= 0)}</span><span class='hs-varid'>acc</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</span></a> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a> <a class=annot href="#"><span class=annottext>x1:[{x9 : (Int) | (x9 >= 0)}] -> {x5 : (Int) | (x5 < (len x1)) && (0 <= x5)} -> {x9 : (Int) | (x9 >= 0)}</span><span class='hs-varop'>!!</span></a> <a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 < n)}</span><span class='hs-varid'>i</span></a><span class='hs-layout'>)</span> <span class=hs-linenum>91: </span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (len xs))}</span><span class='hs-varid'>n</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:[{x6 : (Int) | (x6 >= 0)}] -> {x2 : (Int) | (x2 == (len x1))}</span><span class='hs-varid'>length</span></a> <a class=annot href="#"><span class=annottext>{x4 : [{x7 : (Int) | (x7 >= 0)}] | (x4 == xs) && ((len x4) >= 0) && ((sumLens x4) >= 0)}</span><span class='hs-varid'>xs</span></a> </pre> <br> <div class="fragment" align="center"> ---- ---- --------------------------------------- (+) `::` `x:Int -> y:Int -> {v:Int| v=x+y}` `<:` `Nat -> Nat -> Nat` ---- ---- --------------------------------------- </div> Example: Summing `Nat`s ----------------------- <br> <pre><span class=hs-linenum>109: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>110: </span><span class='hs-definition'>listNatSum</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>n</span> <span class='hs-num'>0</span> <span class='hs-varid'>body</span> <span class=hs-linenum>111: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>112: </span> <span class='hs-varid'>body</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>acc</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span> <span class='hs-varop'>!!</span> <span class='hs-varid'>i</span><span class='hs-layout'>)</span> <span class=hs-linenum>113: </span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>length</span> <span class='hs-varid'>xs</span> </pre> <br> Hence, verified by *instantiating* `α` of `loop` with `Nat` <div class="fragment">`Int -> Int -> Nat -> (Int -> Nat -> Nat) -> Nat`</div> Example: Summing `Nat`s ----------------------- <br> <pre><span class=hs-linenum>126: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>listNatSum</span> <span class='hs-keyglyph'>::</span> <span class='hs-keyglyph'>[</span><span class='hs-conid'>Nat</span><span class='hs-keyglyph'>]</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Nat</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>127: </span><span class='hs-definition'>listNatSum</span> <span class='hs-varid'>xs</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>loop</span> <span class='hs-num'>0</span> <span class='hs-varid'>n</span> <span class='hs-num'>0</span> <span class='hs-varid'>body</span> <span class=hs-linenum>128: </span> <span class='hs-keyword'>where</span> <span class=hs-linenum>129: </span> <span class='hs-varid'>body</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyglyph'>\</span><span class='hs-varid'>i</span> <span class='hs-varid'>acc</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>acc</span> <span class='hs-varop'>+</span> <span class='hs-layout'>(</span><span class='hs-varid'>xs</span> <span class='hs-varop'>!!</span> <span class='hs-varid'>i</span><span class='hs-layout'>)</span> <span class=hs-linenum>130: </span> <span class='hs-varid'>n</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>length</span> <span class='hs-varid'>xs</span> </pre> <br> + Parameter `α` corresponds to *loop invariant* + Instantiation corresponds to invariant *synthesis* Instantiation And Inference --------------------------- + <div class="fragment">Polymorphic instantiation happens *everywhere*</div> + <div class="fragment">Automatic inference is crucial</div> + <div class="fragment">*Cannot use* unification (unlike indexed approaches)</div> + <div class="fragment">*Can reuse* [SMT/predicate abstraction.](http://goto.ucsd.edu/~rjhala/papers/liquid_types.html)</div> Iteration Dependence -------------------- **Cannot** use parametric polymorphism to verify: <br> <pre><span class=hs-linenum>161: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>add</span> <span class='hs-keyglyph'>::</span> <span class='hs-varid'>n</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-varid'>m</span><span class='hs-conop'>:</span><span class='hs-conid'>Nat</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Nat</span><span class='hs-keyword'>|v=m+n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>162: </span><a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= 0)} -> m:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV == (m + n)) && (VV >= 0)}</span><span class='hs-definition'>add</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>m</span></a> <span class='hs-keyglyph'>=</span> <span class=hs-error><a class=annot href="#"><span class=annottext>x1:{x24 : (Int) | (x24 == 0) && (x24 >= 0)} -> x2:{x21 : (Int) | (x21 >= 0) && (x21 >= x1)} -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)} -> ({x15 : (Int) | (x15 >= 0) && (x15 >= x1) && (x15 < x2)} -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)} -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}) -> {x18 : (Int) | (x18 >= 0) && (x18 >= n)}</span><span class='hs-varid'>loop</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == m) && (x3 >= 0)}</span><span class='hs-varid'>m</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a></span><span class=hs-error> </span><span class=hs-error><span class='hs-layout'>(</span></span><span class=hs-error><a class=annot href="#"><span class=annottext>{x11 : (Int) | (x11 >= 0) && (x11 < m)} -> x2:{x8 : (Int) | (x8 >= 0) && (x8 >= n)} -> {x5 : (Int) | (x5 > 0) && (x5 > x2) && (x5 > n) && (x5 >= 0)}</span><span class='hs-keyglyph'>\</span></a></span><span class=hs-error><span class='hs-keyword'>_</span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0) && (VV >= n)}</span><span class='hs-varid'>i</span></a></span><span class=hs-error> </span><span class=hs-error><span class='hs-keyglyph'>-></span></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>{x4 : (Int) | (x4 == i) && (x4 >= 0) && (x4 >= n)}</span><span class='hs-varid'>i</span></a></span><span class=hs-error> </span><span class=hs-error><a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}</span><span class='hs-varop'>+</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 class='hs-layout'>)</span></span> </pre> <br> - <div class="fragment">As property only holds after **last** loop iteration...</div> - <div class="fragment">... cannot instantiate `α` with `{v:Int | v = n + m}`</div> <div class="fragment">**Problem:** Need *iteration-dependent* invariants...</div>