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)Refinement Types = Types + Logical Predicates
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))}0We 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))}0which 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))}0where `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))}0The 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)] -> aerrorThe 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 `String`s 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)}dWe 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}dand 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)}nWe 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](http://rise4fun.com/Z3/) 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)}maxand *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](https://github.com/ucsd-progsys/liquidhaskell/blob/master/include/Language/Haskell/Liquid/Prelude.hs)
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)}maxIn 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.