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
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.
The core of the unification algorithm is written in Haskell
(using the interpreter Hugs)
and the polytypic part is written in the Haskell extension
The full code is available as
.tar.gz and in
Last modified: Thu Feb 18 17:22:24 MET 1999
Patrik Jansson /