Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell

Nikolai Kudasov, Artem Starikov

TL;DR

A statically typed embedding of relational programming (specifically a dialect of miniKanren with disequality constraints) in Haskell that extends standard relational combinator repertoire with a variation of relational matching that supports static exhaustiveness checks.

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.

typedKanren: Statically Typed Relational Programming with Exhaustive Matching in Haskell

TL;DR

A statically typed embedding of relational programming (specifically a dialect of miniKanren with disequality constraints) in Haskell that extends standard relational combinator repertoire with a variation of relational matching that supports static exhaustiveness checks.

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.
Paper Structure (21 sections, 1 figure)

This paper contains 21 sections, 1 figure.

Table of Contents

  1. Introduction
  2. Related Work
  3. Contribution
  4. Core
  5. Logical Types and Unification Terms
  6. Unification of Terms
  7. The Goal Monad
  8. Example
  9. Exhaustive Matching
  10. Prisms as First-Class Patterns in Haskell
  11. Changing Types with Prisms
  12. Eliminating Alternatives with Prisms
  13. Typed Relational Matching
  14. Exhaustive Relational Matching
  15. Patterns Tagged with Exhaustiveness Information
  16. ...and 6 more sections

Figures (1)

  • Figure 1: Preliminary benchmark results. The benchmarks were executed on an ASUS ZenBook 15 with an AMD Ryzen 7 7735U CPU, 16GB of memory, using NixOS, Linux 6.10.2.