DOC PREVIEW
Penn CIS 500 - Subtyping Lecture

This preview shows page 1-2-3-4-28-29-30-31-57-58-59-60 out of 60 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 60 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 60 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 60 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 60 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 60 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 60 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 60 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 60 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 60 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 60 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 60 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 60 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 60 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

Penn CIS 500 - Subtyping Lecture

Download Subtyping Lecture
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 Subtyping Lecture 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 Subtyping Lecture 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?