let (rec) insertion without Effects, Lights or Magic
summary
Claims a denotational semantics for let(rec)-insertion that avoids delimited control and other effects, models insertion as composable annotations (sticky notes) that merge when code combinators combine, and handles parameterized and mutually recursive definitions. Implements the idea in plain OCaml/MetaOCaml, replacing previous effectful implementations with a small change (about 20 lines added) to an existing interpreter, and reports that the approach works and simplifies the interface and implementation.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:05Paper overview
- 3:13Code generation
- 8:05Composition limits
- 9:51Let insertion purpose
- 12:36Why definitions first
- 17:32Let insertion without effects
- 21:43Recursive definitions
- 25:34Conclusion
- 26:37Q&A
related talks
15mElaboration with First-Class Implicit Function Types
15mLatent Effects for Reusable Language Components
14mA Limited Case for Reification by Type Inference
35mFlattening Meets Effects: A Surprising Connection
28mImplicit modules, a middle step towards modular implicits
28mOne Weird Trick to Untie Landin's Knot
15mLiberating Merges via Apartness and Guarded Subtyping
27mLightweight Semantics Engineering with Redex