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.
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.
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!
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.
We can now demonstrate the Fix library, used to compute arbitrary fixpoints, by implementing variance computation for the toy type system of our first post.
In this post I will present a simple language of type definitions, and use it as an example use-case for the Pprint library.