Demo article: This is it

The promise of relational programming

Relational interpreters have no notion of the direction of a computation: to say they run “forward” or “backward” is a temporary concession for traditional programmers learning relational programming.

There is only one direction about which a relational interpreter cares: toward the solution(s).

Consider the possibilities that emerge:

1. One can write an evaluator for a traditional programming language in a purely relational style, and generate programs that evaluate to specific outputs.

2. In the same vein as above, one can write a partial progarm with “unknowns” and provide a specification for the output using those same unknowns.

3. If one were to write a proof “checker” in a purely relational style, and run it “backward,” it immediately and necessarily becomes a proof generator.

[Of course, we have already implemented and tested all three of these.]

The goal: The essence of relational programming

Relational programming is extremely expressive and very powerful.

Yet few programmers are even aware it exists,

Even fewer understand the “magic” of how it works.

The goal of this article is to hint at the power of relational programming and then to strip away that magic by developing a concise (one-page) implementation of a relational interpreter for miniKanren.

(miniKanren is currently the most popular relational programming language.)

We will do so by creating microKanren: a minimalist core atop of which miniKanren is merely syntactic sugar.

In the end, the biggest surprise is not how relational programming is implemented.

It’s how it is not implemented:

1. relational interpreters do not need continuations; and

2. relational interpreters do not need backtracking.

Rather, for the implementation of a relational interpreter:

1. the big hammer is unification;

2. the structural timber is a monad;

3. and the nails that hold it all together are higher-order functions.

In the interest of increasing accessibility, we will even dispense with the monadic interpretation in our initial development, directly replacing monads with streams.

Since streams can be implemented with higher-order functions, it means that microKanren can be embedded in any language that supports closures via lambda.

In fact, in the end, we’ll present an even-more-minimalist implementation of microKanren (nanoKanren?) that does exactly that: the only language feature it expects are lambda and cons.

An analogy to algebra

High-school algebra makes a good analogy for relational programming.

In algebra, one might write an equation like:

\( y = 3x^2 + 4 \)

By convention, we tend to view \(x\) as an input and \(y\) as the output.

Traditional programmers drop in a value of \(x\) to find the value of \(y\).

Relational programmers can drop in a value of \(y\) to find the value(s) of \(x\).

Or, they can ask for all pairs of \(x\) and \(y\) for which the equation holds.

The analogy can be made even more exact.

A traditional programmer might think of the equation in terms of a function \(f\), which creates an implicit direction from \(x\) to \(y\):

\( f(x) = 3x^2 + 4 \)

A relational programmer sees the equation as a relation \(R\), specifying the relationship between possible values of \(x\) and \(y\):

\( R(x,y) \text{ iff } y = 3x^2 + 4 \text. \)

At the exact same time, a relational programmer will also view the relation as a set of tuples:

\( R = \{ (x,y) : y = 3x^2 + 4 \} \text. \)

[In fact, one of the major advantages of relational programming is that it unifies the predicate interpretation and collection-of-elements interpretation of a set into the same specification.

From the same specification of a relation, one can both enumerate members and test for membership.]

An example with lists

Every pure function can be encoded as a relation.

For instance, if we have an append function on lists, then we might ask the interpreter to evaluate:

(append '(1 2 3) '(4 5 6))

which would return '(1 2 3 4 5 6).

In relational programming, we would write a relation that defines the relationship between the “input” and the “output” of the function append, so that we could issue a constraint:

(relational-append '(1 2 3) '(4 5 6) output)

Then, instead of executing append, we would ask the relational interpreter to solve for output.

The relational interpreter would return '(1 2 3 4 5 6) as the sole satisfying value of output.

The key difference with relational programming is that relations don’t discriminate between “input” and “output.”

Any part of a relation can be fully constrained, partially constrained or totally unconstrained.

So, from a relational interpreter’s perspective, it makes just as much sense to write:

(relational-append '(1 2 3) y '(1 2 3 4 5 6))

and then to ask the relational interpreter to solve for y, which yields '(4 5 6).

In fact, we can even write:

(relational-append x y '(1 2 3 4 5 6))

and ask it to solve for both x and y, in which case it will return a collection of solutions:

x = '()                y = '(1 2 3 4 5 6)
x = '(1)               y = '(2 3 4 5 6)
x = '(1 2)             y = '(3 4 5 6)
x = '(1 2 3)           y = '(4 5 6)
x = '(1 2 3 4)         y = '(5 6)
x = '(1 2 3 4 5)       y = '(6)
x = '(1 2 3 4 5 6)     y = '()

Writing relational programs in miniKanren

Our ultimate goal is to write an interpreter for miniKanren.

This section is a crash course in the core constructs of miniKanren.

The core constructs are:

1. equality constraints;

2. disjunction of constraints;

3. fresh variable generation;

4. conjunction of constraints; and

5. recursion.

We’ll show how to translate a traditional functional program into a relational program.

The host language in this case will be Racket, but it could easily be another Lisp or Scheme.

Equality constraints

At a high level, relational programs are conjunctions and disjunctions of constraints.

And, the “big hammer” constraint in miniKanren is the equality constraint.

(Under the hood, equality constraints are solved with the very powerful method of unification.)

miniKanren uses == to say that two expressions must have the same value.

For instance:

(== x 42)

constrains x to have the same value as 42.

To invoke miniKanren on this constraint, we can use the solve form:

(solve for x in (== x 42))

in which case miniKanren dutifully evaluates this to 42.

[Experienced miniKanren programmers will recognize that in the interest of presenting this material to newcomers we have added a macro called solve which is a wrapper around the run form.]

We can also drop the x inside a data structure; for instance:

(solve for x in (== (cons 1 x) (list 1 2 3 4)))

evaluates to '(2 3 4).

For experienced miniKanren programmers, it’s customary to use the quasiquoting list syntax; they would write the above as:

(solve for x in (== `(1 . ,x) '(1 2 3 4)))

Disjunction of constraints

Sometimes, it is acceptable to have one of two constraints satisfied.

miniKanren has a conde form that combines constraints so that the resulting constraint holds if either or both hold.

[The name conde comes from the fact that in the process of translating a Scheme function into a miniKanren relation, cond in Scheme maps to conde in miniKanren.

In fact, or would have been a sensible name for conde if or were not already claimed by Scheme.]

For example:

(solve for x in (conde [(== x 13)]
                       [(== x 17)]))

will return 13.

Since there are two satisfying assignments to x, we can ask miniKanren for both of them:

(solve for 2 x in (conde [(== x 13)]
                         [(== x 17)]))

returns '(13 17).

Fresh variable generation

By default, miniKanren provides one “query” variable.

While writing a constraint, however, a relational programmer may need more than one unknown value.

For instance, if we have two unknown variables, head and tail, we can write an equation about a list:

(== (cons head tail) '(1 2 3 4))

We can ask miniKanren to solve this equation for head:

(solve for head in (== (cons head tail) '(1 2 3 4)))

but miniKanren crashes, saying that tail is an undefined variable.

We can use fresh to to bind tail to an unknown:

``` (solve for head in (fresh (tail) (== (cons head tail) ’(1 2 3 4)))) ````

returns 1.

Of course, we probably want to return both head and tail, and to do that we can use conjunction.

Conjunction of constraints

---