7: module SimpleRefinements where 8: import Language.Haskell.Liquid.Prelude
We use special comments to give specifications, as refinement types.
This type describes Int
values that equal 0
.
22: {-@ zero :: {v:Int | v = 0} @-} 23: zero :: Int 24: {VV : (GHC.Types.Int) | (VV == 0)}zero = x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1 : int))}0
If
refinement of T1
implies refinement of T2
p1 => p2
Then
T1
is a subtype of T2
{v:t | p1} <: {v:t | p2}
For example, since
v = 0
implies v >= 0
Therefore
{v:Int | v = 0} <: {v:Int | v >= 0}
58: type Nat = {v:Int | v >= 0}
And, via SMT based subtyping LiquidHaskell verifies:
68: {-@ zero' :: Nat @-} 69: zero' :: Int 70: {VV : (GHC.Types.Int) | (VV >= 0)}zero' = x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1 : int))}0
Constructors enable universally quantified invariants.
For example, we define a list:
82: infixr `C` 83: data L a = N | C a (L a)
And specify that, every element in a list is non-negative:
91: {-@ natList :: L Nat @-} 92: natList :: L Int 93: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})natList = {VV : (GHC.Types.Int) | (VV == (0 : int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)} -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)}) -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= SimpleRefinements.zero)})`C` {VV : (GHC.Types.Int) | (VV == (1 : int))}1 {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)} -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)}) -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})`C` {VV : (GHC.Types.Int) | (VV == (3 : int))}3 {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)} -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)}) -> (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV > 0) && (VV > SimpleRefinements.zero) && (VV >= 0)})`C` (SimpleRefinements.L {VV : (GHC.Types.Int) | false})N
Demo: Lets see what happens if natList
contained a negative number.
Consider a safeDiv
operator:
105: safeDiv :: Int -> Int -> Int 106: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV /= 0)} -> (GHC.Types.Int)safeDiv (GHC.Types.Int)x {VV : (GHC.Types.Int) | (VV /= 0)}y = {VV : (GHC.Types.Int) | (VV == x)}x x1:(GHC.Types.Int) -> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (((x1 >= 0) && (x2 >= 0)) => (VV >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (VV <= x1)) && (VV == (x1 / x2))}`div` {VV : (GHC.Types.Int) | (VV == y) && (VV /= 0)}y
We can use refinements to specify a precondition: divisor is non-zero
113: {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}
Demo: Lets see what happens if the preconditions cannot be proven.
126: (!!) :: L a -> Int -> a 127: (C x _) !! 0 = x 128: (C _ xs)!! n = xs!!(n-1) 129: _ !! _ = liquidError "This should not happen!"
We desire a precondition that index i
be between 0
and list length.
We use measures to talk about the length of a list in logic.