An implementation of μKanren in Swift (http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf)

Kanren.swift

//: Playground - noun: a place where people can play
//: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

typealias Var = Int
typealias Subst = [(Var, Term)]
typealias State = (Subst, Int)
typealias Goal = State -> Stream

indirect enum Stream {
	case Nil, Cons(State, Stream), Lazy(() -> Stream)
	
	func mplus(s2 : Stream) -> Stream {
		switch (self, s2) {
		case (.Nil, _):
			return s2
		case let (.Cons(v1, a1), a2):
			return .Cons(v1, a1.mplus(a2))
		case let (.Lazy(a1), a2):
			return .Lazy({ a2.mplus(a1()) })
		}
	}
	
	func flatMap(goal : Goal) -> Stream {
		switch self {
		case .Nil:
			return .Nil
		case let .Cons(st, rest):
			return goal(st).mplus(rest.flatMap(goal))
		case let .Lazy(f):
			return .Lazy({ f().flatMap(goal) })
		}
	}
}

indirect enum Term {
	case Variable(Var), Pair(Term, Term), Integer(Int)
	
	/// Apply a substitution to a term.
	func walk(s : Subst) -> Term {
		switch self {
		case .Variable(let u):
			if let (_, t) = s.filter({ $0.0 == u }).first { return t.walk(s) }
			return .Variable(u)
		default:
			return self
		}
	}
}

/// Attempt to unify two terms under a substitution, returning an extended substitution on success.
func unify(u : Term, _ v : Term, _ s : Subst) -> Subst? {
	func extend(s : Subst, _ v : (Var, Term)) -> Subst { return [v] + s }
	
	// Walk the substitution down both terms before unifying.
	switch (u.walk(s), v.walk(s)) {
	case let (.Variable(u), .Variable(v)):
		if u == v {
			// Trivial
			return .Some(s)
		}
		// Otherwise we need to sub in the fresh variable.
		return .Some(extend(s, (u, .Variable(v))))
	case let (.Variable(u), v):
		// Unifying a variable with a thing that doesn't look like a variable means we have to sub
		// in the new thing for the old.
		return .Some(extend(s, (u, v)))
	case let (_, .Variable(v)):
		// and vice-versa.
		return .Some(extend(s, (v, u)))
	case let (.Pair(u1, u2), .Pair(v1, v2)):
		// To unify pairs, it suffices to unify the elements.
		return unify(u1, v1, s).flatMap { unify(u2, v2, $0) }
	case let (.Integer(i1), .Integer(i2)):
		// Unification succeeds under ==.
		return (i1 == i2) ? .Some(s) : .None
	default:
		// wat?
		return .None
	}
}

/// MARK: Goal Constructors

/// Equiv succeeds when both arguments unify.
func equiv(u : Term, _ v : Term) -> Goal {
	return { (subst, counter) in
		switch unify(u, v, subst) {
		case .None:
			return .Nil
		case let .Some(subst):
			return .Cons(((subst, counter)), .Nil)
		}
	}
}

/// Returns a goal that binds a fresh logic variable before passing state.
func callFresh(f : Term -> Goal) -> Goal { 
	return { (subst, counter) in 
		return f(.Variable(counter))((subst, counter + 1)) 
	} 
}

/// Returns a non-empty stream if either argument is successful.
func disj(g1 : Goal, _ g2 : Goal) -> Goal { 
	return { (state, counter) 
		in return g1((state, counter)).mplus(g2((state, counter))) 
	}
}
/// Returns a non-empty stream if both arguments are successful.
func conj(g1 : Goal, _ g2 : Goal) -> Goal { 
	return { (state, counter) in 
		return g1((state, counter)).flatMap(g2) 
	}
}

let emptyState : State = ([], 0)

func five(x : Term) -> Goal {
	return equiv(x, .Integer(5))
}

func fives(x : Term) -> Goal {
	return disj(equiv(x, .Integer(5)), { sc in .Lazy({ fives(x)(sc) }) })
}

print(callFresh(fives)(emptyState))