Optimal Representations of Polymorphic Types with Subtyping

Alexander Aiken, Edward L. Wimmers and Jens Palsberg

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-96-909
July 1996

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1996/CSD-96-909.pdf

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.


BibTeX citation:

@techreport{Aiken:CSD-96-909,
    Author = {Aiken, Alexander and Wimmers, Edward L. and Palsberg, Jens},
    Title = {Optimal Representations of Polymorphic Types with Subtyping},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1996},
    Month = {Jul},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1996/5474.html},
    Number = {UCB/CSD-96-909},
    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.}
}

EndNote citation:

%0 Report
%A Aiken, Alexander
%A Wimmers, Edward L.
%A Palsberg, Jens
%T Optimal Representations of Polymorphic Types with Subtyping
%I EECS Department, University of California, Berkeley
%D 1996
%@ UCB/CSD-96-909
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1996/5474.html
%F Aiken:CSD-96-909