2013-01-01-refinement-types-101.lhs

---
layout: post
title: "Refinement Types 101"
date: 2013-01-01 16:12
author: Ranjit Jhala
published: true
comments: true
external-url:
categories: basic
demo: refinements101.hs
---

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, 

<blockquote><p>
Refinement Types = Types + Logical Predicates
</p></blockquote>

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? 

<!-- more -->

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

\begin{code}
module Intro where

import Language.Haskell.Liquid.Prelude  (liquidAssert)
\end{code}

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

\begin{code}
zero' :: Int
zero' = 0
\end{code}

We can ascribe to the variable `zero'` the refinement type

\begin{code}
{-@ zero' :: {v: Int | 0 <= v} @-}
\end{code}

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!


\begin{code}
{-@ zero'' :: {v: Int | (0 <= v && v < 100) } @-}
zero'' :: Int
zero'' = 0
\end{code}

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

\begin{code}
{-@ zero''' :: {v: Int | ((v mod 2) = 0) } @-}
zero''' :: Int
zero''' = 0
\end{code}

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

\begin{code}
{-@ zero'''' :: {v: Int | v = 0 } @-}
zero'''' :: Int
zero'''' = 0
\end{code}

(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:

\begin{code}
{-@ zero :: {v: Int | ((0 <= v) && ((v mod 2) = 0) && (v < 100)) } @-}
zero     :: Int
zero     =  0
\end{code}

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 

\begin{code}
{-@ error' :: {v: String | false } -> a  @-}
error'     :: String -> a
error'     = error
\end{code}

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 `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

\begin{code}
{-@ lAssert     :: {v:Bool | (Prop v)} -> a -> a  @-}
lAssert         :: Bool -> a -> a 
lAssert True  x = x
lAssert False _ = error' "lAssert failure" 
\end{code}

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. 

\begin{code}
divide     :: Int -> Int -> Int
divide n 0 = error' "divide by zero"
divide n d = n `div` d
\end{code}

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

\begin{code}
{-@ divide :: Int -> {v: Int | v != 0 } -> Int @-}
\end{code}

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

\begin{code}
{-@ divide' :: Int  -> {v:Int | v /= 0} -> Int @-}
divide'     :: Int -> Int -> Int
divide' n 0 = error' "divide by zero"
divide' n d = lAssert (d /= 0) $ n `div` d
\end{code}

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

\begin{code}
abz               :: Int -> Int
abz n | 0 < n     = n
      | otherwise = 0 - n
\end{code}

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

\begin{code}
{-@ abz :: Int -> {v: Int | 0 <= v } @-}
\end{code}

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. 

\begin{code}
{-@ truncate :: Int -> Int -> Int @-}
truncate i max  
  | i' <= max' = i
  | otherwise  = max' * (i `divide` i')
    where i'   = abz i
          max' = abz max 
\end{code}

`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

\begin{code}
{-@ truncate' :: Int -> Int -> Int @-}
truncate' i max  
  | i' <= max' = i
  | otherwise  = lAssert (i' /= 0) $ max' * (i `divide` i')
    where i'   = abz i
          max' = abz max 
\end{code}

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](https://github.com/ucsd-progsys/liquidhaskell/blob/master/include/Language/Haskell/Liquid/Prelude.hs)

\begin{code}
{-@ truncate'' :: Int -> Int -> Int @-}
truncate'' i max  
  | i' <= max' = i
  | otherwise  = liquidAssert (i' /= 0) $ max' * (i `divide` i')
    where i'   = abz i
          max' = abz max 
\end{code}

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.