miniKanren implementation taken from William E. Byrd and Daniel P. Friedman, "From Variadic Functions to Variadic Relations: A miniKanren Perspective", Proceedings of the 2006 Scheme and Functional Programming Workshop, University of Chicago Technical Report TR-2006-06, 2006, pp. 105-117

miniKanren.scm

; miniKanren evolved from Kanren [1]; its implementation comprises three kinds
; of operators: functions such as unify and reify, which take substitutions
; explicitly; goal constructors ==, conde, and fresh, which take substitutions
; implicitly; and the interface operator run. We represent substitutions as
; association lists associating variables with values.

; unify is based on the triangular model of substitutions (See Baader and
; Snyder [2], for example). Vectors should not occur in arguments passed to
; unify, since we represent variables as vectors.

(define (unify u v s)
  (let ((u (walk u s))
        (v (walk v s)))
    (cond
      ((eq? u v) s)
      ((var? u)
       (cond
         ((var? v) (ext-s u v s))
         (else (ext-s^ u v s))))
      ((var? v) (ext-s^ v u s))
      ((and (pair? u) (pair? v))
       (let ((s (uify (car u) (var v) s)))
         (and s (unify (cdr u) (cdr v) s))))
      ((equal? u v) s)
      (else #f))))

(define (walk v s)
  (cond
    ((var? v)
     (let ((a (assq v s)))
       (cond
         (a (walk (cdr a) s))
         (else v))))
    (else v)))

(define (ext-s^ x v s)
  (cond
    ((occurs^ x v s) #f)
    (else (ext-s x v s))))

(define (occurs^ x v s)
  (let ((v (walk v s)))
    (cond((var? v) (eq? v x))
      ((pair? v)
       (or (occurs^ x (car v) s) (occurs^ x (cdr v) s)))
      (else #f))))

(define (ext-s x v s)
  (cons `(,x . ,v) s))

(define empty-s '())

(define var vector)

(define var? vector?)

; reify takes a substitution and an arbitrary value, perhaps containing
; variables. reify first uses walk* to apply the substitution to a value and
; then methodically replaces any variables with reified names.

(define reify
  (letrec
    ((reify-s
      (lambda (v s)
        (let ((v (walk v s)))
          (cond
            ((var? v) (ext-s v (reify-name (length s)) s))
            ((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
            (else s))))))
    (lambda (v s)
      (let ((v (walk* v s)))
        (walk* v (reify-s v empty-s))))))

(define (walk* w s)
  (let ((v (walk w s)))
    (cond
      ((var? v) v)
      ((pair? v) (cons (walk* (car v) s) (walk* (cdr v) s)))
      (else v))))

(define (reify-name n)
  (string->symbol
    (string-append "_" "." (number->string n))))

; A goal g is a function that maps a substitution s to an ordered sequence of
; zero or more values--these values are almost always substitutions. Because
; the sequence of values may be infinite, we represent it not as a list but as
; a special kind of stream, a~.

; Such streams contain either zero, one, or more values [10, 16]. We use
; (mzero) to represent the empty stream of values. If a is a value, then (unit
; a) represents the stream containing just a. To represent a non-empty stream
; we use (choice a f), where a is the first value in the stream, and where f is
; a function of zero arguments. Invoking the function f produces the remainder
; of the stream. (unit a) can be represented as (choice a (lambda () (mzero))),
; but the unit constructor avoids the cost of building and taking apart pairs
; and invoking functions, since many goals return only singleton streams. To
; represent an incomplete stream, we create an f using (inc e), where e is an
; expression that evaluates to an a~.

(define-syntax mzero
  (syntax-rules ()
   ((_) #f)))

(define-syntax unit
  (syntax-rules ()
   ((_ a) a)))

(define-syntax choice
  (syntax-rules ()
   ((_ a f) (cons a f))))

(define-syntax inc
  (syntax-rules ()
   ((_ e) (lambda () e))))

; To ensure that streams produced by these four a~ constructors can be
; distinguished, we assume that a singleton a~ is never #f, a function, or a
; pair whose cdr is a function. To discriminate among these four cases, we
; define case~.

(define-syntax case~
  (syntax-rules ()
    ((_ e on-zero ((a^) on-one) ((a f) on-choice) ((f^) on-inc))
     (let ((a~ e))
       (cond
         ((not a~) on-zero)
         ((procedure? a~) (let ((f^ a~)) on-inc))
         ((and (pair? a~) (procedure? (cdr a~)))
          (let ((a (car a~)) (f (cdr a~))) on-choice))
         (else (let ((a^ a~)) on-one)))))))

; The simplest goal constructor is ==, which returns either a singleton stream
; or an empty stream, depending on whether the arguments unify with the
; implicit substitution. As with the other goal constructors, == always expands
; to a goal, even if an argument diverges. We avoid the use of unit and mzero
; in the definition of ==, since unify returns either a substitution (a
; singleton stream) or #f (our representation of the empty stream).

(define-syntax ==
  (syntax-rules ()
    ((_ u v)
     (lambda (s) (unify u v s)))))

; conde is a goal constructor that combines successive conde-clauses using
; mplus*. To avoid unwanted divergence, we treat the conde-clauses as a single
; inc stream. Also, we use the same implicit substitution for each
; conde-clause. mplus* relies on mplus, which takes an a~ and an f and combines
; them (a kind of append). Using inc, however, allows an argument to become a
; stream, thus leading to a relative fairness because all of the stream values
; will be interleaved.

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambda (s)
       (inc
         (mplus*
           (bind* (g0 s) g ...)
           (bind* (g1 s) g^ ...) ...))))))

(define-syntax mplus*
  (syntax-rules ()
    ((_ e) e)
    ((_ e0 e ...) (mplus e0 (lambda () (mplus* e ...))))))

(define (mplus a~ f)
  (case~ a~
    (f)
    ((a) (choice a f))
    ((a f^) (choice a (lambda () (mplus (f^) f))))
    ((f) (inc (mplus (f) f^)))))

; If the body of condewere just the mplus* expression, then the inc clauses of
; mplus, bind, and take would never be reached, and there would be no
; interleaving of values.

; fresh is a goal constructor that first lexically binds its variables (created
; by var) and then, using bind*, combines successive goals. bind* is
; short-circuiting: since the empty stream (mzero) is represented by #f, any
; failed goal causes bind* to immediately return #f. bind* relies on bind [11,
; 17], which applies the goal g to each element in a~. These a~’ are then
; merged together with mplus yielding an a~. (bind is similar to Lisp’s mapcan,
; with the arguments reversed.)

(define-syntax fresh
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (lambda (s)
       (let ((x (var 'x)) ...)
         (bind* (g0 s) g ...))))))

(define-syntax bind*
  (syntax-rules ()
    ((_ e) e)
    ((_ e g0 g ...)
     (let ((a~ e))
       (and a~ (bind* (bind a~ g0) g ...))))))

(define (bind a~ g)
  (case~ a~
    (mzero)
    ((a) (g a))
    ((a f) (mplus (g a) (lambda () (bind (f) g))))
    ((f) (inc (bind (f) g)))))

; To minimize heap allocation we create a single lambda closure for each goal
; constructor, and we define bind* and mplus* to manage sequences, not lists,
; of goal-like expressions.

; run, and therefore take, converts an f to a list.
; We wrap the result of (reify x s) in a list so that the case~ in take can
; distinguish a singleton a~ from the other three a~ types. We could simplify
; run by using var to create the fresh variable x, but we prefer that fresh be
; the only operator that calls var.

(define-syntax run
  (syntax-rules ()
    ((_ n (x) g0 g ...)
     (take n
        (lambda ()
          (let ((g^ (fresh (x)
                      (lambda (s)
                        (bind* (g0 s) g ...
                          (lambda (s)
                            (list (reify x s))))))))
            (g^ empty-s)))))))

(define (take n f)
  (if (and n (zero? n))
    '()
    (case~ (f)
      '()
      ((a) a)
      ((a f) (cons (car a) (take (and n (- n 1)) f)))
      ((f) (take n f)))))

; If the first argument to take is #f, we get the behavior of run*. It is
; trivial to write a read-eval-print loop that uses the run* interface by
; redefining take.

; [1] A declarative applicative logic programming system.
; http://kanren.sourceforge.net/.
 
; [2] Baader, F., and Snyder, W.Unification theory.In Handbook of Automated
; Reasoning, A. Robinson and A. Voronkov, Eds., vol. I. Elsevier Science, 2001,
; ch. 8, pp. 445–532.

; [10] Kiselyov, O., Shan, C., Friedman, D. P., and Sabry, A.Backtracking,
; interleaving, and terminating monad transformers: (functional pearl). In
; Proceedings of the 10th ACM SIGPLAN International Conference on Functional
; Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005 (2005), O.
; Danvy and B. C. Pierce, Eds., ACM, pp. 192–203.