Embedding by Unembedding
summary
Presents a concrete recipe that turns a tagless‑final (HOAS) interface into de Bruijn terms via embedding by unembedding, exposing when HOAS fails and how to fix it. Provides an NV wrapper, lifting functions and a variables type class that automate environment reindexing. Demonstrates two full case studies: CTS incremental lambda (initial run has overhead but Template Haskell optimizations remove it) and Hobbit lenses (first embedding of a bidirectional language with binders). Code and artifacts are available and reusable.
AI-written summary · about
chapters (15)
- 0:00Embedding languages by program manipulation
- 0:21Embedding and advanced semantics
- 3:13Incremental and bidirectional programming
- 3:35Limitations of HOAS for binders
- 8:09De Bruijn indices and HOAS combination
- 9:31Recipe for embedding by unembedding
- 10:36Recipe applied to Lambda calculus
- 13:25HOAS syntax to advanced semantics
- 16:37NV wrapper and lifting functions
- 19:27Incremental Lambda calculus case study
- 20:52Unembedding performance results
- 21:14Hobbit higher-order lens language
- 22:20Future directions and open questions
- 22:42Summary and conclusion
- 23:05Q&A
related talks
19mContextual Embeddings: Implementing Bound Variables through Instance Resolution
23mTyped Embedding of miniKanren for Functional Conversion
31mDependent tagless final
25mShallowly embedding type theories
27mCompositional Embeddings of Domain-Specific Languages
23mMacro-embedding Compiler Intermediate Languages in Racket
35mPractical Normalization by Evaluation for EDSLs
29mAnnotating Deeply Embedded Languages