Bartosz Witkowski - Blog.

In the previous blog post, I introduced a logic programming system, inspired by Oleg Kiselyov’s toy kanren implementation. In this blog post I’d like to address its two major issues: lack of variable scoping and the lack of type safety.

# Variable scoping

The lack of variable scoping means we cannot safely reuse predicates that introduce new variables.

For example, if we would like to write an append predicate:

We cannot guarantee in any way that the id’s: h, t, l3p aren’t already bound in the current scope.

What we need is to be able to declare and use completely fresh variables.

Previously, we defined Predicate as:

For variable scoping to work we need to thread not only Knowledge between predicate but also the current state of the world:

Now, our new definition of Predicate becomes:

and the definition of VarId needs to become:

New VarIds need to come directly from the state, so we can write a “smart constructor”:

We also need a way to “run” a predicate and get out the variable values:

run and VarId.fresh methods of higher arity would be constructed in a similar manner.

Armed with the above we can now safely define an append predicate:

Tests:

# Reintroducing type safety

One shortcoming of a direct scheme port is that we lost type safety entirely.

In particular there is nothing in the above snipped disallowing us to call choice(UInt(1), UInt(2)) or choice(ulist(UInt(1)), ulist(UInt(1))) even though it could be inferred at compile time that these goals would fail.

For me, the essence of logic programming is the ability to interactively reason about unknowns. It would be a shame to let go of the ability to exclude some invalid forms at compile time.

In the rest of this blog post I’ll try to implement mechanisms improving type safety in our unityped logic programming system.

## Unification reconsidered

We implemented our unification algorithm using a typeclass Unifiable[T] where T is some universe of types for which we can perform unification (logical reasoning), and we implemented this typeclass for an Universe type.

If we take a look again at the Unifiable type class:

The topLevelEquivalent and varCheck methods are completely benign when it comes to type safety. It gets tricky when it comes to children and mapChildren as they smoosh possibly unrelated types together. What would a hypothetical typesafe unification method look like?

Unification would, unfortunately, demand passing around not only the types and their children, but also the children’s children (and their children… and so on). I tried sketching out an implementation but it quickly devolves into code that’s not my idea of fun.

Other alternative approaches that I have not tried:

I give up on trying to redefine unification as I had another approach in mind.

## Predicates reconsidered

What we would like to work is something like this:

Unfortunately, we only know how to unify terms belonging to some unifiable U type. Additionally, for a type to work in predicates it would need to:

1. Be able to hold values.
2. Be able to work as a variable.

So instead of working on raw values we will provide a wrapper type for logical values:

Similarly, we can provide a wrapper for a logical list (a recursive data type that’s either an empty list, a variable, or a value and the rest of the list):

Our choice predicate expressed with LogicalValue/LogicalList becomes:

But neither LogicalValue nor LogicalList is Unifiable. We could add it to the example Universe type but we can do even something better - and make the predicates that we write polymorphic. Consider the following two type classes:

We only need some tiny bit of additional machinery to make universe-polymorphic predicates work: a way to create variables when a Logical type class evidence is available, and the ability to run the predicates.

A little bit of syntax sugar will help us along the way:

Now we can correctly implement the both cons and append predicates:

To actually run and test it we need concrete evidence of Logical[LogicalValue[A], U] (and the same for LogicalList) for some unifiable type:

Testing it all:

# Why all the bother?

In this post we added two important features to the toy logic system described previously: variable scoping and an ability to write type-safe predicates.

Our strategy of writing type-safe wrappers for both values or logical lists introduces some ceremony but it facilities writing predicates that are polymorphic in the universe type.

In the previous blog post we defined an Unifiable type class that allows working with multiple concrete Unifiable instances. The reason for doing it is simple: for logical programming in Scala to be practical unification cannot be a closed class. New types can be unified as long as an user creates his own Unifiable type class.

As library writers we can provide both an default Unifiable type (like we did with the Universe type), type safe wrappers (like LogicalValue[T] and LogicalList[T]) and predicates that work on any Unifiable Universe type - and they work as long as an Embedding and Logical type classes for the Universe type are implemented.