Refinement Types via SMT and Predicate Abstraction

The “Hello World!” example for fancy type systems is probably the sized vector or list append function (“The output has size equal to the sum of the inputs!”). One the one hand, it is perfect: simple enough to explain without pages of code, yet complex enough to show off whats cool about dependency. On the other hand, like the sweater I’m sporting right now, it’s a bit well-worn and worse, was never wholly convincing (“Why do I care what the size of the output list is anyway?”)

Recently, I came across a nice example that is almost as simple, but is also well motivated: Okasaki’s beautiful Lazy Amortized Queues. This structure leans heavily on an invariant to provide fast insertion and deletion. Let’s see how to enforce that invariant with LiquidHaskell.

A large part of the allure of Haskell is its elegant, high-level ADTs that ensure1 that programs won’t be plagued by problems like the infamous SSL heartbleed bug.

However, another part of Haskell’s charm is that when you really really need to, you can drop down to low-level pointer twiddling to squeeze the most performance out of your machine. But of course, that opens the door to the #heartbleeds.

Can we have have our cake and eat it too?

Can we twiddle pointers and still get the nice safety assurances of high-level types?

Yesterday someone asked on Reddit how one might define GHC’s OrdList in a way that statically enforces its three key invariants. The accepted solution required rewriting OrdList as a GADT indexed by a proof of emptiness (which is essentially created by a run-time check), and used the new Closed Type Families extension in GHC 7.8 to define a type-level join of the Emptiness index.

Today, let’s see a somewhat more direct way of tackling this problem in LiquidHaskell, in which we need not change a single line of code (well.. maybe one), and need not perform any dynamic checks.

We’ve seen how, in the presence of lazy evaluation, refinements require termination. Next, we saw how LiquidHaskell can be used to prove termination.

Today, lets see how termination requires refinements.

That is, a crucial feature of LiquidHaskell’s termination prover is that it is not syntactically driven, i.e. is not limited to say, structural recursion. Instead, it uses the wealth of information captured by refinements that are at our disposal, in order to prove termination.

This turns out to be crucial in practice. As a quick toy example – motivated by a question by Elias – lets see how, unlike purely syntax-directed (structural) approaches, LiquidHaskell proves that recursive functions, such as Euclid’s GCD algorithm, terminates.

As explained in the last two posts, we need a termination checker to ensure that LiquidHaskell is not tricked by divergent, lazy computations into telling lies. Happily, it turns out that with very little retrofitting, and a bit of jiu jitsu, we can use refinements themselves to prove 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.

One crucial goal of a type system is to provide the guarantee, memorably phrased by Milner as well-typed programs don’t go wrong. The whole point of LiquidHaskell (and related systems) is to provide the above guarantee for expanded notions of “going wrong”. All this time, we’ve claimed (and believed) that LiquidHaskell provided such a guarantee.

We were wrong.

LiquidHaskell tells lies.

Most demonstrations for verification techniques involve programs with complicated invariants and properties. However, these methods can often be rather useful for describing simple but important aspects of APIs or programs with more humble goals. I saw a rather nice example of using Scala’s Shapeless library for preventing off-by-one errors in CSV processing code. Here’s the same, short, example rephrased with LiquidHaskell.

Hello again! Since we last met, much has happened that we’re rather excited about, and which we promise to get to in the fullness of time.

Today, however, lets continue with our exploration of abstract refinements. We’ll see that this rather innocent looking mechanism packs quite a punch, by showing how it can encode various ordering properties of recursive data structures.