[ Pobierz całość w formacie PDF ]
.4 Soundness of translation for 327In each of the above derivations, we can replace expressions of the formby in the last line because the argument of involvesonly type variables already in.Recall thatmethfun self SelfTypelet close SelfType Y VisObj Y,M (MyType)closeobj [IVR (MyType)] [M (MyType)]in meth [MyType][SelfType]By the Let and Function typing rules,methfun SelfType M MyTypeIt follows from the above and the type-checking rules Function and Pair ofthatinst methfunIV MyType SelfType M MyTypeFinally, by the type-checking rule BdPolyFunc in Figure 9.9,M M IVR IVrefinst [MyType] methfunM M IVR IVrefIV MyType SelfType M MyTypeThusclass inst meth ClassType IV MSubclass Omitted here.Similar to class.Message SupposeE m T UbecauseE UandU ObjectType m T MyType 328 16 AddingMyTypeto Object-Oriented Programming LanguagesBy Lemma 16.2.2, (U) =ObjectTypeM(MyType) for someMsuch thatM TpFunc(MT).m:T(MT)By Theorem 16.4.1,M TpFunc MT m T MTwhere TpFunc MT m T MT MT m T MT.Hence for all type identifiers, IVR , MT ,IVR IVR M MT(16.1)IVR IVR m T MTBy induction,E ULetMT U ObjectTypeM MyType Obj MY Y Y M MTBy definition,E m open E as IVR vo in proj vo proj vo mBy equation 16.1 and subsumption,vo IVR IVR M MTvo IVR IVR m T MTBy the projection typing rules and the Selection rule of ,vo IVR IVR M MTproj vo proj vo m T MTIt follows from the Unpack rule thatopen E as IVR vo in proj vo proj vo m T MTHenceE m T UThe reader should be sure to understand why the match, rather than sub-type, bound onUwas sufficient for proving the soundness of this rule. 16.4 Soundness of translation for 329Inst Vble SupposeE l T VbecauseE UandUvisVisObjectType l T MyTypewhere (U) =VisObjectType(IVR(MyType),M(MyType)) and (V) =Ob-jectTypeM(MyType).By Lemma 16.2.3,IVR TpFunc MT l T MTand hence by Theorem 16.4.1,IVR TpFunc MT l T MTBy induction,E VisObjectType IVR MyType M MyTypewhile, by definition,VisObjectType IVR MyType M MyTypeVisObj IVR (MT), M (MT)IVR MT IVR MT M MTwhere MT = V = ObjectTypeM MyType = Obj ( M ).By rule Proj,proj E IVR MTand thus by subsumption in ,proj E l T MTBy definition,E l proj E lTherefore, by the Selection type-checking rule of ,E l T MTand thusE l T V 330 16 AddingMyTypeto Object-Oriented Programming LanguagesSelf Message This case is similar to sending messages to regular objectsexcept that it is not necessary to unpack the existential.16.5 SummaryIn this chapter we designed the language by adding aMyTypecon-struct to.The type expressionMyTyperepresents the type ofselfinside of a class definition.As the meaning ofselfchanges automaticallywhen moving from a class to a subclass, so does the meaning ofMyType.Just as this automatic change of the meaning ofselfis extremely helpfulwhen inheriting methods from a superclass, so is the automatic change inthe meaning ofMyType.In particular, it provides a way to support covariantchanges to types in classes, whether they are the types of instance variables,method parameters, or method return types.While subclasses of classes whose methods have parameters with typeMy-Typedo not generate object types that are in the subtype relation, they dogenerate object types that match.While the loss of subtyping might be seento be a disadvantage, we saw that matching is often all that is needed.Inparticular, if typeT Sthen any method ofSwill also be inT, and thetype of that method inTwill be a subtype of that inS.In the next chapter we will extend with match-bounded poly-morphism and show the expressiveness of the combination ofMyTypeandmatching.YLFMAET 17 Match-Bounded PolymorphismIn this chapter we add bounded polymorphism to.Of course wehave already done this in extending to.The difference isthat this time we will be more interested in introducing match-bounded poly-morphism rather than polymorphism in which the bounds are expressed interms of the subtyping relation.We have already seen that in languages withMyType, subclasses gener-ate types that are in the matching relation, and thus seems a more naturalrelation than subtyping.We will also see that we can simplify many oc-currences of F-bounded polymorphism to simple match-bounded polymor-phism.Match-bounded polymorphism also has the added benefit of fittingmore smoothly with subclasses than does F-bounded polymorphism.17.1 Benefits of match-bounded polymorphismWhile the matching relation does not allow values of one object type to mas-querade as values of the other, as is the case with subtyping, we have seen itprovides useful information on the availability and types of methods.Inter-estingly, it is also very useful as a constraint on type variables for polymor-phism.In fact, the use ofMyTypeand matching will allow the possibility ofdispensing with most of the uses of F-bounded polymorphism.Recall from the last chapter the following example of F-bounded polymor-phism.OrderableF(t TopObject) = ObjectType {equal:t Boolean;greaterThan:t Boolean;lessThan:t Boolean} 332 17 Match-Bounded Polymorphismclass BPOrderedList(Elt OrderableF(Elt)) {.};The use of F-bounded polymorphism was needed in parameterized classBPOrderedListbecause the constraint onEltwas that it haveequal,greaterThan, andlessThanmethods that took parameters of typeElt.Thus when one of these methods is sent to an element of typeElt, it shouldhave the same type as the receiver.Of course this should suggest to us theuse ofMyType.DefineOrderableMT = ObjectType {equal:MyType Boolean;greaterThan:MyType Boolean;lessThan:MyType Boolean}UnlikeOrderableF, the typeOrderableMTneed not be parameterized
[ Pobierz całość w formacie PDF ]