Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |


Fritz Henglein. Syntactic Properties of Polymorphic Subtyping. TOPPS Report D-293 DIKU, University of Copenhagen, May 1996.


Download paper: Adobe portable document (pdf) pdf

Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.


In this paper we study polymorphic subtyping, where the subtyping theory is \emph{not} required to be structural. We observe that type schemes with subtyping qualifications are strictly necessary in order to obtain principal typing. We identify a new instance relation on typing judgements, the \emph{halbstark} relation. It is a hybrid, lying in strength between Mitchell's original instance relation and Fuh and Mishra's lazy instance relation. We present a sound and complete type inference algorithm in the style of Milner's Algorithm W. The significance of the halbstark relation emerges from the fact that the algorithm is \emph{generic} in that it admits replacing typing judgements by \emph{any} halbstark-equivalent judgements at any point. This provides a generalized correctness argument for Algorithm W independent of any particular constraint simplification strategy chosen. Finally, we show that polymorphic typing judgements are preserved under let-unfolding, let-folding, and $\eta$-reduction, but not in general under $\beta$-reduction. The latter holds, though, if the subtyping discipline has the \emph{decomposition} property, which says that two function types are in a subtype relation only if their domain and range types are in the appropriate contra-/covariant subtype relation


Fritz Henglein

BibTex Reference

   Author = {Henglein, Fritz},
   Title = {Syntactic Properties of Polymorphic Subtyping},
   Institution = {DIKU, University of Copenhagen},
   Address = {Universitetsparken 1, DK-2100 Copenhagen, Denmark},
   Month = {May},
   Year = {1996}

EndNote Reference [help]

Get EndNote Reference (.ref)