| < Free Open Study > |
|
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 enough—to 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. C→C. 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 function—or 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 type—it is a type variable. This is not just a silly restriction of the typing rules that we have defined—e.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:X→Nat,inc:X→X}, 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.C→C 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.C→C, 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 achieved—and how to achieve it—in 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 > |
|