Skip to content

Refinement Types 101

One of the great things about Haskell is its brainy type system that allows one to enforce a variety of invariants at compile time, thereby nipping a large swathe of run-time errors in the bud. Refinement types allow us to use modern logic solvers (aka SAT and SMT engines) to dramatically extend the scope of invariants that can be statically verified.

What is a Refinement Type?

In a nutshell,

Refinement Types = Types + Logical Predicates

That is, refinement types allow us to decorate types with logical predicates (think boolean-valued Haskell expressions) which constrain the set of values described by the type, and hence allow us to specify sophisticated invariants of the underlying values.

Say what?

(Btw, click the title to demo LiquidHaskell on the code in this article)

42: module Intro where
43: 
44: import Language.Haskell.Liquid.Prelude  (liquidAssert)

Let us jump right in with a simple example, the number 0 :: Int. As far as Haskell is concerned, the number is simply an Int (lets not worry about things like Num for the moment). So are 2, 7, and 904. With refinements we can dress up these values so that they stand apart. For example, consider the binder

54: zero' :: Int
55: {VV : (GHC.Types.Int) | (0 <= VV)}zero' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0

We can ascribe to the variable zero' the refinement type

61: {-@ zero' :: {v: Int | 0 <= v} @-}

which is simply the basic type Int dressed up with a predicate. The binder v is called the value variable, and so the above denotes the set of Int values which are greater than 0. Of course, we can attach other predicates to the above value, for example

Note: We will use @-marked comments to write refinement type annotations the Haskell source file, making these types, quite literally, machine-checked comments!

75: {-@ zero'' :: {v: Int | (0 <= v && v < 100) } @-}
76: zero'' :: Int
77: {VV : (GHC.Types.Int) | (VV < 100),(0 <= VV)}zero'' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0

which states that the number is in the range 0 to 100, or

83: {-@ zero''' :: {v: Int | ((v mod 2) = 0) } @-}
84: zero''' :: Int
85: {VV : (GHC.Types.Int) | ((VV mod 2) = 0)}zero''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0

where mod is the modulus operator in the refinement logic. Thus, the type above states that zero is an even number.

We can also use a singleton type that precisely describes the constant

94: {-@ zero'''' :: {v: Int | v = 0 } @-}
95: zero'''' :: Int
96: {VV : (GHC.Types.Int) | (VV = 0)}zero'''' = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0

(Aside: we use a different names zero', zero'' etc. for a silly technical reason -- LiquidHaskell requires that we ascribe a single refinement type to a top-level name.)

Finally, we could write a single type that captures all the properties above:

106: {-@ zero :: {v: Int | ((0 <= v) && ((v mod 2) = 0) && (v < 100)) } @-}
107: zero     :: Int
108: {VV : (GHC.Types.Int) | ((VV mod 2) = 0),(VV < 100),(0 <= VV)}zero     =  x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x  :  int))}0

The key points are:

  1. A refinement type is just a type decorated with logical predicates.
  2. A value can have different refinement types that describe different properties.
  3. If we erase the green bits (i.e. the logical predicates) we get back exactly the usual Haskell types that we know and love.
  4. A vanilla Haskell type, say Int has the trivial refinement true i.e. is really {v: Int | true}.

We have built a refinement type-based verifier called LiquidHaskell. Lets see how we can use refinement types to specify and verify interesting program invariants in LiquidHaskell.

Writing Safety Specifications

We can use refinement types to write various kinds of more interesting safety specifications.

First, we can write a wrapper around the usual error function 

133: {-@ error' :: {v: String | false } -> a  @-}
134: error'     :: String -> a
135: {VV : [(GHC.Types.Char)] | false} -> aerror'     = [(GHC.Types.Char)] -> aerror

The interesting thing about the type signature for error' is that the input type has the refinement false. That is, the function must only be called with Strings that satisfy the predicate false. Of course, there are no such values. Thus, a program containing the above function typechecks exactly when LiquidHaskell can prove that the function error' is never called.

Next, we can use refinements to encode arbitrary programmer-specified assertions by defining a function

149: {-@ lAssert     :: {v:Bool | (Prop v)} -> a -> a  @-}
150: lAssert         :: Bool -> a -> a 
151: {VV : (GHC.Types.Bool) | (? Prop([VV]))} -> a -> alAssert True  ax = {VV : a | (VV = x)}x
152: lAssert False _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"lAssert failure"

In the refinement, (Prop v) denotes the Haskell Bool value v interpreted as a logical predicate. In other words, the input type for this function specifies that the function must only be called with the value True.

Refining Function Types : Preconditions

Lets use the above to write a divide function that only accepts non-zero denominators. 

168: divide     :: Int -> Int -> Int
169: (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)divide (GHC.Types.Int)n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero"
170: divide n d = {VV : (GHC.Types.Int) | (VV = n)}n x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | (VV != 0)}d

We can specify that the non-zero denominator precondition with a suitable refinement on the input component of the function's type 

177: {-@ divide :: Int -> {v: Int | v != 0 } -> Int @-}

How does LiquidHaskell verify the above function?

The key step is that LiquidHaskell deduces that the expression "divide by zero" is not merely of type String, but in fact has the the refined type {v:String | false} in the context in which the call to error' occurs.

LiquidHaskell arrives at this conclusion by using the fact that in the first equation for divide the denominator parameter is in fact 0 :: {v: Int | v = 0} which contradicts the precondition (i.e. input) type.

In other words, LiquidHaskell deduces by contradiction, that the first equation is dead code and hence error' will not be called at run-time.

If you are paranoid, you can put in an explicit assertion

199: divide'     :: Int -> Int -> Int
200: {VV : (GHC.Types.Int) | false}
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}divide' {VV : (GHC.Types.Int) | false}n 0 = {VV : [(GHC.Types.Char)] | false} -> {VV : (GHC.Types.Int) | false}error' {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero"
201: divide' n d = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}lAssert ({VV : (GHC.Types.Int) | false}d x:{VV : (GHC.Types.Int) | false}
-> y:{VV : (GHC.Types.Int) | false}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ({VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false})
-> {VV : (GHC.Types.Int) | false} -> {VV : (GHC.Types.Int) | false}$ {VV : (GHC.Types.Int) | false}n x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x / y))}`div` {VV : (GHC.Types.Int) | false}d

and LiquidHaskell will verify the assertion (by verifying the call to lAssert) for you.

Refining Function Types : Postconditions

Next, lets see how we can use refinements to describe the outputs of a function. Consider the following simple absolute value function

214: abz               :: Int -> Int
215: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz (GHC.Types.Int)n | {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV = n)}n     = {VV : (GHC.Types.Int) | (VV = n)}n
216:       | otherwise = {VV : (GHC.Types.Int) | (VV = (0  :  int))}0 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}- {VV : (GHC.Types.Int) | (VV = n)}n

We can use a refinement on the output type to specify that the function returns non-negative values

223: {-@ abz :: Int -> {v: Int | 0 <= v } @-}

LiquidHaskell verifies that abz indeed enjoys the above type by deducing that n is trivially non-negative when 0 < n and that in the otherwise case, i.e. when not (0 < n) the value 0 - n is indeed non-negative (lets not worry about underflows for the moment.) LiquidHaskell is able to automatically make these arithmetic deductions by using an SMT solver which has decision built-in procedures for arithmetic, to reason about the logical refinements.

Putting It All Together

Lets wrap up this introduction with a simple truncate function that connects all the dots. 

244: {-@ truncate :: Int -> Int -> Int @-}
245: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate (GHC.Types.Int)i (GHC.Types.Int)max  
246:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
247:   | otherwise  = {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
248:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
249:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

truncate i n simply returns i if its absolute value is less the upper bound max, and otherwise truncates the value at the maximum. LiquidHaskell verifies that the use of divide is safe by inferring that at the call site

  1. i' > max' from the branch condition.
  2. 0 <= i' from the abz postcondition (hover mouse over i').
  3. 0 <= max' from the abz postcondition (hover mouse over max').

From the above, LiquidHaskell infers that i' != 0. That is, at the call site i' :: {v: Int | v != 0}, thereby satisfying the precondition for divide and verifying that the program has no pesky divide-by-zero errors. Again, if you really want to make sure, put in an assertion

268: {-@ truncate' :: Int -> Int -> Int @-}
269: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate' (GHC.Types.Int)i (GHC.Types.Int)max  
270:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
271:   | otherwise  = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> (GHC.Types.Int) -> (GHC.Types.Int)lAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),
                          (VV >= zero''''),
                          (0 <= VV),
                          (VV <= i')}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
                             (VV >= zero''''),
                             (0 <= VV),
                             (VV <= i')}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ((GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int) -> (GHC.Types.Int)$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
272:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
273:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

and lo! LiquidHaskell will verify it for you.

Modular Verification

Incidentally, note the import statement at the top. Rather than rolling our own lAssert we can import and use a pre-defined version liquidAssert defined in an external module

286: {-@ truncate'' :: Int -> Int -> Int @-}
287: (GHC.Types.Int) -> (GHC.Types.Int) -> (GHC.Types.Int)truncate'' (GHC.Types.Int)i (GHC.Types.Int)max  
288:   | {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),(VV >= zero''''),(0 <= VV)}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' = {VV : (GHC.Types.Int) | (VV = i)}i
289:   | otherwise  = {VV : (GHC.Types.Bool) | (? Prop([VV]))}
-> (GHC.Types.Int) -> (GHC.Types.Int)liquidAssert ({VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i' x:{VV : (GHC.Types.Int) | (VV >= 0),
                          (VV >= zero''''),
                          (0 <= VV),
                          (VV <= i')}
-> y:{VV : (GHC.Types.Int) | (VV >= 0),
                             (VV >= zero''''),
                             (0 <= VV),
                             (VV <= i')}
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x != y))}/= {VV : (GHC.Types.Int) | (VV = (0  :  int))}0) ((GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int) -> (GHC.Types.Int)$ {VV : (GHC.Types.Int) | (VV = max'),(0 <= VV)}max' x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (&& [(x >= 0); (y >= 0)] => (VV >= 0))}* ({VV : (GHC.Types.Int) | (VV = i)}i (GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = i'),(0 <= VV)}i')
290:     where {VV : (GHC.Types.Int) | (0 <= VV)}i'   = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = i)}i
291:           {VV : (GHC.Types.Int) | (0 <= VV)}max' = (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = max)}max

In fact, LiquidHaskell comes equipped with suitable refinements for standard functions and it is easy to add refinements as we shall demonstrate in subsequent articles.

Conclusion

This concludes our quick introduction to Refinement Types and LiquidHaskell. Hopefully you have some sense of how to

  1. Specify fine-grained properties of values by decorating their types with logical predicates.
  2. Encode assertions, preconditions, and postconditions with suitable function types.
  3. Verify semantic properties of code by using automatic logic engines (SMT solvers) to track and establish the key relationships between program values.
Ranjit Jhala
2013-01-01 16:12
basic