Higher-Order Unification, Polymorphism and Subsorts
Tobias Nipkow
This paper analyzes the problems that arise in extending Huet's higher-order
unification algorithm from the simply typed lambda-calculus to one with type
variables. A simple, incomplete, but in practice very useful extension to
Huet's algorithm is discussed. This extension takes an abstract view of
types. As a particular instance we explore a type system with ML-style
polymorphism enriched with a notion of sorts. Sorts are partially ordered and
classify types, thus giving rise to an order-sorted algebra of types. Type
classes in the functional language Haskell can be understood as sorts in this
sense. Sufficient conditions on the sort structure to ensure the existence of
principal types are discussed. Finally we suggest a new type system for the
lambda-calculus which may pave the way to a complete unification algorithm
for polymorphic terms.
dvi
SpringerLink
BibTeX:
<![CDATA[
@inproceedings{Nipkow-CTRS-90,
author="Tobias Nipkow",
title="Higher-Order Unification, Polymorphism, and Subsorts",
booktitle="Proc.\ 2nd Int.\ Workshop Conditional and Typed Rewriting Systems",
editor={S. Kaplan and M. Okada},
year=1991,publisher=Springer,series=LNCS,volume=516}
]]></plaintext></p></div></div>