CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Functional Pearl: Polytypic Unification

Patrik Jansson (Institutionen för datavetenskap, Funktionell programmering ; Institutionen för datavetenskap, Programmeringslogik) ; Johan Jeuring
Journal of Functional Programming (0956-7968). Vol. 8 (1998), 5, p. 527-536.
[Artikel, refereegranskad vetenskaplig]

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.

Denna post skapades 2006-10-09. Senast ändrad 2014-09-02.
CPL Pubid: 10122


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för datavetenskap, Funktionell programmering (2002-2004)
Institutionen för datavetenskap, Programmeringslogik (2002-2004)


Teoretisk datalogi

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:

Functional Polytypic Programming --- Use and Implementation