Typed Embedding of miniKanren for Functional Conversion

TL;DR

This paper presents a typed, elegant embedding of miniKanren into Haskell that improves performance and reduces boilerplate in relational programming for program synthesis.

Contribution

It introduces a typed, tagless-final embedding of miniKanren into Haskell, addressing previous inefficiencies and complexities in functional conversion.

Findings

Significantly reduces boilerplate code.

Maintains or improves performance speedups.

Provides a typed, elegant embedding approach.

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.