A blog at Gallium: informal posts about research, programming practice, OCaml development, and general ramblings.

Rss feed

The 6 parameters of (’a, ’b, ’c, ’d, ’e, ’f) format6

The infamous format6 type is the basis of the hackish but damn convenient, type-safe way in which OCaml handles format strings:

Printf.printf "%d) %s -> %f\n"
  3 "foo" 5.12

The first argument of printf in this example is not a string, but a format string (they share the same literal syntax, but have different type, and there is a small hack in the type-inference engine to make this possible). It's type, which you can get by asking ("%d) %s -> %f\n" : (_,_,_,_,_,_) format6) in a toplevel, is a mouthful (and I renamed the variables for better readability):

(int -> string -> float -> 'f, 'b, 'c, 'd, 'd, 'f) format6

What do those six arcane parameters mean? In the process of reviewing Benoît Vaugon's work on using GADTs to re-implement format functions, I've finally felt the need (after years of delighted oblivion) to understand each of those parameters. And that came after several days of hacking on easier-to-understand ten-parameters GADT functions; hopefully most of our readers will never need this information, but the probability that I need to refresh my memory in the future is strong enough for me to write this blog post.


OCaml 5.00


Try Mezzo in your browser!

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.

An original programming pattern in Mezzo

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.


Bove-Capretta, Reloaded

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 much shorter proof of a recent result on a conjecture by Erdős

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.


Papers, papers, papers

We're now well past the autumn season, but paper leaves are still stacking up in Gallium. Here are a few drafts we've produced in these last few months. You may be interested in having a look, and of course we warmly welcome feedback.


Experiment: OCaml patch review on github.com/ocaml/ocaml

TL;DR: During the six next months, we will follow pull requests (PR) posted on the github mirror of the OCaml distribution, as an alternative to the mantis bugtracker. This experiment hopes to attract more people to participate in the extremely helpful and surprisingly rewarding activity of patch reviews.


The Chinese restaurants of Gallium

As some of you may know, we have a shared office in Paris. This means on Wednesdays and Thursdays, a chunk of the team works at Place d'Italie. For those of you who don't know the area, Place d'Italie is on the fringe of Paris' Chinatown. Two members of the team live (or have been living) in the area, meaning that we developed quite a flair for good Chinese restaurants (see the (incomplete) map of the places I have tried out for instance).

We thus happily present our list of favorite restaurants. These are not classy, well-designed, western-looking restaurants. They're rather the obscure, hidden, ridiculously small restaurants filled with Chinese people and where the waitresses barely speak French and the chef shouts orders in Chinese from the kitchen. Most of these restaurants serve one of the eight major Chinese cuisine styles, and have relatively small menus. In case you're visiting us, or just want to try out any of these, we hope that the list may be useful!


Pattern synonyms, arbitrary patterns as expressions

A few weeks^Wmonths ago now, Pierre Dagand asked me about pattern synonyms for OCaml. I told him I had a design conundrum of the worst kind with pattern synonyms: a choice between two incompatible option, with none being better than the other. Synonyms that capture the pattern language, or restricted synonyms that can be used as expressions? Well, it turns out we can have both.