Compiling Haskell into C++ template metaprograms

After Lőri posted his C++ template meta-program solution to the 9-digit problem, Encsé asked me to help him understand it, being the first real-world metaprogram he's encountered. To help both him and myself, I rewrote, function-by-function, his code into Haskell.

This rewriting process was surprisingly straightforward, and the resulting code, while being in a very strict one-to-one correspondence with the original C++ code, was immensely more readable. So this, naturally, lead to the idea of a simple functional programming language that could be compiled into C++ compile-time metaprograms.

A couple of days later, I had a small accident and had to stay in bed for a week, which gave me plenty of time to throw together a proof-of-concept compiler from a Haskell-like language into C++ TMP.

And so MetaFun was born.

MetaFun is structured into three separate modules, one for parsing and typechecking the input language called Kiff (for Keep It Fun & Functional), one for unparsing C++ metaprograms, and the third one is, of course, the compiler itself. I plan to re-use the Kiff module whenever I come up with an idea for another new throwaway functional compiler.

The B Method for Programmers (Part 2)

In my previous post, I introduced the B method and showed the steps of writing a simple program for finding the n^th element of a sequence satisfying a given predicate p. While you may think the resulting program is correct, we can't just say so and be done with it. The whole point of the B method is that the resulting program can be formally proven correct.

The B software generates 69 so-called proof obligations for the code from the first part. These are assertions about the program actually behaving as specified. For example, let's look at PO69 which asserts that ll is correctly set. Recall first the relevant portion of the specification:

And the invariant of the implementation:

So what we have to prove is that given the preconditions, by the time the loop in the implementation terminates, the invariant makes sure ll is equal to its specified value. This is what's described (somewhat more verbosely) by the actual proof obligation below.

The B Method for Programmers (Part 1)

Last month, I had to use Atelier B, an implementation of the B method, for a university assignment. But what is the B method, and what does programming with B look like in practice?

I'm going to introduce B from the perspective of a traditional programmer. You can find documentation on the web, but most of it is from the viewpoint of designing complex state machines. However, B is also a Pascal-like language than can be used for imperative programming. The big added value of using B is that the resulting program can be proven to be correct. In fact, I first encountered B a year ago while working on my B.Sc. thesis, which was about deriving new correct programs from existing ones.

As for its theoretical backgrounds, B is based on the Hoare-Dijkstra model of imperative programming. I'm not going to delve into it; instead, let's look at a concrete example, and I'll guide you through the process of first writing a formal specification, then creating the implementation (this part), and then proving its correctness (in the next part).

Eliminating magic strings from ELisp's (interactive)

If you hate magic string API's as much as I do, you'll like this macro replacing Emacs's (interactive) declaration. It allows you to rewrite the following function definition:

into the much cleaner form below:

It currenty only supports :pos, :region and strings entered at the prompt, but the code is trivial to extend to other initializers.

Type inference for CLazy

CLazy now features Hindley-Milner type inference, the type calculus all the cool guys use. For example, given the following recursive definition of map:

the type inference engine of CLazy correctly reconstructs the following type signature:

Still to come: virtual functions like Haskell's typeclasses. The plan is to define abstract functions like (+ a) :: (fun a a a) and collect requirements for functions in the form of "this function has type (fun a b) as long as an overload for (+ a) exists".