DOC PREVIEW
Penn CIS 500 - CIS 500 LECTURE NOTES

This preview shows page 1-2-3-4-30-31-32-33-34-62-63-64-65 out of 65 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 65 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Notes from Yesterday's Email DiscussionBig PictureSubtyping (again)Properties of SubtypingSubtyping with Other FeaturesAlgorithmic SubtypingCIS 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 c onfused, 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 s imple e xamples in class is goodI... in part because 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 been getting a little lost 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? MLmodule system? ...)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 be well typed.Similarly, in object-oriented languages, we want to be able todefine hierarchies of classe s, w ith classe s 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 expe cte d.SubsumptionWe achiev e 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. declared subtypingThe subtype relation we have defined is structural: We decidewhether S is a subty pe 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 com e back to declared subtyping when we talk ab outFeatherweight Java.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)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 subderivation), 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 subderivation), 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 subderivation), 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 subderivation), 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<:


View Full Document

Penn CIS 500 - CIS 500 LECTURE NOTES

Download CIS 500 LECTURE NOTES
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view CIS 500 LECTURE NOTES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CIS 500 LECTURE NOTES 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?