unification

[Koen Claessen]

 | Thank you for this information.  However, it does not
 | quite satisfy my curiosity:  are these purely
 | functional type checkers as efficient (big-O) as
 | imperative ones?  And if not, why not?

I usually use the ST monad to implement these kinds of
things, which gives the same performance and a functional
interface to the whole thing.

Papers you should check are:

  * Typed Logical Variables in Haskell,
    by me and Peter Ljunglöf.

  * Polytypic Unification,
    by Patrik Jansson and Johan Jeuring.

/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.