CIS 500Software FoundationsFall 2006November 1Notes from Yesterday’s EmailDiscussionSome lessonsIThis is generally a crunch-time in the semesterISlow down a little and give people a chance to catch upIOnce you’re confused, it’s hard to know what to askISo not necessarily a problem if people are not asking manyquestions, but definitely a sign to slow down moreIWorking simple examples in class is goodI... in part bec ause it makes people think of other questionsISome hard homework problems have been too vagueINot enough information −→ need to look at the solution tosee what is wanted −→ hard to think independently any moreIBig picture has be en ge tting a little los t in the detailsBig PicturePlan for the rest of the semesterIThis week: Basic subtypingINext week: Review and midtermINov 13,15: Algorithmics of subtypingINov 20,22: Modeling OO languages in typed lambda-calculusINov 27,29: Featherweight JavaIDec 4,6: To be decided (Parametric polymorphism? MLmo dule s yste m? ...)IDec 20: Final examWhat’s it all forITechniques and notations for formalizing languages andlanguage constructsIinductive definitions, operational semantics, typing andsubtyping relations, etc.IRecords, exceptions, etc. as case studiesIStrong intuitions about fundamental safety propertiesIEspecially: Healthy scepticism and good investigative skills forhow things can be broken!ISome specific fundamental building blocks of languagesIVariables, scope, and bindingIFunctions and their types (higher-order programming)IReferences (mutable state, aliasing)ISubtypingIObjects and classesUltimately, the goal is to give you the ability to put all thistogether and formalize your own languages or language features.Subtyping (again)MotivationWe want terms like(λr:{x:Nat}. r.x) {x=0,y=1}to b e well typed.Similarly, in object-oriented languages, we want to be able todefine hierarchies of classes, with classes lower in the hierarchyhaving richer interfaces than their ancestors higher in the hierarchy,and use instances of richer classes in situations where one of theirancestors are expected.SubsumptionWe achieve the effect we want by:1. defining a new subtyping relation between types, writtenS <: T2. adding a new rule of subsumption to the typing relation:Γ ` t : S S <: TΓ ` t : T(T-Sub)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)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:{}}Another example{x:Nat,y:Nat} <: {y:Nat}(board)Aside: Structural vs. decl ared subtypingThe subtype relation we have defined is structural: We decidewhether S is a subtype of T by examining the structure of S and T.By contrast, the subtype relation in most OO languages (e.g.,Java) is explicitly declared: S is a subtype of T only if theprogrammer has stated that it should be.There are pragmatic arguments for both.For the moment, we’ll concentrate on structural subtyping, whichis the more fundamental of the two. (It is sound to declare S to bea subtype of T only when S is structurally a subtype of T.)We’ll come back to declared subtyping when we talk aboutFeatherweight Java.Properties of SubtypingSafetyStatements of progress and preservation theorems are unchangedfrom λ→.Proofs be com e 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)An Inversion Lemma for SubtypingLemma: If U <: T1→T2, then U has the form U1→U2, with T1<: U1and U2<: T2.Proof: By induction on subtyping derivations.Case S-Arrow: U = U1→U2T1<: U1U2<: T2Immediate.Case S-Refl: U = T1→T2By S-Refl (twice), T1<: T1and T2<: T2, as required.Case S-Trans: U <: W W <: T1→T2Applying the IH to the second subderivation, we find that W hasthe form W1→W2, with T1<: W1and W2<: T2. Now the IH appliesagain (to the first sub derivation), telling us that U has the formU1→U2, with W1<: U1and U2<: W2. By S-Trans, T1<: U1, and,by S-Trans again, U2<: T2, as required.An Inversion Lemma for SubtypingLemma: If U <: T1→T2, then U has the form U1→U2, with T1<: U1and U2<: T2.Proof: By induction on subtyping derivations.Case S-Arrow: U = U1→U2T1<: U1U2<: T2Immediate.Case S-Refl: U = T1→T2By S-Refl (twice), T1<: T1and T2<: T2, as required.Case S-Trans: U <: W W <: T1→T2Applying the IH to the second subderivation, we find that W hasthe form W1→W2, with T1<: W1and W2<: T2. Now the IH appliesagain (to the first sub derivation), telling us that U has the formU1→U2, with W1<: U1and U2<: W2. By S-Trans, T1<: U1, and,by S-Trans again, U2<: T2, as required.An Inversion Lemma for SubtypingLemma: If U <: T1→T2, then U has the form U1→U2, with T1<: U1and U2<: T2.Proof: By induction on subtyping derivations.Case S-Arrow: U = U1→U2T1<: U1U2<: T2Immediate.Case S-Refl: U = T1→T2By S-Refl (twice), T1<: T1and T2<: T2, as required.Case S-Trans: U <: W W <: T1→T2Applying the IH to the second subderivation, we find that W hasthe form W1→W2, with T1<: W1and W2<: T2. Now the IH appliesagain (to the first sub derivation), telling us that U has the formU1→U2, with W1<: U1and U2<: W2. By S-Trans, T1<: U1, and,by S-Trans again, U2<: T2, as required.An Inversion Lemma for SubtypingLemma: If U <: T1→T2, then U has the form U1→U2, with T1<: U1and U2<: T2.Proof: By induction on subtyping derivations.Case S-Arrow: U = U1→U2T1<: U1U2<: T2Immediate.Case S-Refl: U = T1→T2By S-Refl (twice), T1<: T1and T2<: T2, as required.Case S-Trans: U <: W W <: T1→T2Applying the IH to the second subderivation, we find that W hasthe form W1→W2, with T1<: W1and W2<: T2. Now the IH appliesagain (to the first sub derivation), telling us that U has the formU1→U2, with W1<: U1and U2<: W2. By S-Trans, T1<: U1, and,by S-Trans again, U2<: T2, as required.An Inversion Lemma for SubtypingLemma: If U <: T1→T2, then U has the form U1→U2, with T1<: U1and U2<: T2.Proof: By induction on subtyping derivations.Case S-Arrow: U = U1→U2T1<: U1U2<: T2Immediate.Case S-Refl: U = T1→T2By S-Refl (twice), T1<: T1and T2<: T2, as required.Case S-Trans: U <: W W <: T1→T2Applying the