description | A Rust implementation of MicroKanren. |

last change | Mon, 17 Feb 2020 16:58:58 +0000 (17:58 +0100) |

URL | https://git.witchoflight.com/mukan |

readme

```
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.

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));
}
```

2020-02-17 |
Cassie Jones | Make the Bind iterator for AND goals fair develop | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Formatting fix | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Allow goals to yield to other goals while working | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Derive Eq for Term for performance | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Evaluate larger peano for performance evaluation | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Change Subst to store a single mapping for vars | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Move the terms out into a separate file | commit | commitdiff | tree | snapshot |

2020-02-17 |
Cassie Jones | Add a README | commit | commitdiff | tree | snapshot |

2020-02-16 |
Cassie Jones | What a horrible night to have an initial commit | commit | commitdiff | tree | snapshot |

3 years ago |
develop | shortlog | log | tree |