[Haskell-cafe] Associative Commutative Unification

[Don Stewart]

ramsdell0:
> I'd like to write an obviously correct implementation of a unifier, a
> program that when given two terms, finds a substitution that makes the
> two terms equal.  The phrase "obviously correct" is meant to imply
> that the clarity of the code trumps efficiency.  As near as I can
> tell, high performance unifiers are full of side-effects, and
> achieving the same performance without side-effects in Haskell is
> difficult or impossible.
> 
> In contrast, it is easy to write obviously correct Hasklell
> implementations of unifiers for freely generated term algebras.  One
> can use Lawrence Paulson's code in ML for the Working Programmer as a
> template or follow Martelli and Montanari's simple set of rules.
> 
> My problem is one of my operators is multiplication, which is
> associative and commutative.  These two properties make unification
> much more difficult.  Mark Stickel described a complete unification
> algorithm for this problem, but the task of translating his
> description into an obviously correct Haskell program appears to be
> difficult.  For example, the algorithm requires the generation of the
> basis of solutions to linear homogeneous diophantine equations.  I
> haven't located an algorithm for this part yet.
> 
> If you have experience implemented equational unification in Haskell,
> please share it.

"Typing Haskell in Haskell" lives here,

    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/thih

"a Haskell program that implements a Haskell typechecker, thus providing
a mathematically rigorous specification in a notation that is familiar
to Haskell users. We expect this program to fill a serious gap in
current descriptions of Haskell, both as a starting point for
discussions about existing features of the type system, and as a
platform from which to explore new proposals"

Might be useful as a starting point.

-- Don