Many thanks to William Byrd and Jason Hemann for reviewing this implementation and providing links to useful resources.
Thanks to E-liang and Mayank for providing valuable feedback and the presentation as well.
A minimal implementation of microKanren
-
To run tests:
make tests
-
To generate slides:
make slides
Inputs: Application of a goal to a state.
Output: Stream of states (zero or more, can be infinite).
A goal can either succeed or fail.
If the goal succeeds, it may result in a Stream of enlarged states.
-
===goalsconstructed from this succeed when its argumentsunify. It can then cause thestateto grow.This operator permits circular substitution, e.g.
x = x. -
fresh/callTakes in a unary function,
\x -> <body>.The binding variable,
xis a fresh logic variable (unbound to any values).The body is an expression over which the fresh variable's binding is scoped.
The function when applied, evaluates to a
goal. -
disj(disjunction / OR)Takes in 2 goals. If either of its arguments succeed,
disjsucceeds. Returns a non-empty stream if it succeeds. -
conj(conjunction / AND)Takes in 2 goals. Both have to succeed for
conjto succeed. Returns a non-empty stream if it succeeds.
A pair of a subtitution and a variable counter.
Represented as an association list.
E.g. [(x, 1), (y, 2), ...] where x is associated with 1, y associated with 2 and so on.
A non-negative integer. It initializes as 0.
TODO
TODO
TODO
nix microKanren?
microKanren on Haskell's typelevel
Use a Free DSL instead: e.g. Conj vs conj.
We can include side effects such as delay in our interpreter.