In an ideal world we would directly express the operational semantics or type judgements of a programming language as a high-level executable semantics. We could then perform tasks like program synthesis or type inference/type inhabitation by writing queries with variables representing “holes” in a program or a type, and letting an advanced reasoning system efficiently fill in those holes. This is the promise and challenge of relational programming, a pure form of constraint logic programming. Over the past dozen years we and our colleagues have experimented with this approach, using the relational programming language miniKanren (http://minikanren.org/). In the past two years we have applied a variety of optimizations and heuristics to the relational interpreters we use to encode an operational semantics, speeding up some synthesis queries by 9 orders of magnitude. This speed up allows us to synthesize small but interesting higher-order and recursive Racket programs, as shown in our 2017 ICFP Pearl ‘A unified approach to solving seven programming problems’, Byrd, Ballantyne, Rosenblatt, Might.

In this tutorial we will show how we write and extend an interpreter for a Turing-complete subset of Racket as a relation in miniKanren, and then use this relational interpreter for program synthesis. Participants will follow along in the Racket version of miniKanren, and will write their own recursive miniKanren relations, including their own relational interpreter (and relational type inferencer, time allowing). We will also discuss the philosophy of relational programming, and describe open research problems in using relational interpreters for program synthesis. We assume participants have a basic knowledge of functional programming. Familiarity with writing simple interpreters will be helpful, but is not required. No knowledge of miniKanren, relational/logic programming, or program synthesis is assumed.