The Haskell typechecker contains a nice example of a unifier for freely generated terms. My focus is on equational unification, but thanks anyway.
John On Sun, Jul 6, 2008 at 10:38 PM, Don Stewart <[EMAIL PROTECTED]> wrote: > 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 [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
