typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell

TL;DR

typedKanren introduces a statically typed relational programming framework in Haskell that supports exhaustive matching and leverages generic programming and metaprogramming for ease of use, with demonstrated performance benefits.

Contribution

It presents a novel statically typed embedding of relational programming in Haskell with exhaustive matching and automation features, enhancing safety and usability.

Findings

Supports static exhaustiveness checks in relational matching

Uses GHC.Generics and Template Haskell for boilerplate reduction

Demonstrates competitive performance against existing miniKanren implementations

Abstract

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.