# 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