let (rec) insertion without Effects, Lights or Magic

TL;DR

This paper presents a denotational semantics for let(rec)-insertion in program generation, enabling implementation in plain OCaml without effects, and demonstrates its application in MetaOCaml.

Contribution

It provides the first effect-free denotational semantics for let(rec)-insertion, facilitating its implementation in standard OCaml.

Findings

Successfully formalized let(rec)-insertion without effects

Implemented the semantics in MetaOCaml

Enhanced understanding of code generation with recursive definitions

Abstract

Let insertion in program generation is producing code with definitions (let-statements). Although definitions precede uses in generated code, during code generation `uses' come first: we might not even know a definition is needed until we encounter a reoccurring expression. Definitions are thus generated `in hindsight', which explains why this process is difficult to understand and implement -- even more so for parameterized, recursive and mutually recursive definitions. 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.