As a functional pearl, we describe an efficient, modularized implementation of unification using the state of mutable reference cells to encode substitutions. We abstract our algorithms along two dimensions, first abstracting away from the structure of the terms to be unified, and second over the monad in which the mutable state is encapsulated.
We choose this example to illustrate two important techniques which we
believe many functional programmers would find useful. The first of these is the definition of recursive {\tt data} types using two levels, a structure defining level, and a recursive knot tying level. The second is the use of rank-2 polymorphism inside Haskell's record types to implement a form of type parameterized modules.
