Use unification-sop if you want a mechanism to generically derive prolog-style unification for your datatypes, with minimal boilerplate.

When talking of unification, the usual implementation is the unification-fd package. However that package has two major shortcomings in my opinion:

• Your datatype has to be in the form of the fixpoint of a functor.
• It's not immediately clear how to use it, the typeclasses and the types involved, and the lack of documentation can be daunting.

In this package we construct a different mechanism for unification which is strictly more expressive, letting us work with datatypes that are not in the fixpoint form, and simpler, requiring only an additional datatype, and that does not perform abysmally worse (since the core algorithm is the same). That said, try to use `unification-fd` if you want unification for typechecking (which is the main use-case of that package) because it is surely more stable and it still has more optimization than this one (like, path-compression).

Let's consider a datatype we will use as an example through this tutorial:

To use this library you need to deriving the generic instances. You can do that via:

deriving (GHC.Generic, Generic, HasDatatypeInfo)

provided you have the DeriveGeneric and DeriveAnyClass extensions enabled (Generic and HasDatatypeInfo come from generic-sop). That's all the boilerplate you need!

Taking inspiration from prolog, we would like to express terms that are of type Foo, but can have (typed) logical variables as subterms. In this library, that's the role of the Term datatype. In this case a Term Foo is a Foo that can have logical variables as subterms.

Let's see some examples, where I also give a prolog translation (haskell constructors are seen as prolog clean representations). Keep in mind that the show instances that display these result are automatically generated to be consistent with the smart constructors I'll talk about later.

To make easier working with terms, I propose the usage of smart constructors. For example, for our Foo datatype, we could define:

fooS :: Term String -> Term Foo -> Term Foo
fooS ts tf = Rec . SOP . S . Z $ ts :* tf :* Nil

fooI :: Term Int -> Term Foo
fooI ti = Rec . SOP . Z $ ti :* Nil

This constructs could be completely generated by the library (via generics or TH), but in this iteration of the library they have to be generated by the user. It is worth noting that the show instances I generated are geared towards this use-case, and that is automatic. With there smart constructors defined, we can actually write previous examples exactly the way they are shown by our show instance.

Depending on your needs, you could also define these as bidirectional patterns instead, enabling PatternSynonyms and writing:

pattern TFooI :: Term Int -> Term Foo
pattern TFooI t = Rec (SOP (Z (t :* Nil)))

pattern TFooR :: Term String -> Term Foo -> Term Foo
pattern TFooR ti tf = Rec (SOP (S (Z (ti :* tf :* Nil))))

Now let's have an example of a unification between two terms:

The result of unification can be Right and the substituted term, or Left and an explanation of the error.

>>> :t unify exU1 exU2
unify exU1 exU2 :: Monad m => UnificationT m (Term Foo)

>>> runIdentity . evalUnificationT $ unify exU1 exU2
Right (fooS (Con "Hello") (fooS (Con "World") (fooI (Var 1))))

In this case we can see that the unification succeeded, leaving the Int-typed variable alone.

>>> runIdentity . evalUnificationT $ unify exU2 exU3
Left IncompatibleUnification

In this case we can see that the two terms can't be unified.

If you want further inspiration, in the Hinze module I implemented a full typed prolog complete with the Cut construct, following Hinze's paper on denotational semantic of a prolog interpreter. If you have question don't hesitate to write them in the github issue tracker.