Getting To the Bottom
Previously, we caught LiquidHaskell telling a lie. Today, lets try to get to the bottom of this mendacity, in order to understand how we can ensure that it always tells the truth.
20: module GettingToTheBottom where
The Truth Lies At the Bottom¶
To figure out how we might prevent falsehoods, lets try to understand whats really going on. We need to go back to the beginning.
Recall that the refinement type:
30: {v:Int | 0 <= v}
is supposed to denote the set of Int values that are greater than 0.
Consider a function:
36: fib :: {n:Int | 0 <= n} -> {v:Int | 0 <= v} 37: fib n = e
Intuitively, the type signature states that when checking the body e
we can assume that 0 <= n.
This is indeed the case with strict evaluation, as we are guaranteed
that n will be evaluated before e. Thus, either:
ndiverges and so we don't care abouteas we won't evaluate it, or,nis a non-negative value.
Thus, either way, e is only evaluated in a context where 0 <= n.
But this is not the case with lazy evaluation, as we may
well start evaluating e without evaluating n. Indeed, we may
finish evaluating e without evaluating n.
Of course, if n is evaluated, it will yield a non-negative value,
but if it is not (or does not) evaluate to a value, we cannot assume
that the rest of the computation is dead (as with eager evaluation).
That is, with lazy evaluation, the refinement type {n:Int | 0 <= n} actually means:
60: (n = _|_) || (0 <= n)
Keeping LiquidHaskell Honest¶
One approach to forcing LiquidHaskell to telling the truth is to force
it to always split cases and reason about _|_.
Lets revisit explode
70: explode = let z = 0 71: in (\x -> 2013 `divide` z) (foo z)
The case splitting prevents the cheerful but bogus prognosis that explode above was safe, because the SMT solver cannot prove that at the call to divide
75: z == 0 && (x = _|_ || (x >= 0 && x < z)) => z /= 0
But alas, this cure is worse than the disease. It would end up lobotomizing LiquidHaskell making it unable to prove even trivial things like:
_
82: {-@ trivial :: x:Int -> y:Int -> {pf: () | x < y} -> Int @-} 83: trivial x y pf = liquidAssert (x < y) 10
as the corresponding SMT query
87: (pf = _|_ || x < y) => (x < y)
is, thanks to the pesky _|_, not valid.
Terminating The Bottom¶
Thus, to make LiquidHaskell tell the truth while also not just pessimistically
rejecting perfectly good programs, we need a way to get rid of the _|_. That
is, we require a means of teaching LiquidHaskell to determine when a value
is definitely not bottom.
In other words, we need to teach LiquidHaskell how to prove that a computation definitely terminates.