\begin{code}
module Laziness where
import Language.Haskell.Liquid.Prelude
{-@ LIQUID "--no-termination" @-}
safeDiv :: Int -> Int -> Int
foo :: Int -> Int
-- zero :: Int
-- diverge :: a -> b
\end{code}
Lazy Evaluation?
----------------
[[Skip]](11_Evaluation.lhs.slides.html)
Lazy Evaluation
===============
SMT based Verification
----------------------
Techniques developed for **strict** languages
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{spec}
{-@ foo :: n:Nat -> {v:Nat | v < n} @-}
foo n
| n > 0 = n - 1
| otherwise = foo n
\end{spec}
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{spec}
{-@ 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{spec}
**Safe** in Java, ML: program spins away, **never hits** divide-by-zero
*Unsafe* With Lazy Eval
-----------------------
\begin{spec}
{-@ 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{spec}
**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{spec} **Consider**
{-@ e :: {v : Int | P} @-}
let x = e in body
\end{spec}
**Eager Evaluation**
*Can* assume `P(x)` when checking `body`
**Lazy Evaluation**
*Cannot* assume `P(x)` when checking `body`
Eager vs. Lazy Binders
----------------------
\begin{spec}
{-@ 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{spec}
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.