Simple Refinement Types

7: module SimpleRefinements where
8: import Prelude hiding ((!!), length)
9: import Language.Haskell.Liquid.Prelude

Simple Refinement Types

This type describes Int values that equal 0.

20: {-@ zero :: {v:Int | v = 0} @-}
21: zero     :: Int
22: {VV : (GHC.Types.Int) | (VV == 0)}zero     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0

Refinements are logical formulas

Since

v = 0 implies v >= 0

Therefore

{v:Int | v = 0} <: {v:Int | v >= 0}

Refinements are logical formulas

So we can have a type for natural numbers:

41: type Nat = {v:Int | v >= 0}

And we can type 0 as Nat:

51: {-@ zero' :: Nat @-}
52: zero'     :: Int
53: {VV : (GHC.Types.Int) | (VV >= 0)}zero'     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0

Refinements are logical formulas

Similarly, since

v = 0 => v mod 2 = 0

Therefore

{v:Int | v = 0} <: {v:Int | v mod 2 = 0}

Thus, via SMT based subtyping LiquidHaskell verifies:

70: {-@ type Even = {v:Int | v mod 2 = 0} @-}
71: 
72: {-@ zero'' :: Even @-}
73: zero''     :: Int
74: {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}zero''     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0

Lists

Refinements can live inside type constructors:

84: infixr `C`
85: data L a = N | C a (L a)

Lists: Universal Invariants

Constructors enable universally quantified invariants.

For example, every element in a list is non-negative:

96: {-@ natList :: L Nat @-}
97: natList     :: L Int
98: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})natList     =  {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= zero)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (3  :  int))}3 {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV /= 0) && (VV /= zero'') && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | false}) | ((llen VV) == 0)}N

or, every element in a list is even:

104: {-@ evenList :: L Even @-}
105: evenList     :: L Int
106: (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})evenList     =  {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV >= 0) && (VV >= zero)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (2  :  int))}2 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (GHC.Types.Int) | (VV == (8  :  int))}8 {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}
-> xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)})
-> {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0) && (VV /= 0) && (VV > 0) && (VV > zero) && (VV >= 0)}) | ((llen VV) == (1 + (llen xs)))}`C` {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | false}) | ((llen VV) == 0)}N

Demo: Lets see what happens if evenList contained an odd number.

Refinement Function Types

Consider a safeDiv operator:

119: safeDiv    :: Int -> Int -> Int
120: (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 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x / y))}`div` {VV : (GHC.Types.Int) | (VV == y) && (VV /= 0)}y

We can use refinements to specify a precondition: divisor is non-zero

126: {-@ safeDiv :: Int -> {v:Int | v != 0} -> Int @-}

Demo: Lets see what happens if we make safeDivision by zero.

Dependent Function Types

Consider a list indexing function:

137: (!!)         :: L a -> Int -> a
138: (C x _) !! 0 = x
139: (C _ xs)!! n = xs!!(n-1)
140: _       !! _ = liquidError "This should not happen!"

We desire precondition that index i be between 0 and list length.

Measuring A List's length in logic

We define a measure for the length of a List

153: {-@ measure llen :: (L a) -> Int
154:     llen(N)      = 0
155:     llen(C x xs) = 1 + (llen xs)
156:   @-}

The measure strengthens the type of data constructors

162: data L a where 
163:   N :: {v : L a | (llen v) = 0}
164:   C :: a -> xs:(L a) -> {v:(L a) |(llen v) = 1 + (llen xs)}

Measuring A List's length in logic

Now we can verify

175: {-@ length :: xs:(L a) -> {v:Int | v = (llen xs)} @-}
176: length     :: L a -> Int
177: forall a.
xs:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length N        = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x  :  int))}0
178: length (C _ xs) = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ (xs:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L a) | (VV == xs)}xs)

Measuring A List's length in logic

And we can type (!!) as

189: {-@ (!!) :: ls:(L a) -> {v:Nat | v < (llen ls)} -> a @-}
190: (!!)         :: L a -> Int -> a
191: (C x _) forall a.
ls:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))} -> a!! 0 = {VV : a | (VV == x)}x
192: (C _ xs)!! n = (SimpleRefinements.L a)xsls:(SimpleRefinements.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))} -> a!!({VV : (GHC.Types.Int) | (VV >= 0)}nx:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
193: _       !! _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"This should not happen!"

Demo: lets see what happens if we change the precondition