All for one and none forall: Compiling polymorphic relations without(…)
summary
Claims a compiler pass for semiringKanren that removes type variables without monomorphization by compiling polymorphic relations into one canonical small relation plus expansion, using equality patterns and "large-enough" instance thresholds. Implements expansion and special-cases tiny types (e.g. disequality fails for num1 but always succeeds for num2), emits vanilla semiringKanren code, and proves correctness (sketch in paper, full proof separate). Works beyond arity two and supports open polymorphic recursion.
AI-written summary · about
chapters (8)
- 0:00Polymorphic relations intro
- 2:06Canren language overview
- 8:22Polymorphic sum swap
- 11:10Compiling with one array
- 17:15Edge cases in expansion
- 18:59Compiling polymorphic calls
- 20:23Compiling equal relation
- 21:46Conclusion
related talks
26mCommitting to the bit: Relational programming with semiring arrays and SAT solving
26mtypedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
14mMicroKanren in J
20mKanren Light
16mMulti-stage Relational Programming
14mRelational Synthesis for Pattern Matching
17mλKanren: Higher-order Logic Programming with Shallow Embedding
14mOn Fair Relational Conjunction