 6: module Laziness where
 7: 
 8: import Language.Haskell.Liquid.Prelude
 9: 
10: {-@ LIQUID "--no-termination" @-}
11: {-@ LIQUID "--short"          @-}
12: 
13: 
14: safeDiv :: Int -> Int -> Int
15: foo     :: Int -> Int
16: -- zero    :: Int 
17: -- diverge :: a -> b

Lazy Evaluation?

[Skip]

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

71: {-@ safeDiv :: Int -> {v:Int|v /= 0} -> Int @-}
72: Int -> {v : Int | (v /= 0)} -> IntsafeDiv Intn 0 = {x2 : [Char] | false} -> IntliquidError {x2 : [Char] | ((len x2) >= 0)}"div-by-zero!"
73: safeDiv n d = {x2 : Int | (x2 == n)}n x1:Int
-> x2:Int
-> {x6 : Int | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x2 : Int | (x2 /= 0)}d

Should only call safeDiv with non-zero values

An Innocent Function

foo returns a value strictly less than input.

90: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
91: foo n   
92:   | n > 0     = n - 1
93:   | otherwise = foo n

LiquidHaskell Lies!

100: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
101: x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {v : Int | (v >= 0)}n   
102:   | {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}> {x2 : Int | (x2 == (0  :  int))}0     = {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == (1  :  int))}1
103:   | otherwise = x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {x3 : Int | (x3 == n) && (x3 >= 0)}n
104: 
105: Intexplode = let {x2 : Int | (x2 == (0  :  int))}z = {x2 : Int | (x2 == (0  :  int))}0    
106:               {x3 : Int | (x3 >= 0) && (x3 < z)}a = x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {x3 : Int | (x3 == z) && (x3 == (0  :  int))}z
107:           in  
108:               ({VV : Int | (VV == 0) && (VV == 1) && (VV == a) && (VV == z) && (VV > 0) && (VV > a) && (VV > z) && (VV < 0) && (VV < a) && (VV < z)}
-> Int\{VV : Int | (VV == 0) && (VV == 1) && (VV == a) && (VV == z) && (VV > 0) && (VV > a) && (VV > z) && (VV < 0) && (VV < a) && (VV < z)}x -> {x2 : Int | (x2 == (2013  :  int))}2013 Int -> {x3 : Int | (x3 /= 0)} -> Int`safeDiv` {x3 : Int | (x3 == z) && (x3 == (0  :  int))}z) {x4 : Int | (x4 == a) && (x4 >= 0) && (x4 < z)}a

Why is this program deemed safe?!

Safe With Eager Eval

122: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
123: foo n   
124:   | n > 0     = n - 1
125:   | otherwise = foo n
126: 
127: explode = let z = 0     -- :: {v:Int| v = 0}
128:               a = foo z -- :: {v:Nat| v < z}
129:           in  
130:               (\x -> 2013 `safeDiv` z) a

Safe in Java, ML: program spins away, never hits divide-by-zero

Unsafe With Lazy Eval

143: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
144: foo n   
145:   | n > 0     = n - 1
146:   | otherwise = foo n
147: 
148: explode = let z = 0     -- :: {v:Int| v = 0}
149:               a = foo z -- :: {v:Nat| v < z}
150:           in  
151:               (\x -> 2013 `safeDiv` z) a

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

diverges!

Classical Floyd-Hoare notion of partial correctness

Problem: Divergence

Consider

191:         {-@ e :: {v : Int | P} @-}
192: 
193:         let x = e in body

Eager Evaluation

Can assume P(x) when checking body

Lazy Evaluation

Cannot assume P(x) when checking body

Eager vs. Lazy Binders

216: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
217: foo n   
218:   | n > 0     = n - 1
219:   | otherwise = foo n
220: 
221: explode = let z = 0     -- :: {v:Int| v = 0}
222:               a = foo z -- :: {v:Nat| v < z}
223:           in  
224:               (\x -> 2013 `safeDiv` z) a

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

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Strengthened Constructors
Abstract: Refinements over functions and data
Lazy Evaluation: Requires Termination
Termination: via Refinements!

[continue...]