[ Pobierz całość w formacie PDF ]
.The underlying semantics is based on an object calculus sim-ilar to that used in [FM98].In Section 13.2, we noted the difficulties with the coherence of a transla-tion based on derivations of typing judgements.The problem is that twodifferent typing derivations of the same judgement may result in differenttranslations.Curien and Ghelli, in their paper Coherence of subsumption,minimum typing and type-checking in [CG92] provided a careful anal-ysis of coherence issues in a version of the bounded polymorphic lambdacalculus.They provided a rewriting system for typing derivations that pro-vide the basis of a proof that a semantics is well-defined.Mitchell s text Historical Notes and References for Section III 287[Mit96] provides a compact discussion of the issues and techniques to showcoherence.A style of writing semantics for object-oriented languages that we have notdiscussed here is the use of row variables.Row variables were introduced byWand [Wan87, Wan89] in connection with a type inference scheme for sim-ple objects, and were used in Mitchell s semantics of typed object-orientedlanguages [Mit90].They can be used in specifying partial information aboutthe method suite of an object, but allow further extension.(The version usedby Mitchell also allows the specification of negative information.) Row typesare especially useful with type inference.The language Objective ML is the theoretical basis of the language Objec-tive CAML, an extension of ML with classes and objects.The semantics ofObjective ML is expressed in terms of row variables.The language supportstype inference, but requires explicit coercions to treat an object as having thetype of one of its superclasses.The paper, Objective ML: An effective object-oriented extension to ML [RV98], describes the language and its semantics,as well as providing a host of references on row variables and type inferencein object-oriented languages.Another fairly minimal extension to ML sup-porting features of object-oriented languages is Simple Objects for StandardML [RR96], by Reppy and Riecke.There has been a great deal of interest in the semantics of Java and thesafety of its type system.Representative papers are by Drossopoulou et al.[DE98, DEK99] and Börger and Schulte [BS98].The design of FeatherweightJava by Igarashi et al.[IPW99] is an important development for languagetheoreticians wanting to test their language ideas with a simplified versionof Java that is amenable to theoretical analysis.The full Java language isextremely complicated, and many of these complications get in the way ofcareful study of particular language features.Because Featherweight Javahas a simple semantics, it is easy to extend it to encompass new features andyet still prove type soundness. This page intentionally left blank Part IVExtending SimpleObject-Oriented Languages This page intentionally left blankYLFMAET Adding Bounded Polymorphism15 toAdding F-bounded parametric polymorphism of the sort discussed in Sec-tion 4.1 to is relatively straightforward, as it is not that different fromthe addition of parametric polymorphism to the lambda calculus.In thischapter we provide the details of an extension, , of.Thereader is invited to go back and review Section 4.1 for the motivation to addF-bounded polymorphism.15.1 IntroducingWe begin by introducing the syntax of type and value expressions inand then providing type-checking rules.We follow this with a few simpleexamples of the use of F-bounded polymorphism.We first add a kind system like that for the polymorphic lambda calculusin Chapter 9.However, for simplicity we restrict the kinds to those that taketypes as arguments rather than elements of higher kinds.We represent thekind of all types by*.Kind * *Type constructors are either types or functions that take a type as a pa-rameter and return a constructor.We writeU:: to indicate thatUis a typeconstructor with kind.Let be a set of type constants containing thetype constantTopObject.Let be a set of record labels, and aset of typeidentifiers.Constructor expressions of , ,(with their associated kinds) are defined as follows:1.Ifc , thenc::*.2.Ift , thent::*. 292 15 Adding Bounded Polymorphism to3.IfT::*andU:: , thenTpFunc(t).U::*.4.IfT::*andF::* , thenF(T)::.5.IfT::*andU::*, thenForAll(t T).U::*.6.The elided elements in the last case consist of all of the type definitions from, all given with kind*.We omit them here because they would over-whelm the new constructor expressions.IfThas kind*, then we say thatTis a type expression of (writtenT ).Notice that the constructor identifiers andconstants are only of kind*(and hence will be referred to as type identifiersand constants).Constructor expressions of the formTpFunc(t).Urepresent functions tak-ing a typeTto type [T/t]U.The expressionF(T)represents the applicationof type functionFto argumentT.IfTandUare types, thenForAll(t T).Uis the type of polymorphicfunctions taking subtypes ofTto values of typeU.While constructors may only take types as arguments, it is possible toobtain type functions taking several type parameters by writing them in acurried fashion, that is, defining a type function that returns another typefunction.An example isTpFunc(t).TpFunc(u).t u.As in , we include in Figure 15.1 a congruence rule, FuncAppCong, forsimplifying constructor applications.In combination with the correspond-ing subtyping and type-checking rules, Cong and Congruence, this willallow us to simplify constructor applications appearing in expressions to betype-checked.(While we don t bother to write the corresponding rules, thecongruence relation is reflexive, symmetric, and transitive.)It is important not to confuse polymorphic types those types with theformForAll(t T)
[ Pobierz całość w formacie PDF ]
