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

## Two final versions and a Verasco release

- November 3, 2014

We have just submitted the final version of two papers, presenting the state of our recent research.

- A Formally-Verified C Static Analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie
- Verified compilation of floating-point computations, by Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond

## Lawvere theories and monads

- July 29, 2014
- Last updated on 2014/07/30

In this Agda file, I give an introduction to Lawvere theories and Monads. It's not exactly a "gentle" introduction because:

- I'm still trying to grok these things myself,
- I've to live up to my reputation of writing unfathomable gagaposts.

We'll start with the State monad and, briefly, a Tick monad. The game is the following: I'll present them syntactically -- through a signature -- and semantically -- through a collection of equations. I'll then show how the usual monad is related to this presentation.

## Paper draft: the Essence of Ornaments

- June 16, 2014

The Essence of Ornaments (pdf) is a draft of a new article, hoping to provide an accessible introduction to the theory of ornaments. Any feedback on the draft, in the comments or by email, is warmly welcome.

## Ornaments in practice

- May 27, 2014

I (Thomas Williams) am currently doing an internship with Pierre Dagand and Didier Rémy on ornaments, a way to relate datatypes sharing a common structure. Ornaments come from the scary world of dependent types, and the goal of my internship is to implement them in the more familiar setting of ML datatypes. We've produced a draft where we present how ornaments can be useful in practice in an ML-like programming language.

## Current (and future?) state of OCamlbuild parallelization

- May 18, 2014

A few days ago, Hugo Heuzard asked about the details of the problem with OCamlbuild's parallelism today on mantis: PR#5754. My mantis comment quickly grew into the blog post below.

I worked last September on better parallelization for OCamlbuild, but didn't finish the thing (I couldn't get something mergeable in time for ICFP) and got distracted with tons on other things to do since. I just uploaded the state of my branch:

https://github.com/gasche/ocaml/tree/ocamlbuild-indirect-style

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

- April 18, 2014

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

- April 1, 2014

## Try Mezzo in your browser!

- March 24, 2014

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

- March 11, 2014

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

- March 3, 2014

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.