We have earlier presented an interface for let(rec) insertion -- i.e. for generating (mutually recursive) definitions. We demonstrated its expressiveness and applications, but not its implementation, which relied on effects and compiler magic.
We now show how one can understand let insertion, and hence implement it in plain OCaml. We give the first denotational semantics of let(rec)-insertion, which does not rely on any effects at all. The formalization has guided the implementation of let(rec) insertion in the current version of MetaOCaml.
Not only we have shown what let-insertion actually means; Not only we have developed the first formal model that uniformly treats let-, letrec- and mutually-letrec--insertion, without any continuation or state effects. We have also simplified the previously proposed interface for generating mutually recursive definitions. In particular, memoization comes out naturally; the explicit memoizing fixed-point combinator is no longer needed. The simplification has lead to the straightforward implementation, in the current MetaOCaml.
Joint work with Jeremy Yallop.
talk.pdf [158K]
Slides of the talk at PEPM 2022 (recorded)
Embedded two-staged DSL with let-, letrec- and mutual-letrec--insertion in plain, pure OCaml
Generating Mutually Recursive Definitions
Derivation and illustration of the interface for mutually recursive
let-insertion (simplified in the present work)
The implementation also serves as an executable denotational semantics of two-level staging with (mutually recursive) let-insertion. It has been used in the above paper to verify all semantic calculations, for all the examples.
The implementation takes form of a two-stage DSL, embedded into OCaml in the tagless-final style.
Unfortunately, currently MetaOCaml can only build recursive groups
whose size is hard-coded in the generating program. The general case
requires something other than quotation, and seemingly weakens static
guarantees on the resulting code. We describe the challenges and
propose a new language construct for assuredly generating binding
groups of arbitrary size -- illustrating with a collection of examples
for mutual, n-ary, heterogeneous, value and polymorphic
recursion.
Joint work with Jeremy Yallop.
simple.ml [10K]
Code for the most of the paper,
including the
generation of recursive (but not mutually recursive) definitions.
Generation of the recursive definitions is already supported by
MetaOCaml, as it turns out.
dummy_genletrec.ml [6K]
The prototype of the genletrec
primitive proposed in the paper. It is a mere
a prototype; the complete implementation requires a revision of
MetaOCaml (which has since been carried out).
token.mli [<1K]
The token interface for the
example of generating a finite state recognizer as a group of
mutually recursive functions, from the FSM description. The example
is implemented using the genletrec prototype.
let (rec) insertion without Effects, Lights or Magic
The improved and much simplified interface,
implemented in MetaOCaml (BER N111)