Gagallium

With Pierre Boutillier, we have been working on a new Coq tactic lately, called invert. From my point of view, it started as a quest to build a replacement to the inversion tactic. inversion is a pain to use, as it generates sub-goals with many (dependent) equalities that must be substituted, which force the use of subst, which in turns also has its quirks, making the mantra inversion H; clear H; subst quite fragile. Furthermore, inversion has efficiency problems, being quite slow and generating big proof terms. From Pierre's point of view, this work was a good way to implement a better destruct tactic, based on what he did during an internship (report in French (PDF)).

In a previous post I described two extensions to CompCert's memory model that I implemented during my visit at Gallium. Another thing I have been working on is non-determinism and sequence points in C. As some of you will know, the evaluation order of expressions is not specified by the C standard. This allows a compiler to pick its preferred evaluation strategy. To allow a compiler also to delay side-effects, and to interleave evaluation, the allowed non-determinism is slightly restricted.

Let me start this post by briefly introducing myself: I am a PhD student at the Radboud University Nijmegen, the Netherlands, working on developing a formal semantics for the C11 standard in Coq. Between January and March, I have been a guest at Gallium (many thanks to Xavier Leroy for inviting me!). During this stay I have been able to do some CompCert hacking, and to get more experience with CompCert and its semantics.

For my 25th birthday, my (awesome) friends offered me a new gadget, a Nexus 7 tablet. Of course, my first impulse was to install Debian on it. That seemed a little bit excessive; I tried to be reasonable, and decided to first try to run OCaml programs on the tablet.

I successfully managed to set up Unison on the tablet, and used it to synchronize documents between the tablet and my home computer. At the end of this blog post, hopefully you'll be able to do the same!

Sometimes using OCAMLRUNPARAM="b" returns a disappointingly unhelpful backtrace, because the program you're trying to debug has a non-trivial usage of exceptions that destroys the backtrace information you were expecting. Here is a new library that should solve this problem, by allowing you to reliably register backtraces. Read more for the source, and the juicy internal details: weak tables, semi-manual garbage collection logic, and an optional change to the OCaml runtime to improve the library performances.

Batteries contributors recently started a new discussion on the Enum module, whose purpose is to provide an good intermediate representation for conversion between data-structures, but whose implementation is perceived as too complicated and not well-understood enough. Going back to fundamentals (forgetting about half the features of Enum), what is the ultimate intermediate traversal interface?

There are two obvious choices in an effectful setting: a generator, that is a "next-element" function of type ('a -> unit) that generates the next element each time it is called, or an exception to signal end of input; or an iterator, a fold-function of type ('a -> unit) -> unit, that iterates a consumer function through all elements of the list.

Both are suitable as an abstract representation of any sequence (the second is precisely the basis for Simon Cruanes' Sequence library), and their are at opposite ends of the control spectrum: generators give control to the consumer of the sequence (she decides when to call the generator function), while iterators give control to the producer of the sequence (she decides when to call the iterated function). It's easy to transform a structure into a iter (to_iter), or to build a structure from a next (of_next), because you have the control. But as a library writer, you should also write the without-control conversions (of_iter and to_next), despite them being slower and harder to implement, so that your users can live the easy in-control life!

Finally, continuation capture is a well-known technique to invert control, letting you write code in "direct style", as if you were in control, when you're not. In this post, I will demonstrate how you can start from a conversion function that has control and, by systematic source-to-source transformations of conversion to continuation-passing-style (CPS) and defunctionalization, obtain a conversion function that works without the control.

The n-ary cartesian product (on lists) returns the cartesian product of a list of list, rather than just two lists: product [[1]; [2;3]; [4;5]] is [[1;2;4]; [1;2;5]; [1;3;4]; [1;3;5]]. The result is the empty list as soon of one of the input lists is empty. But what is the product of the empty list of lists?

I first answered this question with mathematical considerations that, while working on set theory, will fell familiar to anyone having worked with dependent types. But there is a direct, much simpler answer in the code.

A quick and dirty blog post about the -documentation option of ocamlbuild, how to use and understand its output.

I am pleased to announce the first official release of PPrint, an OCaml library for pretty-printing textual documents.

During the second part of my internship this summer, I worked on a test implementation for a new data structure in OCaml : Hash Array Mapped Tries (HAMT). I did not have the time to finish it, but I now have a usable and quite complete version, still to be more documented but already available at http://gitorious.org/ocaml-hamt.

On this article, I will quickly explain the principles and the use cases of this structure, and I will expose a few details of my implementation in OCaml.