Refinement Types

Defining Types

Let us define some refinement types:¹

The Value Variable v denotes the set of valid inhabitants of each refinement type. Hence, Zero describes the set of Int values that are equal to 0, that is, the singleton set containing just 0, and NonZero describes the set of Int values that are not equal to 0, that is, the set {1, -1, 2, -2, ...} and so on. ²

To use these types we can write:

Errors

If we try to say nonsensical things like:

LiquidHaskell will complain with an error message:

../liquidhaskell-tutorial/src/03-basic.lhs:72:3-6: Error: Liquid Type Mismatch

72 |   one' = 1 :: Int
       ^^^^

  Inferred type
    VV : {VV : Int | VV == (1 : int)}

  not a subtype of Required type
    VV : {VV : Int | VV == 0}

The message says that the expression 1 :: Int has the type

    {v:Int | v == 1}

which is not (a subtype of) the required type

    {v:Int | v == 0}

as 1 is not equal to 0.

Subtyping

What is this business of subtyping? Suppose we have some more refinements of Int

What is the type of zero? Zero of course, but also Nat:

and also Even:

and also any other satisfactory refinement, such as ³

Zero is the most precise type for 0::Int, as it is a subtype of Nat, Even and Lt100. This is because the set of values defined by Zero is a subset of the values defined by Nat, Even and Lt100, as the following logical implications are valid:

• \(v = 0 \Rightarrow 0 \leq v\)
• \(v = 0 \Rightarrow v \ \mbox{mod}\ 2 = 0\)
• \(v = 0 \Rightarrow v < 100\)

In Summary the key points about refinement types are:

1. A refinement type is just a type decorated with logical predicates.
2. A term can have different refinements for different properties.
3. When we erase the predicates we get the standard Haskell types.⁴

Writing Specifications

Let’s write some more interesting specifications.

Typing Dead Code We can wrap the usual error function in a function die with the type:

The interesting thing about die is that the input type has the refinement false, meaning the function must only be called with Strings that satisfy the predicate false. This seems bizarre; isn’t it impossible to satisfy false? Indeed! Thus, a program containing die typechecks only when LiquidHaskell can prove that die is never called. For example, LiquidHaskell will accept

by inferring that the branch condition is always False and so die cannot be called. However, LiquidHaskell will reject

as the branch may (will!) be True and so die can be called.

Refining Function Types: Pre-conditions

Let’s use die to write a safe division function that only accepts non-zero denominators.

From the above, it is clear to us that div is only called with non-zero divisors. However, LiquidHaskell reports an error at the call to "die" because, what if divide' is actually invoked with a 0 divisor?

We can specify that will not happen, with a pre-condition that says that the second argument is non-zero:

To Verify that divide never calls die, LiquidHaskell infers that "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 die occurs. LiquidHaskell arrives at this conclusion by using the fact that in the first equation for divide the denominator is in fact

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

which contradicts the pre-condition (i.e. input) type. Thus, by contradiction, LiquidHaskell deduces that the first equation is dead code and hence die will not be called at run-time.

The above signature forces us to ensure that that when we use divide, we only supply provably NonZero arguments. Hence, these two uses of divide are fine:

Refining Function Types: Post-conditions

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

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

LiquidHaskell verifies that abs indeed enjoys the above type by deducing that n is trivially non-negative when 0 < n and that in the otherwise case, the value 0 - n is indeed non-negative. ⁵

Testing Values: Booleans and Propositions

In the above example, we compute a value that is guaranteed to be a Nat. Sometimes, we need to test if a value satisfies some property, e.g., is NonZero. For example, let’s write a command-line calculator:

which takes two numbers and divides them. The function result checks if d is strictly positive (and hence, non-zero), and does the division, or otherwise complains to the user:

Finally, isPositive is a test that returns a True if its input is strictly greater than 0 or False otherwise:

To verify the call to divide inside result we need to tell LiquidHaskell that the division only happens with a NonZero value d. However, the non-zero-ness is established via the test that occurs inside the guard isPositive d. Hence, we require a post-condition that states that isPositive only returns True when the argument is positive:

In the above signature, the output type (post-condition) states that isPositive x returns True if and only if x was in fact strictly greater than 0. In other words, we can write post-conditions for plain-old Bool-valued tests to establish that user-supplied values satisfy some desirable property (here, Pos and hence NonZero) in order to then safely perform some computation on it.

Hint: You need a pre-condition that lAssert is only called with True.

Putting It All Together

Let’s wrap up this introduction with a simple truncate function that connects all the dots.

The expression truncate i n evaluates to i when the absolute value of i is less than the upper bound max, and otherwise truncates the value at the maximum n. LiquidHaskell verifies that the use of divide is safe by inferring that:

1. max' < i' from the branch condition,
2. 0 <= i' from the abs post-condition, and
3. 0 <= max' from the abs post-condition.

From the above, LiquidHaskell infers that i' /= 0. That is, at the call site i' :: NonZero, thereby satisfying the pre-condition for divide and verifying that the program has no pesky divide-by-zero errors.

Recap

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, pre-conditions, and post-conditions 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.