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