Gagallium

This is just to let you know that you can now try Mezzo online! Mezzo runs in your browser, thanks to js_of_ocaml and a few hacks to glue the type-checker to the web interface. There’s a few examples, and you can type-check and/or interpret your programs (currently, only the graph traversal actually does something observable).

There’s a lot of room for improvement (currently, all files are loaded during initialization, for instance), but it believe it’s nice enough already that I can release it. It is known to work in the latest versions of Firefox, Chrome and Internet Explorer.

Lately, it seems all I've been doing is writing. There's been that paper about the implementation of Mezzo, which I'm supposed to push out at some point. There's that ICFP submission (blog post pending) which we've been writing with some other cool kids from the lab. That's not counting the various presentations, research statements, and other misc. documents that I've been busy with...

Last week, I was (again!) writing, this time working on my part for a journal version of our ICFP paper, and I was trying to write a small tutorial with longer examples and a better introduction to Mezzo. After explaining tail-recursive concatenation for the n-th time, I decided to try out explaining a new example. Here's the result.

The example is about an interesting programming pattern in Mezzo, which I dub "control-flow inversion". The idea is not new: we've been using it for iterators, but is was somehow buried under the details of how iterators work. The present blog post tries to present it in a more self-contained way. It somehow showcases both the strengths and weaknesses of Mezzo as it stands right now. Hopefully we'll improve the shortcomings soon.

The following construction is based upon a note scribbled by Conor McFermat^W McBride on a draft of my PhD thesis a few months ago. Upon seeing an earlier version of this file, Stevan Andjelkovic (aka Mr Freemonadic) urged me to borrow one of his free monads to write my recursive functions.

The tl;dr: we intensionally characterise a class of Bove-Capretta predicates (using a custom-made universe of datatypes) with the guarantee that these predicates are "collapsible", ie. have no run-time cost. We then write a generic program that computes such a predicate from the recursive definition of a function. Using this framework, we can write a recursive function without being bothered by that administrative termination-checker and prove its termination after the fact.

A recent breakthrough by Boris Konev and Alexei Lisitsa has been described as “too big for humans to check” due to its use of a SAT solver on a large instance. I disagree with this characterization, and will try to explain why.