Generic unification via two-level types and parameterized modules

As a functional pearl, we describe an efficient, modularized implementation of unification using the state of mutable reference cells to encode substi tutions. We abstract our algorithms along two dimensions, first abstracting away from the structure of the terms to be unified, and second over the mo nad in which the mutable state is encapsulated. We choose this example to illustrate two important techniques that we belie ve many functional programmers would find useful. The first of these is the definition of recursive data types using two levels: a structure defining level, and a recursive knot-tying level. The second is the use of rank-2 po lymorphism inside Haskell's record types to implement a form of type parame terized modules.