Skip to content


Folders and files

Last commit message
Last commit date

Latest commit



14 Commits

Repository files navigation


Pony-Kanren is an implementation of microKanren for the Pony programming language.

The easiest way to use Pony-Kanren in your code is via Pony-Stable: run

stable add github kulibali/pony-kanren

to add Pony-Kanren as a dependency to your bundle.json, and then

use "kanren"

in your code to import the library.

You can find library documentation here.


To set up a logic expression and query its results:

  • Create an empty State value, with a functor that can unify the data type that your variables refer to.
  • Create a Goal that represents a logical expression.
    • Use the Goal.fresh() function to obtain a new state that knows about a variable. That variable will now be visible to subgoals. Note that if you use Goal.fresh() more than once, the variables will be disjoint. If their scopes intersect, you will get errors.
    • Use Goal.conj() for the logical AND operation. This will succeed only if both its subgoals succeed.
    • Goal.disj() is logical OR. This will succeed if either of its subgoals succeeds.
    • Goal.unify_vars() will unify two variables, if possible.
    • Goal.unify_vals() will attempt to structurally unify two values.
    • Goal.unify_val() will bind a variable to a value, if possible.
  • A goal is a function that returns a sequence of states. Each state may contain variable bindings that represent a solution to the logical expression.
    • If there is no solution for the expression, the sequence will be empty.
    • If an error occurrs when solving, the sequence will contain a solution with unbound variables and some error messages obtainable via its get_errors() method.
  • You can query the value of any variable in a particular state using the state's apply() method.


The following Pony code initializes and solves the expression A = B && (B = 123 || B = 456). Running the goal will result in a sequence of two states, one where A and B are bound to 123, and one where A and B are bound to 456:

use "kanren"

let a = Var("A")
let b = Var("B")
let g =
        Goals.unify_vars[USize](b, a),
          Goals.unify_val[USize](b, 123),
          Goals.unify_val[USize](b, 456)

let results = g(State[USize](UnifyEq[USize]))
let s1 =
s1(a) == 123 // true
s1(b) == 123 // true
let s2 =
s2(a) == 456 // true
s2(b) == 456 // true