# Laziness

```8: module Laziness where
```

# Infinite Objects can lead to Unsoundness

Infinite Objects can be refined with false
```17: infList :: {v:[Int] | false}
18: infList = incr 0
19:
20: incr :: Int -> {v:[Int] | false}
21: incr x = x : incr (x+1)
```

Under false anything can be proven
```27: prop = liquidAssert ((\_ -> 0==1) infList)
```

# Our solution (Current Work)

• Use termination analysis to track infinite objects

• Use true refinements for infinite objects

# Size-based Termination Analysis

• Use refinement types to force the recursive argument to decrease
```44: unsafeIncr :: Int -> [Int]
45: {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : [{VV : (GHC.Types.Int) | false}]<\_ VV -> false> | false}unsafeIncr {VV : (GHC.Types.Int) | (VV >= 0)}x
46:   -- unsafeIncr :: {v:Int | v < x} -> [Int]
47:   = {VV : (GHC.Types.Int) | (VV == x) && (VV >= 0)}x forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:{VV : (GHC.Types.Int) | false}
-> x2:[{VV : (GHC.Types.Int)<p x1> | false}]<p>
-> {VV : [{VV : (GHC.Types.Int) | false}]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}: {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : [{VV : (GHC.Types.Int) | false}]<\_ VV -> false> | false}unsafeIncr ({VV : (GHC.Types.Int) | (VV == x) && (VV >= 0)}xx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
```

• `prop` is safe, but the program is decided unsafe
```54: forall a. a -> aprop1 = {VV : (GHC.Types.Bool) | ((Prop VV))}
-> {VV : a | false} -> {VV : a | false}liquidAssert ({VV : (GHC.Types.Bool) | false}(\_ -> {VV : (GHC.Integer.Type.Integer) | (VV == 1)}0x1:{VV : (GHC.Integer.Type.Integer) | false}
-> x2:{VV : (GHC.Integer.Type.Integer) | false}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}==1) {VV : [{VV : (GHC.Types.Int) | false}]<\_ VV -> false> | false}unsafeL)
55:   where {VV : [{VV : (GHC.Types.Int) | false}]<\_ VV -> false> | false}unsafeL = {VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : [{VV : (GHC.Types.Int) | false}]<\_ VV -> false> | false}unsafeIncr {VV : (GHC.Types.Int) | (VV == (0  :  int))}0
```

Demo: Check the type of `unsafeL`

# Refinements of infinite Structures

If you need a non-terminating function, use `Lazy` to declare

• We know that `incr` may not terminate

• Its return type is refined with true

```71: {-@ Lazy safeIncr @-}
72: {-@ safeIncr :: Int -> [Int] @-}
73: safeIncr :: Int -> [Int]
74: (GHC.Types.Int) -> [(GHC.Types.Int)]safeIncr (GHC.Types.Int)x = {VV : (GHC.Types.Int) | (VV == x)}x forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
x1:(GHC.Types.Int)
-> x2:[{VV : (GHC.Types.Int)<p x1> | true}]<p>
-> {VV : [(GHC.Types.Int)]<p> | (((null VV)) <=> false) && ((len VV) == (1 + (len x2)))}: (GHC.Types.Int) -> [(GHC.Types.Int)]safeIncr ({VV : (GHC.Types.Int) | (VV == x)}xx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
```

Now, `prop` is unsafe

```82: forall a. a -> aprop2 = {VV : (GHC.Types.Bool) | ((Prop VV))} -> a -> aliquidAssert ({VV : (GHC.Types.Bool) | (not (((Prop VV))))}(\_ -> {VV : (GHC.Integer.Type.Integer) | (VV == 1)}0x1:{VV : (GHC.Integer.Type.Integer) | (VV >= 0)}
-> x2:{VV : (GHC.Integer.Type.Integer) | (VV >= 0)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}==1) {VV : [(GHC.Types.Int)] | (VV == safeL) && ((len VV) >= 0)}safeL)
83:   where [(GHC.Types.Int)]safeL = (GHC.Types.Int) -> [(GHC.Types.Int)]safeIncr {VV : (GHC.Types.Int) | (VV == (0  :  int))}0
```

# Restore Soundness

• Use termination analysis to track infinite objects

• Use true refinements for infinite objects