telling-lies-old.lhs

---
layout: post
title: "LiquidHaskell Caught Telling Lies!"
date: 2013-11-19 16:12
comments: true
external-url:
categories: termination
author: Niki Vazou
published: false
demo: TellingLies.hs
---

If you used liquidHaskell lately, you may have noticed some type errors that
just make no sense.
Well, that is not a bug, but a ... **termination checker** failing to prove that
your function terminates.

LiquidHaskell, *by default*, performs a termination check while verifying your
code.
Of course the tool would be useless if it required all your functions
to terminate.
Instead, it just requires that non-terminating functions return unrefined
results.
We will shortly explain when and how one can turn off termination checking while preserve
sound type checking.
To do so, we should start by explaining why termination is requied. 

<!-- more -->

\begin{code}
module TellingLies where

import Prelude  hiding (repeat)
import Language.Haskell.Liquid.Prelude (liquidAssert)
\end{code}

Why is Termination Analysis Required
-------------------------------------

Consider a no-terminating function:

\begin{code}
{-@ foo :: Int -> {v:Int | false} @-}
foo     :: Int -> Int
foo n   = foo n
\end{code}

According to the *partial correctness property*
the type signature for `foo` means that any
value `foo` returns will satisfy the result refinement
`false`. 
Since `foo` never returns, 
it can return *none* value, thus it trivially satisfies its
type.

Now, in an environment where `false` (i.e., `foo`'s result)
exists, liquidHaskell can prove anything, 
even the contradiction `0==1`:

\begin{code}
prop = liquidAssert ((\_ -> 0==1) (foo 0))
\end{code}

This is totally valid under *eager* evaluation, where
to execute the assertion one should first compute the argument
`foo 0` which never returns.
But, it is not valid under haskell's *lazy* semantics
where execution ignores the unused argument, and fails.

From the above discussion we see that partial correctness is not enough to
verify Haskell's lazy code.
To restore soundness we require *total correctness*, or
that each function terminates.
This explains why termination checking is set as default to liquidHaskell (as is
in many other verifiers, like Coq or Agda.)

Turning off Termination Checking
--------------------------------

Of course, you cannot prove termination of functions like `repeat`

\begin{code}
{-@ repeat :: a -> [a] @-}
repeat     :: a -> [a]
repeat a   = a : repeat a
\end{code}

Instead, you can mark `repeat` as `Lazy` to disable termination for these
functions:
\begin{code}
{-@ Lazy repeat @-}
\end{code}

But, be careful!
By marking a function as `Lazy` *you* also guarantee that *the result type
cannot contain inconsistencies*.
In our previous example, liquidHaskell typechecked the unsafe `prop`, just
because we marked `foo` (who's return type contains inconsistency) as `Lazy`
\begin{code}
{-@ Lazy foo @-}
\end{code}

Even though it is hard to decide if a type can contain inconsistencies,
trivially *unrefined types* (or types refined to `true`) cannot ever be resolved
to `false`.
In other words, it is always safe to mark as `Lazy` functions with unrefined
result.

\begin{code}Finally, you have the option to totally disable termination checking, using the `no-termination` flag:
{-@ LIQUID "--no-termination" @-}
\end{code}


Prevent liquidHaskell from Telling Lies
---------------------------------------

In this post, we saw why termination is required for sound type checking and when
it is safe to deactivate it.
But still, we didn't discuss how to prevent the tool from telling lies, i.e., how
to actually prove termination.
Turns out that liquidHaskell is powerful enough to prove
termination on a great number of functions, but this is a topic of another post.