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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe