@inproceedings{bc7d97fb5e674e7ab54013fb03516c9e,
title = "Higher-order unification, polymorphism, and subsorts",
abstract = "This paper analyzes the problems that arise in extending Huet's higher-order unification algorithm from the simply typed λ-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 λ-calculus which may pave the way to a complete unification algorithm for polymorphic terms.",
author = "Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1991.; 2nd International Workshop on Conditional and Typed Rewriting Systems, CTRS 1990 ; Conference date: 11-06-1990 Through 14-06-1990",
year = "1991",
doi = "10.1007/3-540-54317-1_112",
language = "English",
isbn = "9783540543176",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "436--447",
editor = "Stephane Kaplan and Mitsuhiro Okada",
booktitle = "Conditional and Typed Rewriting Systems - 2nd International CTRS Workshop, Proceedings",
}