typedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
summary
typedKanren is a statically typed embedding of a miniKanren dialect in Haskell that implements disequality constraints, GHC.Generics-derived Logical instances and Template Haskell helpers to remove boilerplate. It adds a prism-based matching API and an exhaustive relational matching combinator (matchE') that verifies at compile time that all constructors are handled. The implementation runs fair search via an explicit stream monad, works functionally both forward and backward, and benchmarks slower than Racket’s faster-miniKanren, roughly on par with klogic and slightly behind OCanren, with performance degrading on larger tree-like examples.
AI-written summary · about
chapters (9)
- 0:00Introduction to typedKanren
- 3:10Core features in Haskell
- 8:07Type class and Go monad design
- 13:07State, constraints and search
- 15:14Relational matching with prisms
- 17:41Exhaustive relational matching
- 19:09Performance evaluation
- 21:14Conclusion and future work
- 22:18Q&A
related talks
23mTyped Embedding of miniKanren for Functional Conversion
14mRelational Synthesis for Pattern Matching
20mKanren Light
17mλKanren: Higher-order Logic Programming with Shallow Embedding
16mMulti-stage Relational Programming
24mAll for one and none forall: Compiling polymorphic relations without(…)
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
22mA Case Study in Functional Conversion and Mode Inference in miniKanren