Contextual Embeddings: Implementing Bound Variables through Instance Resolution
summary
Introduces contextual embeddings: an embedding that preserves typing contexts and uses the host's type-class instance-resolution based index reconstruction to compute De Bruijn indices automatically, removing unsafe coercions and producing a provable type-safe un-embedding. Implemented in Haskell with DataKinds and type classes, plus artifacts in Lean and Agda; supports modal and substructural (e.g. linear, Fitch-style) systems and reversible unembedding for superfold optimizations. Reports modest compile/run overheads and reusable, evaluated artifacts.
AI-written summary · about
chapters (7)
- 0:00Embedded DSLs with binders
- 2:07Golden binder representation
- 8:05Contextual embeddings solution
- 13:03Embeddings vs criteria
- 15:29Practical benefits and limits
- 16:11Summary and future
- 17:12Q&A
related talks
27mEmbedding by Unembedding
24mLocal Contextual Type Inference
23mTyped Embedding of miniKanren for Functional Conversion
27mCompositional Embeddings of Domain-Specific Languages
15mElaboration with First-Class Implicit Function Types
25mShallowly embedding type theories
25mRobust Dynamic Embedding for Gradual Typing
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs