Hostname: page-component-78c5997874-ndw9j Total loading time: 0 Render date: 2024-11-09T07:02:22.871Z Has data issue: false hasContentIssue false

Polytypic unification

Published online by Cambridge University Press:  01 September 1998

PATRIK JANSSON
Affiliation:
Computing Science, Chalmers University of Technology, S-412 96 Göteborg, Sweden
JOHAN JEURING
Affiliation:
Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508 TB, Utrecht, The Netherlands
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
FUNCTIONAL PEARL
Copyright
© 1998 Cambridge University Press
Supplementary material: Link
Link
Submit a response

Discussions

No Discussions have been published for this article.