Parametric HOAS with first-class modules

One of the first choice to make when starting the development of a compiler, or any program manipulating syntax with binders (e.g. programs with functions and variables), is how to represent these terms. Some specialized programming languages, like Beluga, have built-in facilities for this. But if you choose a general-purpose one, like OCaml, then you have plenty of choices: Named terms, De Bruijn indices, Locally nameless, Higher-order abstract syntax (HOAS)… each with their idiosyncrasies, inconvenients etc. This issue is pervasive in PL research and almost formed a subfield of itself. If you are interested, there is a wealth of literature on the topic; a documented discussion happened on LtU some years back (already), which is probably a good starting point, although of course some has happened since then.

Today I will be looking at implementing in OCaml one of the most recent and praised ones: Parametric HOAS (PHOAS). For some reason that I detail hereafter, the traditional way of implementing PHOAS can be cumbersome, and I propose an alternative here, which happens to be one of my very first uses of first-class modules.

Escaping continuations

Beta had a funny joke at POPL last year; he said: “you exit a monad like you exit a building on fire: by running”. I recently got myself in the stressful situation of being trapped in a monad—the continuation monad—but without a possibility to “run”. There an exit nonetheless: just jump out! This is the (short) story of an escape.