does anybody know how to do a term unification in Haskell in O(n), where n is length of the input terms? I know Montanari-Martelli algorithm for this, but I'm unable to code it in Haskell (in O(n)). I would need a destructive update of the directed graph representing terms (to do a substitution) and checking for cycles in directed graphs (these cycles emerge when unifying things like x=f(x) -- their detection is also called occurs-check).
Take a look at Tackling the Awkward Squad http://research.microsoft.com/Users/simonpj/papers/marktoberdorf/ to find out about (amongst other things) how to do destructive updates in Haskell, in IORefs. Note that instead of (IO a) you can use (ST s a) and runST to encapsulate a pure function that does destruction inside it. To see how some graph algorithms can be implemented elegantly in a pure functional language (Haskell) *without* destructive update, see Structuring Depth-First Search Algorithms in Haskell http://www.dcs.gla.ac.uk/~gnik/publications.html and Purely Functional Data Structures, by Chris Okasaki (find it on http://www.cup.org/) (and also various other papers by Okasaki, see Citeseer for example - I can't find Okasaki's home page any more) Haskell programmers don't usually do destructive updates, but it is possible to write programs using them, as long as these operations are carefully delimited so they don't violate the assumptions of the rest of the code. HTH. --KW 8-)