d Abstract) Alexander Aiken1 and Edward L. Wimmers2 and Jens Palsberg3 1 EECS Department, University of California at Berkeley, Berkeley, CA 94720-1776. 2 IBM Almaden Research Center, 650 Harry Rd., San Jose, CA 95120-6099. 3 Department of Computer Science, Purdue University, West Lafayette, IN 47907. 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.
Alexander Aiken, Edward L. Wimmers, Jens Palsberg