Typed Embedding of miniKanren for Functional Conversion
summary
A typed tagless-final embedding of miniKanren into Haskell replaces the old untyped deep AST with generated logic-term types (via Template Haskell), enabling typed tagless-final embedding, eliminating the monolithic Term and making generators implicit generator passing based on Haskell types. The pipeline normalizes the EDSL into the existing functional-conversion backend that emits deterministic functions returning lazy streams preserve completeness of nondeterministic results; the conversion runs and yields the earlier speedups, embedding alone does not.
AI-written summary · about
chapters (16)
- 0:00Typed miniKanren embedding intro
- 0:21Functional conversion importance
- 1:25Verifiers and solvers from relations
- 2:28Performance bottlenecks
- 3:13Specialization for faster miniKanren execution
- 4:57Eliminating unifications
- 6:03Haskell embedding
- 8:55Logical variables with generators
- 9:58Limitations of untyped embedding
- 11:48Requirements for typed embedding
- 13:12Designing typed embedding
- 15:00Final tagless style
- 16:22Implementing interpreters
- 17:04Normalization pipeline
- 18:29Typed embedding benefits
- 19:16Q&A
related talks
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
22mA Case Study in Functional Conversion and Mode Inference in miniKanren
20mKanren Light
17mλKanren: Higher-order Logic Programming with Shallow Embedding
27mEmbedding by Unembedding
40mminiKanren Philosophy
31mDependent tagless final
16mMulti-stage Relational Programming