15. Subtyping - Subtype polymorphism - Object-oriented languages - cf. the use of subtyping vs. the insertion of run-time coercions 15.1 Subsumption - ( lam r:{x:Nat}. r.x ) {x=0,y=1} is not typable under the (extension of) simply typed lambda calculus - The goal of subtyping is to refine the typing rules so that they can accept terms like the one above. - S <: T (S is a subtype of T) [The principle of safe substitution] Any term of type S can safely be used in a context where a term of type T is expected. Inforamlly, 1) Every value described by S is also described by T. 2) The elements of S are a subset of the elements of T. 3) More refined interpretations of subtyping (Sec. 15.6) - The rule of subsumption Gamma |- t : S S <: T -------------------------- (T-Sub) Gamma |- t : T - Quiz. Use the rule of subsumption to make the following term be typable. ( lam r:{x:Nat}. r.x ) {x=0,y=1} 15.2 The Subtype Relation - A collection of inference rules for deriving statements of the form S <: T S is a subtype of T, or T is a supertype of S. - For record types, (S-REFL), (S-TRANS), (S-RCDWIDTH), (S-RCDDEPTH), (S-RCDPERM) - For function types, (S-ARROW) the (direction of the) subtype relation is reversed (contravariant) for the argument types while the subtype relation has the same direction for the result types (covariant). - (S-Top) S <: Top Example of typing derivation (P.185) 15.5 Other Features Ascription and Casting - (T-Ascribe) - (T-DOWNCAST) f = lam(x:Top) (x as {a:Nat}).a (Potentially unsafe!!) - Another approach: "Trust, but verify" 1) by insertion of runtimer verification (E-Ascribe) vs. (E-Downcast) We lose progress, since a well-typed program can certainly get stuck by attempting to evaluate a bad down-cast. 2) A failed down-cast raise a dynamic exception that can be caught and handled by the program. 3) Introduce the down-cast operator by a form of dynamic type test. - Down-casts in Java supports "poor-man's polymorphism." Variants Lists - covariant References - invariant - Source T and Sink T Arrays - invariant Channels - cf. reference types Base Types - Bool <: Nat 15.6 Coercision Semantcis for Subtyping - The problem of the subset semantics - Coercision semantics - Coherence