Higher-Order and Symbolic Computation, 12(3)237-282
Optimal Representations of Polymorphic Types with SubtypingAlexander Aiken, EECS Department, University of California, Berkeley, CA 94720-1776
Edward L. Wimmers, IBM Almaden Research Center, 650 Harry Rd., San Jose, CA 95120-6099
Jens Palsberg, Department of Computer Science, Purdue University, West lafayette, IN 47907
|
Abstract: Many type inference and program analysis systems
include notions of subtyping and parametric polymorphism. When used
together, these two features induce equivalences that allow types to
be simplified by eliminating quantified variables. Eliminating
variables both improves the readability of types and the performance
of algorithms whose complexity depends on the number of type
variables. We present an algorithm for simplifying quantified types in
the presence of subtyping and prove it is sound and complete for
non-recursive and recursive types. We also show that an extension of
the algorithm is sound but not complete for a type language with
intersection and union types, as well as for a language of constrained
types.
Keywords: types, polymorphism, subtyping |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)