{#laziness} ============ <div class="hidden"> <pre><span class=hs-linenum>6: </span><span class='hs-keyword'>module</span> <span class='hs-conid'>Laziness</span> <span class='hs-keyword'>where</span> <span class=hs-linenum>7: </span><span class='hs-keyword'>import</span> <span class='hs-conid'>Language</span><span class='hs-varop'>.</span><span class='hs-conid'>Haskell</span><span class='hs-varop'>.</span><span class='hs-conid'>Liquid</span><span class='hs-varop'>.</span><span class='hs-conid'>Prelude</span> <span class=hs-linenum>8: </span> <span class=hs-linenum>9: </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>10: </span> <span class=hs-linenum>11: </span><span class='hs-definition'>divide</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> <span class=hs-linenum>12: </span><span class='hs-definition'>foo</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-linenum>13: </span><span class='hs-comment'>-- zero :: Int </span> <span class=hs-linenum>14: </span><span class='hs-comment'>-- diverge :: a -> b</span> </pre> </div> Lazy Evaluation? ---------------- Lazy Evaluation =============== SMT based Verification ---------------------- Techniques developed for *strict* languages <br> <div class="fragment"> ----------------------- --- ------------------------------------------ **Floyd-Hoare** : `ESCJava`, `SpecSharp` ... **Model Checkers** : `Slam`, `Blast` ... **Refinement Types** : `DML`, `Stardust`, `F7`, `F*`, `Sage` ... ----------------------- --- ------------------------------------------ </div> <br> <div class="fragment"> Surely soundness carries over to Haskell, right? </div> Back To the Beginning --------------------- <pre><span class=hs-linenum>53: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>divide</span> <span class='hs-keyglyph'>::</span> <span class='hs-conid'>Int</span> <span class='hs-keyglyph'>-></span> <span class='hs-keyword'>{v:</span><span class='hs-conid'>Int</span><span class='hs-keyword'>| v /= 0}</span> <span class='hs-keyglyph'>-></span> <span class='hs-conid'>Int</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>54: </span><a class=annot href="#"><span class=annottext>(Int) -> {VV : (Int) | (VV /= 0)} -> (Int)</span><span class='hs-definition'>divide</span></a> <a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-varid'>n</span></a> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : [(Char)] | false} -> {x1 : (Int) | false}</span><span class='hs-varid'>liquidError</span></a> <a class=annot href="#"><span class=annottext>{x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}</span><span class='hs-str'>"div-by-zero!"</span></a> <span class=hs-linenum>55: </span><span class='hs-definition'>divide</span> <span class='hs-varid'>n</span> <span class='hs-varid'>d</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == n)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x6 : (Int) | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}</span><span class='hs-varop'>`div`</span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 /= 0)}</span><span class='hs-varid'>d</span></a> </pre> <br> <div class="fragment"> Should only try to `divide` by non-zero values </div> An Innocent Function -------------------- `foo` returns a value *strictly less than* input. <br> <pre><span class=hs-linenum>72: </span><span class='hs-keyword'>{-@</span> <span class='hs-varid'>foo</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-keyword'>{v:</span><span class='hs-conid'>Nat</span> <span class='hs-keyword'>| v < n}</span> <span class='hs-keyword'>@-}</span> <span class=hs-linenum>73: </span><a class=annot href="#"><span class=annottext>n:{VV : (Int) | (VV >= 0)} -> {VV : (Int) | (VV >= 0) && (VV < n)}</span><span class='hs-definition'>foo</span></a> <a class=annot href="#"><span class=annottext>{VV : (Int) | (VV >= 0)}</span><span class='hs-varid'>n</span></a> <span class=hs-linenum>74: </span> <span class='hs-keyglyph'>|</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>x1:{x8 : (Int) | (x8 >= 0) && (x8 <= n)} -> x2:{x8 : (Int) | (x8 >= 0) && (x8 <= n)} -> {x2 : (Bool) | (((Prop x2)) <=> (x1 > x2))}</span><span class='hs-varop'>></span></a> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> <a class=annot href="#"><span class=annottext>x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}</span><span class='hs-comment'>-</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-linenum>75: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>x1:{x5 : (Int) | (x5 >= 0)} -> {x3 : (Int) | (x3 >= 0) && (x3 < x1)}</span><span class='hs-varid'>foo</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == n) && (x3 >= 0)}</span><span class='hs-varid'>n</span></a> </pre> LiquidHaskell Lies! ------------------- <pre><span class=hs-linenum>82: </span><a class=annot href="#"><span class=annottext>(Int)</span><span class='hs-definition'>explode</span></a> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>let</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-varid'>z</span></a> <span class='hs-keyglyph'>=</span> <a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (0 : int))}</span><span class='hs-num'>0</span></a> <span class=hs-linenum>83: </span> <span class='hs-keyword'>in</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x:{VV : (Int) | (VV == 0) && (VV == 1) && (VV == Laziness.explode) && (VV == z) && (VV > 0) && (VV > Laziness.explode) && (VV > z) && (VV < 0) && (VV < Laziness.explode) && (VV < z)} -> {VV : (Int) | (VV == 0) && (VV == 1) && (VV == Laziness.explode) && (VV == x) && (VV == z) && (VV > 0) && (VV > Laziness.explode) && (VV > x) && (VV > z) && (VV < 0) && (VV < Laziness.explode) && (VV < x) && (VV < z)}</span><span class='hs-keyglyph'>\</span></a><a class=annot href="#"><span class=annottext>{VV : (Int) | (VV == 0) && (VV == 1) && (VV == Laziness.explode) && (VV == z) && (VV > 0) && (VV > Laziness.explode) && (VV > z) && (VV < 0) && (VV < Laziness.explode) && (VV < z)}</span><span class='hs-varid'>x</span></a> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>{x2 : (Int) | (x2 == (2013 : int))}</span><span class='hs-num'>2013</span></a> <a class=annot href="#"><span class=annottext>(Int) -> {x3 : (Int) | (x3 /= 0)} -> (Int)</span><span class='hs-varop'>`divide`</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == z) && (x3 == (0 : int))}</span><span class='hs-varid'>z</span></a><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><a class=annot href="#"><span class=annottext>x1:{x5 : (Int) | (x5 >= 0)} -> {x3 : (Int) | (x3 >= 0) && (x3 < x1)}</span><span class='hs-varid'>foo</span></a> <a class=annot href="#"><span class=annottext>{x3 : (Int) | (x3 == z) && (x3 == (0 : int))}</span><span class='hs-varid'>z</span></a><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> Why is this deemed *safe*? </div> <br> <div class="fragment"> (Where's the *red* highlight when you want it?) </div> Safe With Eager Eval -------------------- <div/> <pre><span class=hs-linenum>103: </span><span class='hs-comment'>{- foo :: n:Nat -> {v:Nat | v < n} -}</span> <span class=hs-linenum>104: </span><span class='hs-definition'>foo</span> <span class='hs-varid'>n</span> <span class=hs-linenum>105: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>n</span> <span class='hs-varop'>></span> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>n</span> <span class='hs-comment'>-</span> <span class='hs-num'>1</span> <span class=hs-linenum>106: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>foo</span> <span class='hs-varid'>n</span> <span class=hs-linenum>107: </span> <span class=hs-linenum>108: </span><span class='hs-definition'>explode</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>let</span> <span class='hs-varid'>z</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span> <span class=hs-linenum>109: </span> <span class='hs-keyword'>in</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>x</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-num'>2013</span> <span class='hs-varop'>`divide`</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>foo</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> </pre> <br> <div class="fragment"> In Java, ML, etc: program spins away, *never hits* divide-by-zero </div> Unsafe With Lazy Eval --------------------- <div/> <pre><span class=hs-linenum>122: </span><span class='hs-comment'>{- foo :: n:Nat -> {v:Nat | v < n} -}</span> <span class=hs-linenum>123: </span><span class='hs-definition'>foo</span> <span class='hs-varid'>n</span> <span class=hs-linenum>124: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>n</span> <span class='hs-varop'>></span> <span class='hs-num'>0</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>n</span> <span class='hs-comment'>-</span> <span class='hs-num'>1</span> <span class=hs-linenum>125: </span> <span class='hs-keyglyph'>|</span> <span class='hs-varid'>otherwise</span> <span class='hs-keyglyph'>=</span> <span class='hs-varid'>foo</span> <span class='hs-varid'>n</span> <span class=hs-linenum>126: </span> <span class=hs-linenum>127: </span><span class='hs-definition'>explode</span> <span class='hs-keyglyph'>=</span> <span class='hs-keyword'>let</span> <span class='hs-varid'>z</span> <span class='hs-keyglyph'>=</span> <span class='hs-num'>0</span> <span class=hs-linenum>128: </span> <span class='hs-keyword'>in</span> <span class='hs-layout'>(</span><span class='hs-keyglyph'>\</span><span class='hs-varid'>x</span> <span class='hs-keyglyph'>-></span> <span class='hs-layout'>(</span><span class='hs-num'>2013</span> <span class='hs-varop'>`divide`</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span><span class='hs-layout'>)</span> <span class='hs-layout'>(</span><span class='hs-varid'>foo</span> <span class='hs-varid'>z</span><span class='hs-layout'>)</span> </pre> <br> In Haskell, program *skips* `(foo z)` & hits divide-by-zero! Problem: Divergence ------------------- <div class="fragment"> What is denoted by `e :: {v:Int | 0 <= v}` ? </div> <br> <div class="fragment"> `e` evaluates to a `Nat` </div> <div class="fragment"> or **diverges**! </div> <div class="fragment"> <br> Classical Floyd-Hoare notion of [partial correctness](http://en.wikipedia.org/wiki/Hoare_logic#Partial_and_total_correctness) </div> Problem: Divergence ------------------- Suppose `e :: {v:Int | 0 <= v}` <br> **Consider** `let x = e in body` With Eager Evaluation --------------------- Suppose `e :: {v:Int | 0 <= v}` <br> **Consider** `let x = e in body` <br> <div class="fragment"> **Can** assume `x` is a `Nat` when checking `body` </div> But With Lazy Evaluation ------------------------ Suppose `e :: {v:Int | 0 <= v}` <br> **Consider** `let x = e in body` <br> <div class="fragment"> **Cannot** assume `x` is a `Nat` when checking e! </div> Oops. Now what? --------------- **Solution** Only assign *non-trivial* refinements to *non-diverging* terms! <br> <div class="fragment"> **Require A Termination Analysis** (Oh dear.) </div> <a href="http://goto.ucsd.edu:8090/index.html#?demo=TellingLies.hs" target="_blank">Demo:</a>Disable `"--no-termination" and see what happens! Recap ----- 1. **Refinements:** Types + Predicates 2. **Subtyping:** SMT Implication 3. **Measures:** Strengthened Constructors 4. **Abstract Refinements:* Decouple Invariants 5. **Lazy Evaluation:** Requires Termination 6. <div class="fragment">**Termination:** Via Refinements!</div>