I keep bumping into logic programming, especially in the form of the *Kanren family. In keeping with tradition, this is my attempt to implement it in Rust, my current hobby language of choice.

After a few false starts, I got a not completely horrific proof of concept running. Then I rewrote it once or twice to improve usability, make it internally type safe and add a form of constraints. The sordid history is buried in git.

The end result? I'm pretty satisfied with the learning experience I got out of it, so any value in the actual artifact is just gravy.

## An Introduction

I'm still a novice, so take everything I say with a grain of salt.

Logic programming is weird. You write statements in (somewhat) arbitrary order and query the zero or more possible results if everything you said before holds true.

Things can be much fancier and terser in core.logic or Prolog, but this is what I've got so far.

``````use canrun::{Goal, both, unify, var, example::I32};

let x = var();
let y = var();
let goal: Goal<I32> = both(unify(x, y), unify(1, x));
let result: Vec<_> = goal.query(y).collect();
assert_eq!(result, vec!)
``````

Breaking it down...

### Imports

``````use canrun::{Goal, both, unify, var, example::I32};
``````

First are some imports, including an example domain that represents all of the types that will be valid in our little logic program. In this case, only `i32`.

### Logic Variables

``````let x = var();
let y = var();
``````

These are typed "logic variables" (specifically `LVar<i32>`), which can be unified with other values in our program.

### Goals

``````let goal: Goal<I32> = both(unify(x, y), unify(1, x));
``````

The `both` and `unify` functions are `Goal` constructors. A `Goal` represents one or more relations between logical values. In other words: A `Goal` is a set of predicates that we wish to prove. They can be evaluated to generate zero or more possible results. Note that it is constrained by the `I32` domain through its type parameter.

`unify(x, y)` essentially declares that `x` and `y` are equal to each other. Or, more precisely, that they must unify with each other. This distinction matters for more complicated values. We'll come back to that.

`both` combines the two `unify` goals into a goal that will only succeed if both sub goals succeed.

### Querying

``````let result: Vec<_> = goal.query(y).collect();
assert_eq!(result, vec!)
``````

To get results from a `Goal`, we can query it with one or more logic variables to get an iterator of possible results. We can take the first result with `.nth(0)`, `.collect()` them all, or use any of the other `Iterator` trait methods.

For example, querying the goal `either(unify(x, 1), unify(2, x))` for the value of `x` would return two possible results: `vec![1, 2]`.

Unification is quite a bit more interesting than simple equality when applied to structures.

The library provides a few "logically superpowered" structures such as `LVec` and `LMap`. Note that these are experimental even by Canrun standards.

``````use canrun::{Goal, val, var, all, unify};
use canrun_collections::{lvec, example::Collections};

let x = var();
let goal: Goal<Collections> = unify(
lvec![x, 2, 3],
lvec![1, 2, 3],
);
let results: Vec<_> = goal.query(x).collect();
assert_eq!(results, vec!);
``````

In this case, we actually plucked a value out of a structure by unifying a compatible structure containing our `LVar`.

Additional specialized collection types and goal constructors are available, with more coming as needs arise and ability allows.

### Member

``````let goal: Goal<Collections> = member(x, lvec![1, 2, 3]);
let results: Vec<_> = goal.query(x).collect();
assert_eq!(results, vec![1, 2, 3]);
``````

### Subset

``````let goal: Goal<Collections> = subset(
lvec![1, x],
lvec![1, 2, 3],
);
let results: Vec<_> = goal.query(x).collect();
assert_eq!(results, vec!);
``````

## What's Next?

Apart from random needs based additions...

### Ergonomics

The biggest obvious pain point I see at the moment is how annoying it is to implement many of traits such as `UnifyIn` and `ReifyIn`. I think 99% of the use cases can be handled with a derive macro.

### Even Fancier DSL

The function based API is not bad at all, but I still dream about doing some sort of fancy custom parser macro magic overkill to unlock something like:

``````let goal = logic! {
y = x
x = 1
}
goal.query(y)
``````

This is mostly so I can type `logic!`

### General Correctness

I've approached this as an engineering problem, with very little theoretical rigor or deep understanding of the prior art. This has been fun and enlightening, but I have no doubt that there are holes.

## Conclusion

Sometimes the types get a little scary, but overall I'm quite pleased with how fluent Rust is able to be with a little architectural care and feeding.

How much I'll actually work on this project is completely dependant on how applicable it actually ends up being to my other experiments. Or how much I keep nerd sniping myself.