[Haskell-cafe] Associative Commutative Unification
dons at galois.com
Sun Jul 6 22:38:56 EDT 2008
> 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,
"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.
More information about the Haskell-Cafe