MiniKanren core unify

(define unify
  (lambda (v w s)
    (let ((v (walk v s))
          (w (walk w s))
      (cond
        ;; Check for variable equality -> are they the same fresh variable?
        ;; Do not introduce (v . w) or (w . v) to s.
        ;; Why? v and w are the same, it will be a cyclic association (self . self)
        ((eq? v w) s)

        ;; Is v a fresh variable? If so, bind to w
        ((var? v) (ext-s v w s))

        ;; Is w a fresh variable? If so, bind to v
        ((var? w) (ext-s w v s))

        ;; Otherwise if they are pairs of variables
        ((and (pair? v) (pair? w))
         (cond
           ;; If we can unify these to get a new substitution, s'
           ((unify (car v) (car w) s) =>
             ;; Try to unify the rest as well
             (lambda (s)
               (unify (cdr v) (cdr w) s)))
             ;; If we can't, unify fails
             (else #f)))

        ;; If either v or w is a pair, and the other is not,
        ;; there's no substitution which can make them equal
        ;; We can generalize this to other shapes - vectors, lists etc...
        ((equal? v w) s)

        (else #f))))))

Improvements

  1. Determine if v is same as w before performing let-bind for v and w.

  2. Generalizing 1., Walk one of them, see if we meet the other while walking -> we know that 2 variables unify