2013-12-02-getting-to-the-bottom.lhs

---
layout: post
title: "Getting To the Bottom"
date: 2013-12-02 16:12
comments: true
external-url:
categories: termination
author: Ranjit Jhala, Niki Vazou
published: true 
demo: TellingLies.hs
---

[Previously][ref-lies], 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.

<!-- more -->

\begin{code}
module GettingToTheBottom where
\end{code}

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.

\begin{code} Recall that the refinement type:
{v:Int | 0 <= v}
\end{code}

is supposed to denote the set of `Int` values that are greater than `0`.

\begin{code} Consider a function:
fib :: {n:Int | 0 <= n} -> {v:Int | 0 <= v}
fib n = e
\end{code}

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). 

\begin{code} That is, with lazy evaluation, the refinement type `{n:Int | 0 <= n}` *actually* means:
(n = _|_) || (0 <= n)
\end{code}

Keeping LiquidHaskell Honest
----------------------------

One approach to forcing LiquidHaskell to telling the truth is to force 
it to *always* split cases and reason about `_|_`.

\begin{code} Lets revisit `explode`
explode = let z = 0
          in  (\x -> 2013 `divide` z) (foo z)
\end{code}

\begin{code}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` 
    z == 0 && (x = _|_ || (x >= 0 && x < z))  => z /= 0
\end{code}

But alas, this cure is worse than the disease. 
It would end up lobotomizing LiquidHaskell making it unable to prove even trivial things like:

\begin{code}_
{-@ trivial    :: x:Int -> y:Int -> {pf: () | x < y} -> Int @-}
trivial x y pf = liquidAssert (x < y) 10
\end{code}

\begin{code}as the corresponding SMT query
    (pf = _|_ || x < y) => (x < y)
\end{code}

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.

[ref-lies]:  /blog/2013/11/23/telling_lies.lhs/