Generic Unification via Two-Level Types and Parameterized Modules

Tim Sheard

To appear at International Conference on Functional Programming (ICFP01), Firenze, Italy, 3-5 September 2001


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.

Server START Conference Manager
Update Time 11 May 2001 at 15:31:50
Start Conference Manager
Conference Systems