metaKanren: miniKanren Program Synthesis, Relationally

Abstract

Relational interpreters, interpreters written for programming languages as mathematical relations, have been studied for at least over a decade. However, while relational interpreters are mostly written in miniKanren, a relational language where programs are mathematical relations, the interpreted language tends to be non-relational. This dissertation presents metaKanren, a purely relational miniKanren-like language, and relational interpreter implemented as a deep embedding for metaKanren. We also construct a relational interpreter for a minimal relational language as a shallow embedding and point out the limitation of a shallow embedding, further emphasizing the need for a deep embedding. We show how one can perform program synthesis of miniKanren programs using our relational interpreter for metaKanren. We also show how to extend metaKanren and its relational interpreter to handle datatype constraints. Finally, we also show how metaKanren can be made fully metacircular, and precisely point out the problems in building a metacircular interpreter for miniKanren. This dissertation argues that it is feasible and useful to build a metacircular relational interpreter for miniKanren