Hopefully, the previous article gave you a basic idea about what refinement types look like. Several folks had interesting questions, that are worth discussing in a separate post, since they throw a lot of light on the strengths (or weaknesses, depending on your point of view!) of LiquidHaskell.

22: module Refinements101Reax where

## How to relate outputs and inputs

Recall the function `divide`

31: {-@ divide :: Int -> {v: Int | v /= 0 } -> Int @-} 32: divide :: Int -> Int -> Int 33: (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)divide (GHC.Types.Int)n 0 = [(GHC.Types.Char)] -> {VV : (GHC.Types.Int) | false}error {VV : [(GHC.Types.Char)] | (len([VV]) >= 0)}"divide by zero" 34: 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

and `abz`

was the absolute value function

40: abz :: Int -> Int 41: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((VV = 0) <=> (x = 0)),(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 42: | 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

nanothief remarked
that LiquidHaskell was unable to verify the safety of the following call to
`divide`

(i.e. was unable to show that `x`

was non-zero at the callsite).

50: {-@ f :: Int -> Int @-} 51: (GHC.Types.Int) -> (GHC.Types.Int)f (GHC.Types.Int)x | x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((VV = 0) <=> (x = 0)),(0 <= VV)}abz {VV : (GHC.Types.Int) | (VV = x)}x x:{VV : (GHC.Types.Int) | (VV >= 0),(0 <= VV)} -> y:{VV : (GHC.Types.Int) | (VV >= 0),(0 <= VV)} -> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x = y))}== {VV : (GHC.Types.Int) | (VV = (0 : int))}0 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}3 52: | otherwise = {VV : (GHC.Types.Int) | (VV = (3 : int))}3 (GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV != 0)} -> (GHC.Types.Int)`divide` {VV : (GHC.Types.Int) | (VV = x)}x

Nanothief correctly argues that the code is clearly safe as *“ abz x == 0 being false implies x /= 0”*.
Indeed, the code

*is safe*, however, the reason that LiquidHaskell rejected it has nothing to do with its inability to

*“track the constraints of values based on tests using new values derived from that value”*as Nanothief surmised, but instead, because LiquidHaskell supports

**modular verification**where the

*only*thing known about

`abz`

at a *use site*is whatever is specified in its

*type*.

Concretely speaking, the type

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

is too anemic to verify `f`

above, as it tells us nothing
about the *relationship* between the output and input – looking at it,
we have now way of telling that when the *output* (of `abz`

) is
non-zero, the *input* must also have been non-zero.

Instead, we can write a *stronger* type which does capture this information, for example

73: abz :: x:Int -> {v:Int | v = (if (x > 0) then x else (0 - x))}

where

77: v = (if p then e1 else e2)

is an abbreviation for the formula

81: (p => v == e1) && ((not p) => v = e2)

With this specification for `abz`

, LiquidHaskell is able to reason that
when `abz x`

is non-zero, `x`

is also non-zero. Of course, `abz`

is trivial
enough that we can very precisely capture its *exact* semantics in the
refinement type, but thats is rarely the case.

Nevertheless, even here, you could write a somewhat *weaker* specification,
that still had enough juice to allow the verification of the `divide`

call
in `f`

. In particular, we might write

94: {-@ abz :: x:Int -> {v:Int | ((0 <= v) && ((v = 0) <=> (x = 0))) } @-}

which states the output is `0`

*if and only if* the input is `0`

.
LiquidHaskell will happily verify that `abz`

implements this specification,
and will use it to verify the safety of `f`

above.

(BTW, follow the link above to *demo this code* yourself.)

## How to tell a Fib

Chris Done asked
why LiquidHaskell refused to verify the following definition of `fib`

.

110: {-@ fib :: n:Int -> { b:Int | (n >= 0 && b >= n) } @-} 111: fib :: Int -> Int 112: n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib 0 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0 113: fib 1 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}1 114: fib n = n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib ((GHC.Types.Int)nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (1 : int))}1) x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib ((GHC.Types.Int)nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (2 : int))}2)

Indeed, the both the *specification* and the *implementation* look pretty
legit, so what gives? It turns out that there are *two* different reasons why.

**Reason 1: Assumptions vs. Guarantees**

What we really want to say over here is that the *input* `n`

is non-negative. However, putting the refinement `n >= 0`

in
the *output* constraint means that it becomes something that
LiquidHaskell checks that the function `fib`

**guarantees**
(or **ensures**).
That is, the type states that we can pass `fib`

*any* value
`n`

(including *negative* values) and yet, `fib`

must return
values `b`

such that `b >= n`

*and* `n >= 0`

.

The latter requirement is a rather tall order when an arbitrary `n`

is passed in as input. `fib`

can make no such guarantees since
it was *given* the value `n`

as a parameter. The only way `n`

could
be non-negative was that if the caller had sent in a non-negative value.
Thus, we want to put the *burden of proof* on the right entity here,
namely the caller.

To assign the burden of proof appropriately, we place the
non-negative refinement on the *input type*

142: {-@ fib' :: n:{v:Int | v >= 0} -> {b:Int | (n >= 0 && b >= n) } @-} 143: fib' :: Int -> Int 144: n:{VV : (GHC.Types.Int) | (VV >= 0)} -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib' 0 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}0 145: fib' 1 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}1 146: fib' n = n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib ({VV : (GHC.Types.Int) | (VV >= 0)}nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (1 : int))}1) x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= n),(n >= 0)}fib ({VV : (GHC.Types.Int) | (VV >= 0)}nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (2 : int))}2)

where now at *calls to* `fib'`

LiquidHaskell will check that the argument
is non-negative, and furthermore, when checking `fib'`

LiquidHaskell will
**assume** that the parameter `n`

is indeed non-negative. So now the
constraint `n >= 0`

on the output is somewhat redundant, and the
non-negative `n`

guarantee holds trivially.

**Reason 2: The Specification is a Fib**

If you run the above in the demo, you will see that LiquidHaskell still doth protest loudly, and frankly, one might start getting a little frustrated at the stubbornness and petulance of the checker.

However, if you stare at the implementation, you will see that it in fact, *does not* meet the specification, as

162: fib' 2 == fib' 1 + fib' 0 163: == 0 + 1 164: == 1

LiquidHaskell is reluctant to prove things that are false. Rather than anthropomorphize frivolously, lets see why it is unhappy.

First, recall the somewhat simplified specification

171: fib' :: n:Int -> { b:Int | (b >= n) }

As we saw in the discussion about `abz`

, at each recursive callsite
the *only information* LiquidHaskell uses about the returned value,
is that described in the *output type* for that function call.

Thus, LiquidHaskell reasons that the expression:

179: fib' (n-1) + fib' (n-2)

has the type

183: {b: Int | exists b1, b2. b == b1 + b2 184: && b1 >= n-1 185: && b2 >= n-2 }

where the `b1`

and `b2`

denote the values returned by the
recursive calls — we get the above by plugging the parameters
`n-1`

and `n-2`

in for the parameter `n`

in output type for `fib'`

.

The SMT solver simplifies the above to

193: {b: Int | b >= 2n - 3}

Finally, to check the output guarantee is met, LiquidHaskell asks the SMT solver to prove that

197: (b >= 2n - 2) => (b >= n)

The SMT solver will refuse, of course, since the above implication is
*not valid* (e.g. when `n`

is `2`

) Thus, via SMT, LiquidHaskell proclaims
that the function `fib'`

does not implement the advertised type and hence
marks it *unsafe*.

## Fixing The Code

How then, do we get Chris' specification to work out? It seems like it
*should* hold (except for that pesky case where `n=2`

. Indeed,
let’s rig the code, so that all the base cases return `1`

.

213: {-@ fibOK :: n:Int -> {b:Int | ((b >= n) && (b >= 1))} @-} 214: fibOK :: Int -> Int 215: n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 1),(VV >= n)}fibOK 0 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}1 216: fibOK 1 = x:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV = (x : int))}1 217: fibOK n = n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 1),(VV >= n)}fibOK ((GHC.Types.Int)nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (1 : int))}1) x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x + y))}+ n:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV >= 1),(VV >= n)}fibOK ((GHC.Types.Int)nx:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV = (x - y))}-{VV : (GHC.Types.Int) | (VV = (2 : int))}2)

Here' we specify that not only is the output greater than the input, it is
**also** greater than `1`

.

Now in the recursive case, LiquidHaskell reasons that the value being output is

224: {b: Int | exists b1, b2. b == b1 + b2 225: && b1 >= n-1 && b1 >= 1 226: && b2 >= n-2 && b2 >= 1 }

which reduces to

230: {b: Int | b = 2n - 3 && n >= 2 }

which, the SMT solver is happy to verify, is indeed a subtype

234: of (i.e. implies the refinement of) the specified output 235: {b: Int | b >= n && b >= 1 }

## Conclusion

There are several things to take away.

We need to distinguish between

*assumptions*and*guarantees*when writing specifications for functions.For

*modularity*, LiquidHaskell, like every type system, uses only the (refinement)*type*of each function at each use site, and not the function’s*body*.Some seemingly intuitive specifications often aren’t; in future work it would be useful to actually generate tests as counterexamples that illustrate when a specification fails.