typedKanren: Statically Typed Relational Programming with Exhaustive Matching in(…)
summary
A statically typed embedding of miniKanren in Haskell that implements disequality constraints and a variant of relational matching with static exhaustiveness checks, so pattern coverage failures surface at compile time rather than at search. Boilerplate for user types is generated with GHC.Generics plus Template Haskell, and several example relations are shown; the prototype is compared to other miniKanren implementations for runtime behavior and tradeoffs (work in progress).
AI-written summary · about
chapters (4)
- 0:00Introduction to typedKanren
- 12:17Core concepts
- 17:45Practical examples
- 27:39Future optimizations & Q&A
related talks
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
47mLogic Programming à la Carte
59mKeynote: Dependently-Typed Haskell
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
23mPartial Type Constructors in Practice
44mRevisiting pattern match overlap checks in Haskell
01h 37mGHC's Renamer
49mMaking sense of the Haskell type system