Many functions have to be written over and over again for different
datatypes, either because datatypes change during the development of
programs, or because functions with similar functionality are needed
on different datatypes.
Examples of such functions are pretty printers, debuggers, equality
functions, unifiers, pattern matchers, rewriting functions,
etc. Such functions are called polytypic functions.
A polytypic function is a function that is defined by induction on
the structure of user-defined datatypes.
This paper introduces polytypic functions, and shows how to
construct and reason about polytypic functions.
A larger example is studied in detail: polytypic functions for term
rewriting and for determining whether a collection of rewrite rules
is normalising.
Last modified: Fri Feb 19 11:18:01 MET 1999
by
Patrik Jansson /
NOpatrikjSP@AMchalmers.se