Getting To the Bottom

Posted by Ranjit Jhala and Niki Vazou Dec 2, 2013

Tags: termination

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:

  1. n diverges and so we don’t care about e as we won’t evaluate it, or,
  2. n is 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.