Unification, or two-way pattern matching, is the process of solving
an equation involving two
first-order terms with variables. Unification is used in type inference
in many programming
languages and in the execution of logic programs. This means that unification
algorithms have
to be written over and over again for different term types. Many other
functions also make
sense for a large class of datatypes; examples are pretty printers, equality
checks, maps etc.
They can be defined by induction on the structure of user-defined datatypes.
Implementations
of these functions for different datatypes are closely related to the structure
of the datatypes.
We call such functions polytypic. This paper describes a unification algorithm
parametrised
on the type of the terms, and shows how to use polytypism to obtain a unification
algorithm
that works for all regular term types.