{#laziness} ============ Lazy Evaluation? ----------------










[[Skip]](11_Evaluation.lhs.slides.html) Lazy Evaluation =============== SMT based Verification ---------------------- Techniques developed for **strict** languages
----------------------- --- ------------------------------------------ **Floyd-Hoare** : `ESCJava`, `SpecSharp` ... **Model Checkers** : `Slam`, `Blast` ... **Refinement Types** : `DML`, `Stardust`, `Sage`, `F7`, `F*`, ... ----------------------- --- ------------------------------------------

Surely soundness carries over to Haskell, right?
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}
Should only call `safeDiv` with **non-zero** values
An Innocent Function -------------------- `foo` returns a value **strictly less than** input.
\begin{code}
{-@ 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}
Why is this program **deemed safe**?!
*Safe* With Eager Eval ---------------------- \begin{code}
{-@ 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}
**Safe** in Java, ML: program spins away, **never hits** divide-by-zero
*Unsafe* With Lazy Eval ----------------------- \begin{code}
{-@ 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}
**Unsafe** in Haskell: program skips `foo z` and **hits** divide-by-zero! Problem: Divergence ------------------- What is denoted by: `e :: {v:Int | P}`
`e` evaluates to `Int` satisfying `P`
or **diverges**!

Classical Floyd-Hoare notion of [partial correctness](http://en.wikipedia.org/wiki/Hoare_logic#Partial_and_total_correctness)
Problem: Divergence ------------------- \begin{code} **Consider**
{-@ e :: {v : Int | P} @-} let x = e in body \end{code}
**Eager Evaluation** *Can* assume `P(x)` when checking `body`

**Lazy Evaluation** *Cannot* assume `P(x)` when checking `body`
Eager vs. Lazy Binders ---------------------- \begin{code}
{-@ 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}
Inconsistent refinement for `a` is sound for **eager**, unsound for **lazy** Panic! Now what? ---------------
**Solution** Assign *non-trivial* refinements to *non-diverging* terms!

**Require A Termination Analysis** Don't worry, its easy...

Demo:   Disable `"--no-termination"` and see what happens!
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.
**Termination:** via Refinements!


[[continue...]](10_Termination.lhs.slides.html)