Laziness

8: module Laziness where
9: import Language.Haskell.Liquid.Prelude

Infinite Objects can lead to Unsoundness

17: infList :: {v:[Int] | false}
18: infList = incr 0
19: 
20: incr :: Int -> {v:[Int] | false}
21: incr x = x : incr (x+1)

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