-- unification-fd 0.6.0
The unification-fd package offers generic functions for single-sorted
first-order structural unification (think Prolog programming or
Hindley--Milner type inference)[1][2]. I've had this laying around for a
few years, so I figured I might as well publish it.
An effort has been made to try to make this package as portable as
possible. However, because it uses the ST monad and the mtl-2 package it
can't be H98 nor H2010. However, it only uses the following common
extensions which should be well supported[3]:
Rank2Types
MultiParamTypeClasses
FunctionalDependencies -- Alas, necessary for type inference
FlexibleContexts -- Necessary for practical use of MPTCs
FlexibleInstances -- Necessary for practical use of MPTCs
UndecidableInstances -- For Show instances due to two-level types
-- Changes (since 0.5.0)
* The kind of variables has been changed from *-* to *. Thus, the
definition of MutVar is now exactly the free monad generated by t on v:
data MutTerm v t
= MutVar !v
| MutTerm !(t (MutTerm v t))
This is a major API-breaking change, however it only affects the type
level, and should only affect you if you're using the functions
class-polymorphically or if you've defined your own variable types.
-- Description
The unification API is generic in the type of the structures being
unified and in the implementation of unification variables, following
the two-level types pearl of Sheard (2001). This style mixes well with
Swierstra (2008), though an implementation of the latter is not included
in this package.
That is, all you have to do is define the functor whose fixed-point is
the recursive type you're interested in:
-- The non-recursive structure of terms
data S a = ...
-- The recursive term type
type PureTerm = Fix S
And then provide an instance for Unifiable, where zipMatch performs one
level of equality testing for terms and returns the one-level spine
filled with pairs of subterms to be recursively checked (or Nothing if
this level doesn't match).
class (Traversable t) = Unifiable t where
zipMatch :: t a - t b - Maybe (t (a,b))
The choice of which variable implementation to use is defined by
similarly simple classes Variable and BindingMonad. We store the
variable bindings in a monad, for obvious reasons. In case it's not
obvious, see Dijkstra et al. (2008) for benchmarks demonstrating the
cost of naively applying bindings eagerly.
There are currently two implementations of variables provided: one based
on STRefs, and another based on a state monad carrying an IntMap. The
former has the benefit of O(1) access time, but the latter is plenty
fast and has the benefit of supporting backtracking. Backtracking itself
is provided by the logict package and is described in Kiselyov et al.
(2005).
In addition to this modularity, unification-fd implements a number of
optimizations over the algorithm presented in Sheard (2001)--- which is
also the algorithm presented in Cardelli (1987).
* Their implementation uses path compression, which we retain. Though we
modify the compression algorithm in order to make sharing observable.
* In addition, we perform aggressive opportunistic observable sharing, a
potentially novel method of introducing even more sharing than is
provided by the monadic bindings. Basically, we make it so that we can
use the observable sharing provided by the previous optimization as much
as possible (without introducing any new variables).
* And we remove the notoriously expensive occurs-check, replacing it
with visited-sets (which detect cyclic terms more lazily and without the
asymptotic overhead of the occurs-check). A variant of unification which
retains the occurs-check is also provided, in case you really need to
fail fast for some reason.
* Finally, a highly experimental branch of the API performs *weighted*
path compression, which is asymptotically optimal. Unfortunately, the
current implementation is quite a bit uglier than the unweighted
version, and I haven't had a chance to perform benchmarks to see how the
constant factors compare. Hence moving it to an experimental branch.
These optimizations pass a test suite for detecting obvious errors. If
you find any bugs, do be sure to let me know. Also, if you happen to
have a test suite or benchmark suite for unification on hand, I'd love
to get a copy.
-- Notes and limitations
[1] At present it does not appear amenable for higher-rank structural
unification (a la HMF, MLF, or other System F type
