ICFP/SPLASH 2025 (series) / Haskell 2025 (series) /  Haskell 2025 / typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell
typedKanren: Statically Typed Relational Programming with Exhaustive Matching in HaskellRemote
We present a statically typed embedding of relational programming (specifically a dialect of miniKanren with disequality constraints) in Haskell. Apart from handling types, our dialect extends standard relational combinator repertoire with a variation of relational matching that supports static exhaustiveness checks. To hide the boilerplate definitions and support comfortable logic programming with user-defined data types we use generic programming via GHC.Generics as well as metaprogramming via Template Haskell. We demonstrate our dialect on several examples and compare its performance against some other known implementations of miniKanren.
| slides (slides.pdf) | 251KiB | 
Fri 17 OctDisplayed time zone: Perth change
Fri 17 Oct
Displayed time zone: Perth change
| 16:00 - 17:30 | |||
| 16:0020m Talk | [CANCELED] Adaptive Search Synthesis as a Recursion Scheme Haskell Lucas Bang Harvey Mudd College, Xuehuai He Yale University, Eli Pregerson Stony Brook University, Jimmy Chen Stanford University, Emma Gandonou Pomona College | ||
| 16:2020m Talk | Derive class instances topdown and derive ttg automatically Haskell Song Zhang None | ||
| 16:4020m Talk | Machine Learning Primitives as Algebraic Effects Haskell | ||
| 17:0020m Talk | typedKanren: Statically Typed Relational Programming with Exhaustive Matching in HaskellRemote HaskellPre-print File Attached | ||
| 17:205m Day closing | Chair's report Haskell | ||
