Typed Embedding of miniKanren for Functional Conversion

TL;DR

This work tackles high overhead in relational program synthesis by introducing a typed, tagless-final embedding of miniKanren in Haskell, augmented with automatic determinism analysis. It refines the previous functional conversion by avoiding a monolithic Term and explicit generator threading, enabling type-safe, composable relations and extensible interpreters. The approach preserves the performance gains of prior work while improving developer experience and safety, particularly for semi-deterministic directions. Experiments show the new converter matches the old in nondeterministic cases and delivers speedups when determinism can be exploited. Overall, the paper advances safe, scalable, and extensible relational programming in statically typed languages.

Abstract

Relational programming enables program synthesis through a verifier-to-solver approach. An earlier paper introduced a functional conversion that mitigated some of the inherent performance overhead. However, the conversion was inelegant: it was oblivious to types, demanded determinism annotations, and implicit generator threading. In this paper, we address these issues by providing a typed tagless-final embedding of miniKanren into Haskell. This improvement significantly reduces boilerplate while preserving, and sometimes enhancing, earlier speedups.

Figures (6)

• Figure 1: miniKanren syntax
• Figure 2: Normalized miniKanren syntax
• Figure 3: Generated Term type
• Figure 4: Execution time (in nanoseconds) of $add$ relation in two nondeterministic directions, requesting first $n$ (x-axis) results. Log plot.
• Figure 5: Execution time (in nanoseconds) of $add$ relation in four deterministic directions, with parameter $a$ on x-axis. Log plot.