Foundations for the Implementation of Higher-Order Subtyping

We show how to implement a calculus with higher-order subtyping and subkinding by replacing uses of implicit subsumption with explicit coercions. To ensure this can be done, a polymorphic function is adjusted to take, as an additional argument, a proof that its type constructor argument has the desired kind. Such a proof is extracted from the derivation of a kinding judgement and may in turn require proof coercions, which are extracted from subkinding judgements. This technique is formalized as a type-directed translation from a calculus of higher-order subtyping to a subtyping-free calculus. This translation generalizes an existing result for second-order subtyping calculi (such as F ). We also discuss two interpretations of subtyping, one that views it as type inclusion and another that views it as the existence of a well-behaved coercion, and we show, by a type-theoretic construction, that our translation is the minimum consequence of shifting from the inclusion interpretation to t...

• Type: Conference
• Year: 1997
• Where: ICFP
• Authors: Karl Crary
• Keywords: ICFP 1997, Programming Languages, Second-order Subtyping Calculi, Show, Type Constructor Argument