SubtypingProperties of SubtypingSubtyping with Other FeaturesAlgorithmic SubtypingCIS 500Software FoundationsFall 2006October 30SubtypingMotivationWith our usual typing rule for applicationsΓ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)the term(λr:{x:Nat}. r.x) {x=0,y=1}is not well typed.But this is silly: all we’re doing is passing the function a betterargument than it needs.MotivationWith our usual typing rule for applicationsΓ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)the term(λr:{x:Nat}. r.x) {x=0,y=1}is not well typed.But this is silly: all we’re doing is passing the function a betterargument than it needs.PolymorphismA polymorphic function may be applied to many different types ofdata.Varieties of polymorphism:IParametric polymorphism (ML-style)ISubtype polymorphism (OO-style)IAd-hoc polymorphism (overloading)Our topic for the next few lectures is subtype polymorphism, whichis based on the idea of subsumption.SubsumptionMore generally: some types are better than others, in the sensethat a value of one can always safely be used where a value of theother is expected.We c an formalize this intuition by introducing1. a subtyping relation between types, written S <: T2. a rule of subsumption stating that, if S <: T, then any value oftype S can also be regarded as having type TΓ ` t : S S <: TΓ ` t : T(T-Sub)ExampleWe will define subtyping between record types so that, for example,{x:Nat, y:Nat} <: {x:Nat}So, by subsumption,` {x=0,y=1} : {x:Nat}and hence(λr:{x:Nat}. r.x) {x=0,y=1}is we ll typed.The Subtype Relation: Records“Width subtyping” (forgetting fields on the right):{li:Tii∈1 ..n+k} <: {li:Tii∈1 ..n}(S-RcdWidth)Intuition: {x:Nat} is the type of all records with at least anumeric x field.Note that the record type with more fie lds is a subtype of therecord type with fewer fields.Reason: the type with more fields places a stronger constraint onvalues, so it describes fewer values.The Subtype Relation: RecordsPermutation of fields:{kj:Sjj∈1 ..n} is a permutation of {li:Tii∈1 ..n}{kj:Sjj∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdPerm)By using S-RcdPerm together with S-RcdWidth andS-Trans allows us to drop arbitrary fields within records.The Subtype Relation: Records“Depth subtyping” within fields:for each i Si<: Ti{li:Sii∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdDepth)The types of individual fields may change.ExampleS-RcdWidth{a:Nat,b:Nat} <: {a:Nat}S-RcdWidth{m:Nat} <: {}S-RcdDepth{x:{a:Nat,b:Nat},y:{m:Nat}} <: {x:{a:Nat},y:{}}VariationsReal languages often choose not to adopt all of these recordsubtyping rules. For example, in Java,IA subclass may not change the argument or result types of amethod of its superclass (i.e., no depth subtyping)IEach class has just one superclass (“single inheritance” ofclasses)−→ each class member (field or method) can beassigned a single index, adding new indices “on theright” as more me mbers are added in subclasses(i.e., no permutation for classes)IA class may implement multiple interfaces (“multipleinheritance” of interfaces)I.e., permutation is allowed for interfaces.The Subtype Relation: Arrow typesT1<: S1S2<: T2S1→S2<: T1→T2(S-Arrow)Note the order of T1and S1in the first premis e. The subtyperelation is contravariant in the left-hand sides of arrows andcovariant in the right-hand sides.Intuition: if we have a functionf of type S1→S2, then we knowthat f accepts elements of type S1; clearly, f will also acceptelements of any subtype T1of S1. The type of f also tells us thatit returns elements of type S2; we c an also view these resultsbelonging to any supertype T2of S2. That is, any function f oftype S1→S2can also be viewed as having type T1→T2.The Subtype Relation: TopIt is convenient to have a type that is a supertype of every type.We introduce a new type constant Top, plus a rule that makes Topa maximum element of the subtype relation.S <: Top(S-Top)Cf. Object in Java.The Subtype Relation: General rulesS <: S(S-Refl)S <: U U <: TS <: T(S-Trans)Subtype relationS <: S(S-Refl)S <: U U <: TS <: T(S-Trans){li:Tii∈1 ..n+k} <: {li:Tii∈1 ..n}(S-RcdWidth)for each i Si<: Ti{li:Sii∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdDepth){kj:Sjj∈1 ..n} is a permutation of {li:Tii∈1 ..n}{kj:Sjj∈1 ..n} <: {li:Tii∈1 ..n}(S-RcdPerm)T1<: S1S2<: T2S1→S2<: T1→T2(S-Arrow)S <: Top(S-Top)Properties of SubtypingSafetyStatements of progress and preservation theorems are unchangedfrom λ→.Proofs become a bit more involved, because the typing relation isno longer syntax directed.Given a derivation, we don’t always know what rule was used inthe last step. The rule T-Sub could appear anywhere.Γ ` t : S S <: TΓ ` t : T(T-Sub)PreservationTheorem: If Γ ` t : T and t −→ t0, then Γ ` t0: T.Proof: By induction on typing derivations.(Which cases are likely to be hard?)Subsumption caseCase T-Sub: t : S S <: TBy the induction hypothesis, Γ ` t0: S. By T-Sub, Γ ` t : T.Not hard!Subsumption caseCase T-Sub: t : S S <: TBy the induction hypothesis, Γ ` t0: S. By T-Sub, Γ ` t : T.Not hard!Subsumption caseCase T-Sub: t : S S <: TBy the induction hypothesis, Γ ` t0: S. By T-Sub, Γ ` t : T.Not hard!Application caseCase T-App:t = t1t2Γ ` t1: T11→T12Γ ` t2: T11T = T12By the inversion lemma for evaluation, there are three rules bywhich t −→ t0can be derived: E-App1, E-App2, andE-AppAbs. Proceed by cases.Subcase E-App1: t1−→ t01t0= t01t2The result follows from the induction hypothesis and T-App.Γ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)t1−→ t01t1t2−→ t01t2(E-App1)Application caseCase T-App:t = t1t2Γ ` t1: T11→T12Γ ` t2: T11T = T12By the inversion lemma for evaluation, there are three rules bywhich t −→ t0can be derived: E-App1, E-App2, andE-AppAbs. Proceed by cases.Subcase E-App1: t1−→ t01t0= t01t2The result follows from the induction hypothesis and T-App.Γ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)t1−→ t01t1t2−→ t01t2(E-App1)Application caseCase T-App:t = t1t2Γ ` t1: T11→T12Γ ` t2: T11T = T12By the inversion lemma for evaluation, there are three rules bywhich t −→ t0can be derived: E-App1, E-App2, andE-AppAbs. Proceed by cases.Subcase E-App1: t1−→ t01t0= t01t2The result follows from the induction hypothesis and T-App.Γ ` t1: T11→T12Γ ` t2: T11Γ ` t1t2: T12(T-App)t1−→ t01t1t2−→ t01t2(E-App1)Case T-App (continued):t = t1t2Γ ` t1: T11→T12Γ ` t2: T11T = T12Subcase E-App2: t1= v1t2−→ t02t0= v1t02Similar.Γ ` t1: T11→T12Γ ` t2:
View Full Document