Typed Embedding of miniKanren for Functional Conversion
Programming Languages
2025-11-04 v1
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.
Cite
@article{arxiv.2511.00740,
title = {Typed Embedding of miniKanren for Functional Conversion},
author = {Igor Engel and Ekaterina Verbitskaia},
journal= {arXiv preprint arXiv:2511.00740},
year = {2025}
}