let (rec) insertion without Effects, Lights or Magic
Oleg Kiselyov (Tohoku University, Japan), Jeremy Yallop (University, of Cambridge, UK)

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Advanced Software Engineering Methodologies
