Case Study: µKanren

µKanren (Hemann & Friedman, 2013; the bibliography has the citation) is a relational programming language whose complete kernel fits in under forty lines of Scheme. lib/mk.naj is the port of namin/pink’s mk.scm, and it stresses a different part of Pink than the matcher did: higher-order goals, streams represented partly as closures, and a program built by wrapping.

The kernel

The concepts, compressed: a logic variable is a tagged pair (var . n); a substitution is an association list from variables to terms; a state is a substitution paired with a fresh-variable counter; a goal is a function from a state to a stream of states — each state in the stream a distinct way the goal can succeed. Four combinators build every goal: == (unify two terms), call/fresh (introduce a variable), disj (either goal), conj (both goals).

mk is a program→program wrapper in the same style as matcher: it splices an object program into a let-chain that binds the kernel around it —

(define mk (lambda _ program
  `(let = (lambda _ a (lambda _ b (if (- a b) 0 1)))
   (let assp ...
   ...
   (let empty-state (cons 'nil 0)
   ,program
   )))...))

so (mk prog) is closed Pink source in which prog sees ==, call/fresh, disj, conj, and empty-state. (Two renamings from the reference: $-prefixed stream names became st names, since $ is not a symbol character here, and '() is written 'nil.)

Running goals

A goal runs by applying it to empty-state. The simplest one binds a fresh variable to 5:

(load lib/mk.naj)
((interpret (mk '(let p ((call/fresh (lambda _ q ((== q) 5))) empty-state) (car p)))) nil-env)
;=> (((('var . 0) . 5)) . 1)

The first state in the stream: the substitution binds variable 0 to 5, and the counter says one variable exists. The rest of the stream is empty — unification succeeds exactly one way:

((interpret (mk '(let p ((call/fresh (lambda _ q ((== q) 5))) empty-state) (cdr p)))) nil-env)
;=> nil

Disjunction is where streams earn their keep. The reference test suite’s a-and-b goal constrains a to 7 and b to 5 or 6; the stream has one state per way to satisfy it:

((interpret (mk '(let p (((conj (call/fresh (lambda _ a ((== a) 7)))) (call/fresh (lambda _ b ((disj ((== b) 5)) ((== b) 6))))) empty-state) (car p)))) nil-env)
;=> (((('var . 1) . 5) (('var . 0) . 7)) . 2)
((interpret (mk '(let p (((conj (call/fresh (lambda _ a ((== a) 7)))) (call/fresh (lambda _ b ((disj ((== b) 5)) ((== b) 6))))) empty-state) (car (cdr p))))) nil-env)
;=> (((('var . 1) . 6) (('var . 0) . 7)) . 2)

First state: b is 5. Second: b is 6. Both carry the a-to-7 binding and a counter of two. Streams are not always fully-built lists — mplus and bind suspend work behind zero-argument closures when a stream’s tail is not yet demanded, which is what lets µKanren enumerate answers from infinite relations.

Through the compiler

(mk prog) is a program like any other, so the whole Futamura pipeline of this part applies to it unchanged. Compiling the wrapped goal — kernel and all — produces the same first state as interpreting it:

(compile (mk '(let p ((call/fresh (lambda _ q ((== q) 5))) empty-state) (car p))))
;=> (((('var . 0) . 5)) . 1)

The residual is the program itself in ANF — the collapse property again — and compile’s run 0 executes it, so the printed value is the finished state rather than a function. Compiling a goal into a reusable compiled artifact needs the goal kept behind a function boundary, and choosing where that boundary sits under staging is exactly what clambda is for, in Part IV.