The first time I was introduced to miniKanren I observed a few it’s quirks which are not fixed yet. In this post I want to describe them down for future generations. Also, in the end, I will give you my thoughts about declarativeness of relational programming.

We are going to use our dialect of miniKanren called ‘OCanren’ – a typed embedding of relational language to OCaml. We have a few syntax extensions to write and run relational programs. I’m going to present OCanren taking two simple relations ‘appendo’ and ‘reverso’ as examples.

let rec appendo xs ys xys =
  fresh (h tl xytl)
    (conde
      [ xs === Std.nil () &&& (ys === xys)
      ; (xs === List.cons h tl) &&&
        (xys === List.cons h xytl) &&&
        (appendo tl ys xytl)
      ])

Relations in OCanren are mapped to plain OCaml functions of a specific type (it’s not important for now which exactly). Therefore recursive relations are defined as recursive OCaml functions. In a body of a relation we could meet a disjunction of multiple arity (called conde); conjunction compinator called &&& (which is in a theory “fair”), unification and creation of fresh logic variables with a macro ‘fresh’. In the example above the macro fresh (h tl xytl) creates three logic variables (h, tl and xytl). Also it inserts a lazy delay, which is required because all the combinators and all the functions are evaluated with call-by-value strategy.

The relation appendo takes two logical lists and associates them (or simply ‘returns’) a list which is concatenation of two. The implementation above is canonical, it doesn’t have much space to vary. The implementation of ‘reverso’ relation, which reverses order of elements in the input list, is more complicated.

let rec reverso xs ys =
 fresh (h tl)
   (conde
      [ xs === Std.nil () &&& (xs === ys)
      ; (xs === List.cons h tl) &&&
        (reverso tl temp) &&&
        (appendo temp (List.singleton h) ys)
      ])

When ‘reverso’ takes a non-empty list, it splits it to head and tail, reverses tail and concatenates reversed tail and a head. In this code the implementer has an ambiguity which call of relation to put first: of reverso or of appendo. In theory left and right conjuncts should be interchangeable. But in practice not always (these ones aren’t), which will be discussed below. In theory the call of unification is always better to put before recursive calls of other relations, because in finite time we will get more information about and it can’t hurt termination. But in practice, it’s not that simple either.

Let’s try to run relations defined above. The appendo relation we can easily turn to inverse algorithms, and, for example, generate all pairs of lists, which concatenation is [1;2;3]

fun q r -> appendo xs ys (Std.list (!!) [1; 2; 3]), all answers {
q=[]; r=[1; 2; 3];
q=[1]; r=[2; 3];
q=[1; 2]; r=[3];
q=[1; 2; 3]; r=[];
}

We can easily call reverso relation in forward direction trying to get first and all answers:

fun xs -> reverso (Std.list (!!) [1; 2; 3]) xs, 1 answer {
q=[3; 2; 1];
}
fun xs -> reverso (Std.list (!!) [1; 2; 3]) xs, all answers {
q=[3; 2; 1];
}

And we could try to call reverso relation in the inverse direction, trying to get first and all answer:

fun xs -> reverso xs (Std.list (!!) [1; 2; 3]), 1 answer {
q=[3; 2; 1];
}
fun xs -> reverso xs (Std.list (!!) [1; 2; 3]), all answers {
q=[3; 2; 1];
<HANGS>

Yikes. Getting the first answer works as expected, but getting all answers diverges after getting the first answer. miniKanren can’t understand that no more answer could be generated when the first argument of relation is a free variable, and the second argument is a ground logic list representing [1;2;3]. It happens because in the implementation of ‘reverso’ we are calling reverso before the appendo. For our input, it splits a free variable (the first argument) into head and tail and tries to get all possible ways to reverse a free variable before calling ‘appendo’.

The educated guess says that if the call of appendo goes before the call of reverso it will help our situation. Let’s try another implementation of ‘reverso’.

let rec reverso xs ys =
  fresh (h tl)
    (conde
      [ xs === Std.nil () &&& (xs === ys)
      ; (xs === List.cons h tl) &&&
        (appendo temp (List.singleton h) ys) &&&
        (reverso tl temp)
      ])

Now execution in the inverse direction is fine:

fun xs -> reverso xs (Std.list (!!) [1; 2; 3]), 1 answer {
q=[3; 2; 1];
}
fun xs -> reverso xs (Std.list (!!) [1; 2; 3]), all answers {
q=[3; 2; 1];
}

But execution in normal direction is broken now:

fun xs -> reverso (Std.list (!!) [1; 2; 3]) xs, 1 answer {
q=[3; 2; 1];
}
fun xs -> reverso (Std.list (!!) [1; 2; 3]) xs, all answers {
q=[3; 2; 1];
<HANGS>

In this case we are passing a free variable as the first argument of ‘appendo’ relation. It tries to find all possible solutions and never understands that no more answers could be generated.

There are a few approaches to workaround this concrete case of divergence. We could try to extend miniKanren with a special branch construction which will reorder branches when one of the relation’s arguments is a ground variable. This will help in that concrete case, but, first, it is not obvious how scalable it is for other cases of a divergence. The second issue is that this insight from a developer makes relational programming less declarative as it plans to be.

The second idea is to detect cases of divergence and cut search space where we are 100% sure that no useful answer will be found. This approach was taken in a paper “Improving Refutational Completeness of Relational Search via Divergence Test” (2018). This idea is not implemented in OCanren, as far as I understand, because it doesn’t help in too many cases.

The third idea (from the paper “On Fair Relational Conjunction” (2020)) tries to unroll relation definition when a relation is structurally recursive by one of it’s arguments. It is a serious change of implementation and in some cases it improves performance, but sometimes degrades. All these ideas are not available in the main repository of OCanren.

As far as I understand, the Prolog language suffers the same illness about unfairness of conjunction. For some extent, Prolog with depth-first search strategy is less declarative than miniKanren, because of the incompleteness of the strategy. miniKanren uses interleaving search which is in between depth-first and breadth-first searches. It is complete as breadth-first but is less efficient when you know exactly in which branch we can find the right answer. So, it looks like miniKanren is more declarative than Prolog, but is not entirely declarative. By the way, in this note I understand the term ‘declarative’ as ‘we don’t need to think about how our program is going to be executed’.