32.3 Bounded Quantification

 < Free Open Study > 



32.3 Bounded Quantification

Of course, it was precisely this sort of information loss due to subsumption that motivated the introduction of bounded quantification in Chapter 26. However, bounded quantification by itself is not quite enoughto be useful in addressing the problem at hand, it needs to be enriched with some additional mechanism.

To see why, observe that the obvious refinement of the type of sendinc using bounded quantification is "C<:Counter. CC. If we had a sendinc of this type, then we could write addthree as

   addthree = λC<:Counter. λc:C.                sendinc [C] (sendinc [C] (sendinc [C] c));  addthree : "C<:Counter. C  C 

and apply it to rc to obtain a result of type ResetCounter.

   rc3 = addthree [ResetCounter] rc;  rc3 : ResetCounter 

Unfortunately, there is no way to write such a functionor rather, no way to write a function that behaves the way we want and give it this type. We can, of course, write an identity function that belongs to this type,

   wrongsendinc = λC<:Counter. λc:C. c;  wrongsendinc : "C<:Counter. C  C 

but if we try to refine the real implementation of sendinc from above by adding a bounded type abstraction at the front, we get something that fails to typecheck.

   sendinc =      λC<:Counter. λc:C.        let {X,body} = c in          {*X,           {state = body.methods.inc(body.state),            methods = body.methods}}          as C;  Error: existential type expected 

The problem here is in the last line. The annotation as C tells the typechecker "use the existential type C for the package being created here." But C is not an existential typeit is a type variable. This is not just a silly restriction of the typing rules that we have definede.g., a consequence of the fact that the rules do not "know" that every subtype of an existential type is an existential type. On the contrary, it would actually be wrong to give the package

    {*X,     {state = body.methods.inc(body.state),      methods = body.methods}} 

the type C. Observe, for example, that the type

   {$X, {state:X, methods:{get:XNat,inc:XX}, junk:Bool}} 

is a subtype of Counter. But the package above certainly does not have this type: it lacks the field junk. So it is not the case that, for any subtype C of Counter, the body of sendinc above "really" has type C, if only the typing rules could see it. Indeed, it can be shown (e.g., by appealing to a denotational model for F<:see Robinson and Tennent, 1988) that, in pure F<:, types of the form "C<:T.CC contain only identity functions.

Several ways of addressing this shortcoming of F<: have been proposed. One possibility is to move from F<: to and use higher-order bounded quantification to give yet more refined types to functions like sendinc. Another possibility is to keep the type "C<:Counter.CC, but to add features to the language that can be used to build interesting inhabitants of this type. A final possibility is simply to add references to the language. However, we have already gone down that path in Chapter 27; the aim in the present chapter is to experiment with what can be achievedand how to achieve itin a purely functional setting.

The development that follows combines two of these methods to address the problem with quantification over object types that we noticed in the previous section, and a new primitive for polymorphic record update (defined in §32.7) to address a related problem that arises i n the treatment of instance variables (§32.8).



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net