content:  {#laziness}
  ============
  
  <div class="hidden">
  \begin{code}
  module Laziness where
  
  import Language.Haskell.Liquid.Prelude
  
  {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short"          @-}
  
  
  safeDiv :: Int -> Int -> Int
  foo     :: Int -> Int
  -- zero    :: Int
  -- diverge :: a -> b
  \end{code}
  </div>
  
  
  Lazy Evaluation?
  ----------------
  
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  <br>
  
  
  [[Skip]](11_Evaluation.lhs.slides.html)
  
  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`, `Sage`, `F7`, `F*`, ...
  -----------------------   ---   ------------------------------------------
  
  </div>
  
  <br>
  
  <div class="fragment">
  Surely soundness carries over to Haskell, right?
  </div>
  
  
  Back To the Beginning
  ---------------------
  
  \begin{code}
  {-@ safeDiv :: Int -> {v:Int|v /= 0} -> Int @-}
  safeDiv n 0 = liquidError "div-by-zero!"
  safeDiv n d = n `div` d
  \end{code}
  
  <br>
  
  <div class="fragment">
  Should only call `safeDiv` with **non-zero** values
  </div>
  
  An Innocent Function
  --------------------
  
  `foo` returns a value **strictly less than** input.
  
  <br>
  
  \begin{code} <div/>
  {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
  foo n
    | n > 0     = n - 1
    | otherwise = foo n
  \end{code}
  
  LiquidHaskell Lies!
  -------------------
  
  \begin{code}
  {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
  foo n
    | n > 0     = n - 1
    | otherwise = foo n
  
  explode = let z = 0
                a = foo z
            in
                (\x -> 2013 `safeDiv` z) a
  \end{code}
  
  <br>
  
  <div class="fragment">
  Why is this program **deemed safe**?!
  </div>
  
  
  *Safe* With Eager Eval
  ----------------------
  
  \begin{code} <div/>
  {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
  foo n
    | n > 0     = n - 1
    | otherwise = foo n
  
  explode = let z = 0     -- :: {v:Int| v = 0}
                a = foo z -- :: {v:Nat| v < z}
            in
                (\x -> 2013 `safeDiv` z) a
  \end{code}
  
  <br>
  
  <div class="fragment">
  **Safe** in Java, ML: program spins away, **never hits** divide-by-zero
  </div>
  
  *Unsafe* With Lazy Eval
  -----------------------
  
  \begin{code} <div/>
  {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
  foo n
    | n > 0     = n - 1
    | otherwise = foo n
  
  explode = let z = 0     -- :: {v:Int| v = 0}
                a = foo z -- :: {v:Nat| v < z}
            in
                (\x -> 2013 `safeDiv` z) a
  \end{code}
  
  <br>
  
  **Unsafe** in Haskell: program skips `foo z` and **hits** divide-by-zero!
  
  Problem: Divergence
  -------------------
  
  What is denoted by:
  
  `e :: {v:Int | P}`
  
  
  <br>
  
  <div class="fragment">
  `e` evaluates to `Int` satisfying `P`
  </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
  -------------------
  
  \begin{code} **Consider** <div/>
          {-@ e :: {v : Int | P} @-}
  
          let x = e in body
  \end{code}
  
  <br>
  
  <div class="fragment">
  **Eager Evaluation**
  
  *Can* assume `P(x)` when checking `body`
  </div>
  
  <br>
  
  <div class="fragment">
  **Lazy Evaluation**
  
  *Cannot* assume `P(x)` when checking `body`
  </div>
  
  Eager vs. Lazy Binders
  ----------------------
  
  \begin{code} <div/>
  {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
  foo n
    | n > 0     = n - 1
    | otherwise = foo n
  
  explode = let z = 0     -- :: {v:Int| v = 0}
                a = foo z -- :: {v:Nat| v < z}
            in
                (\x -> 2013 `safeDiv` z) a
  \end{code}
  
  <br>
  
  Inconsistent refinement for `a` is sound for **eager**, unsound for **lazy**
  
  
  Panic! Now what?
  ---------------
  
  <div class="fragment">
  **Solution**
  
  Assign *non-trivial* refinements to *non-diverging* terms!
  </div>
  
  <br>
  
  <div class="fragment">
  
  **Require A Termination Analysis**
  
  Don't worry, its easy...
  
  </div>
  
  <br>
  
  <div class="fragment">
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=TellingLies.hs" target="_blank">Demo:</a> &nbsp; Disable `"--no-termination"` and see what happens!
  </div>
  
  Recap
  -----
  
  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Strengthened Constructors
  4. Abstract: Refinements over functions and data
  5. **Lazy Evaluation:** Requires Termination
  6. <div class="fragment">**Termination:** via Refinements!</div>
  
  <br>
  <br>
  
  <div class="fragment">[[continue...]](10_Termination.lhs.slides.html)</div>
  