%O Report 
%F henglein96a
%A Henglein, Fritz
%T Syntactic Properties of Polymorphic Subtyping
%I DIKU, University of Copenhagen
%C Universitetsparken 1, DK-2100 Copenhagen, Denmark
%X 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
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1996.pdf
%8 May
%D 1996