MuKan

mukan = { git = "https://git.witchoflight.com/mukan" }

(Micro Kanaya :3)

This is a Rust implementation of MicroKanren, based on the very readable original paper at: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf.

There's a nice Clojure implementation that I also found very informative, for getting another perspective on the unification and an idea of where the natural extension points are: https://mullr.github.io/micrologic/literate.html.

Usage:

You build up goals with goal constructors, and then execute them with the solve method of Goal, running that on an initial state. One of the simplest possible programs you could write is:

use mukan::{Goal, call_fresh, State, eq};

fn main() {
    let goal = call_fresh(|x| eq(413, x));
    for soln in goal.solve(State::new()) {
        println!("{}", soln);
    }
}

This will create a goal that wants to solve 413 = X, and then show you all of the solutions starting with an empty state. You can get slightly fancier, with problems that have multiple solutions:

let goal = call_fresh(|x| or(eq(612, x), eq(1025, x)));

This will produce two solutions, assigning x to 612 and 1025 in them, respectively. There are macros that make several of the features easier to use. Here, we can use fresh! to create multiple variables, and all! to and together an arbitrary number of goals. You can also work with pairs of variables, letting you produce some more interesting cases.

let goal = fresh!((a, b, c) => all! {
    eq((a, b), c),
    eq((b, 8), c),
});

Here this should solve to a = 8, b = 8, and c = (8, 8). Of course, the solution that gets printed is messier, so you might want to ask for a solution in terms of the raw values. You can get the entire state evaluated like this with the reify function, but if you just want to get a few particular variables, then you can use reify_vars with variables that you own.

One way to get those variables, is make your variables in a particular state:

let (vars, state) = State::with_vars(2);
let (a, b) = (vars[0], vars[1]);
let goal = fresh!((c) => all! {
    eq((a, b), c),
    eq((b, 8), c),
});
for soln in goal.solve(state) {
    println!("{:?}", reify_vars(&vars, soln));
}

You can write recursive goals as rust functions, as well!

fn peano(n: impl Into<Term>) -> impl Goal {
    let n = n.into();
    or(
        eq(n.clone(), 0),
        fresh!((x) => and(
            eq(n.clone(), (1, x)),
            delay(move || peano(x)),
        )),
    )
}

We need the delay() in order to prevent the goal from being constructed forever without being searched at all. If you try to solve peano with a variable, then you'd get an infinite stream of assignments that satisfy it. Here we just take the first 10:

let (vars, state) = State::with_vars(1);
let goal = peano(vars[0]);
for soln in goal.solve(state).take(10) {
    println!("{:?}", reify_vars(&vars, soln));
}