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:
One can write an evaluator for a traditional programming language in a purely relational style, and generate programs that evaluate to specific outputs.
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.
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:
relational interpreters do not need continuations; and
relational interpreters do not need backtracking.
Rather, for the implementation of a relational interpreter:
the big hammer is unification;
the structural timber is a monad;
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:
equality constraints;
disjunction of constraints;
fresh variable generation;
conjunction of constraints; and
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.