loop
What is a Refinement Type? In a nutshell,
Refinement Types = Types + Predicates
That is, refinement types allow us to decorate types with logical predicates, which you can think of as boolean-valued Haskell expressions, that constrain the set of values described by the type. This lets us specify sophisticated invariants of the underlying values.
Let us define some refinement types:1
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. 2
To use these types we can write:
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
.
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 3
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:
In Summary the key points about refinement types are:
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 String
s 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.
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:
Exercise: (List Average): Consider the function avg
:
n
?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. 5
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.
Exercise: (Propositions): What happens if you delete the type for isPositive
? Can you change the type for isPositive
(i.e. write some other type) while preserving safety?
Exercise: (Assertions): Consider the following assert function, and two use sites. Write a suitable refinement type signature for lAssert
so that lAssert
and yes
are accepted but no
is rejected.
Hint: You need a pre-condition that lAssert
is only called with True
.
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:
max' < i'
from the branch condition,0 <= i'
from the abs
post-condition, and0 <= 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.
This concludes our quick introduction to Refinement Types and LiquidHaskell. Hopefully you have some sense of how to
You can read the type of Zero
as: “v
is an Int
such that v
equals 0
” and NonZero
as : “v
is an Int
such that v
does not equal 0
”↩︎
We will use @
-marked comments to write refinement type annotations in the Haskell source file, making these types, quite literally, machine-checked comments!↩︎
We use a different names zero'
, zero''
etc. as (currently) LiquidHaskell supports at most one refinement type for each top-level name.↩︎
Dually, a standard Haskell type has the trivial refinement true
. For example, Int
is equivalent to {v:Int|true}
.↩︎
LiquidHaskell is able to automatically make these arithmetic deductions by using an SMT solver which has built-in decision procedures for arithmetic, to reason about the logical refinements.↩︎