[ Pobierz całość w formacie PDF ]
.The rather simple solution344 17 Match-Bounded Polymorphismis to initialize X to the set of all type identifiers that are declared with amatch-bound in the generalized type constructor constraint system used inthe corresponding typing, subtyping, or matching rule.The following theorem corresponds to Theorem 13.1.9 and is proved in thesame way.Theorem 17.5.1 LetSandTbe types of such thatS Tand letX t there exists aTsuch that (t T)ThenX X XS TThe translation of matching types results in functions from types to typesthat are in the subtype relation.Theorem 17.5.2 LetSandTbe types of such thatS Tand letX t there exists aTsuch that (t T)ThenX XXS TProof.We give a proof by induction on the number of steps in the proofthat S T.The proofs for TopObject , Reflex , Transitive , andType Abbrev are trivial.SupposeObjectType M MyType ObjectType M MyTypebecauseM MBy Theorem 17.5.1,X X XM MButXXObjectType M MyType M17.5 Soundness of the translation of 345andXXObjectType M MyType Mso we are done.Now we wish to show that if a type can be assigned to an expression of, then the translation of that type can be assigned to the translatedexpression.Theorem 17.5.3 LetEbe an expression of that does not involvenil, letX t there exists aTsuch that t Tand supposeE SThenX X X XE SProof.We only show the cases for expression identifiers and for match-bounded polymorphic expressions.XIdentifier Suppose id Tbecause id T.Then id TX X X X, and hence id T.Match-bounded polymorphism SupposepolyFunc t T U is Block ForAll t T Ubecause t T Block U.Let  = t T and X =X t.By induction,X X X XBlock UXX XBy definition t T.Thus,XX X X Xt T Block Uand hence by the PolyFunc rule of ,X XX X X Xt T Block t T UButXX XForAll t T U t T U346 17 Match-Bounded PolymorphismandXX XpolyFunc t T U is Block t T BlockX XBy the equivalent of Lemma 13.1.2, M = M for allM.Putting this alltogether, we getX X XpolyFunc t T U is BlockXForAll t T UMatch-bounded polymorphic application SupposeE[T ] T t UbecauseE ForAll t T UandT T t TBy induction,X X X XE ForAll t T UandX XXT T t TThe typing judgement translates toXX X X XE t T Uwhere X X t.X X XIt is easy to show that T t T =[ T /t] T , where thas kind* *.It follows thatX X XX XT T t Tand hence by rule BdPolyApp of thatX X XX X XE [ T ] T t UAs a result,X X X XE [T ] T t U17.6 Summary 34717.6 SummaryIn this chapter we extended to a language that supportsmatch-bounded polymorphism, a form of bounded polymorphism in whichthe bound on type parameters is expressed in terms of the matching relationrather than subtyping.As the examples in Section 17.3 illustrate, this is oftenexactly what is needed.While F-bounded polymorphism can also expressmany of the same examples, match-bounded polymorphism is a simpler con-struct from the point of view of programmers and fits better with subclassesin languages withMyType.The language is very rich, includingMyType, subtyping andmatching, and F-bounded polymorphism where the bounds may be given interms of either subtyping or matching.In the next chapter we step back toinvestigate the possibility of simplifying the language while retaining similarexpressiveness.In particular, we will consider the possibility of droppingsubtyping from the language.This page intentionally left blankSimplifying: Dropping Subtyping18 for Matching Perfection is finally attained not when there is no longer anything toadd, but when there is no longer anything to take away. Antoine de Saint-ExupéryIn this chapter we provide a brief introduction to a simplified version of thelanguage that arises by dropping the notion of subtype and replac-ing it with a notion of hash types.While the language is very expressive, it may be too rich a lan-guage.The notions of subtyping and matching are very similar, differingon object types only based on whether or notMyTypeoccurs as the type of aparameter in a method.Because both subtype and match-bounded polymor-phism are available to programmers, they will have to decide which relationis most appropriate whenever defining polymorphic functions.Moreover, while subclasses will always give rise to object types whichmatch those of the superclass, they will not always be in the subtype rela-tion.However, we have seen that subclasses always result in object typesthat match those of the superclass.Thus, if we believe theMyTypeconstructto be useful (and we do!), it may be worth exploring whether it might bepossible to have matching replace subtyping in an object-oriented language.18.1 Can we drop subtyping?Because it is not wise to include extraneous features in programming lan-guages, it is worth considering whether or not one of these relations can beomitted.The language omittedMyTypeand matching, but did nothave the expressiveness of.In particular, reusable binary methodsare hard to write safely.OnceMyTypeis included in the language, matching350 18 Simplifying: Dropping Subtyping for Matchingseems forced on the programmer.But what about dropping subtyping fromthe language?At first that seems to be a rather extreme position  after all subtyping isone of the key features of object-oriented languages! However, in practice itis usually not necessary for objects of one type to be able to masquerade asanother.Instead what is important is to be able to predict which methods(and signatures) are supported by objects.This is exactly what matchingguarantees.IfT Uthe objects of typeTsupport all of the same methodsasU [ Pobierz caÅ‚ość w formacie PDF ]