Cassie Jones [Sun, 16 Feb 2020 23:06:21 +0000 (00:06 +0100)]
What a horrible night to have an initial commit
This implements MicroKanren in Rust, based on the original paper:
http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
It's also informative to look at the "microLogic" implementation in
Clojure, which inspired the slightly cleaner unification style and
provides some ideas for what the extension points might need to be in
the future: https://mullr.github.io/micrologic/literate.html
This implementation is based around a "goal" trait, which can be asked
to search for solutions in a given state, producing a stream of new
states. Unlike the implementations above, we use Rust's Iterator trait
to implement the state streams. This might need to change in order to
enable "unproductive" steps in searching to be interleaved with other
searches. Potentially we should just change the iterator to use
Iterator<Item = Step> where Step values are Pending or Sat(State).
Goal is implemented for F: Fn(State) -> impl Iterator<Item = State>,
which means that you can write searches with functions. A goal that
wants to prove "true" would look like:
|state: State| std::iter::once(state)
and a goal to prove "false" would look like:
|state: State| std::iter::empty()
The functions and() and or() construct larger goals out of their
sub-goals, although they have more complicated implementations in order
to provide somewhat fair search. The and() goal constructor currently
doesn't produce a fair search, because if the second goal ever produces
infinite streams, then the first goal won't get a chance to advance.
This can be fixed, although it will involve allocation.
The delay() constructor is needed in order to produce recursive
procedures. It takes a thunk that produces a goal, and invokes it only
when it's first searched. Without this, recursive goals would
continually construct larger and larger goals forever. The Rust
implementation needs an additional consideration here: we have to box
the output Goal type. Most of the goal constructors return `impl Goal`
which gives an opaque type that incorporates its contents, including its
code. If you wrote a recursive procedure which directly incorporated
itself without a box in-between, it would have to have a type which
contained its own type, which means an infinite type.
This boxing issue is also what ended up complicating the Clone code.
Goals often need to be cloned, because they need to be able to be used
again and again during search, repeatedly constructing the derived
goals, but if we want a boxed goal that obscures the specific type, then
we needed to use `Box<dyn Goal>`, and so since Clone trait isn't
object-safe, it can't be used as a bound on Goal, and thus we need
`Goal: DynClone` so that the `Box<dyn Goal>` can implement Clone, and
also we need a to write Goal + Clone in lots of places because we need
both bounds.
Some of the constructors use Into<Term> in order to make writing
programs with the terms more convenient. Tuples become pair terms,
integers become literal terms, and variables are wrapped.