[TAPL] Lecture 5. Subtyping

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.

 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,


 - For function types,


 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)


 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."



 - covariant


 - invariant

 - Source T and Sink T


 - invariant


 - cf. reference types

Base Types

 - Bool <: Nat

15.6 Coercision Semantcis for Subtyping

 - The problem of the subset semantics

 - Coercision semantics
 - Coherence