32.7 Polymorphic Update

< Free Open Study >

To add instance variables to classes, we need to add one new mechanism—a primitive for in-place polymorphic update of record fields and an associated refinement to record types. The need for these features arises from the fact that allowing variation in instance variables between classes means making superclasses polymorphic in the instance variables of their subclasses. Let us look at how this happens.

Suppose that we want to define a subclass of resetCounterClass, adding a backup method that saves the current value of the counter and changing the behavior of reset to revert to this saved value instead of to a constant initial value. To hold this saved value, we will need to extend our state type from {x:Nat} to {x:Nat, old:Nat}. This difference in representations immediately creates a technical difficulty. Our ability to reuse the inc method from resetCounterClass when defining backupCounterClass depends on this method behaving the same in both classes. However, if the sets of instance variables are different, then it does not behave quite the same: the inc of a ResetCounter expects a state of type {x:Nat} and returns a new state of the same type, while the inc of BackupCounter expects and produces states of type {x:Nat,old:Nat}.

To resolve this difficulty, it suffices to observe that the inc method does not really need to know that the state type is {x:Nat} or {x:Nat,old:Nat}, but only that the state contains an instance variable x. In other words, we can unify these two methods by giving them both type "S<:{x:Nat}.S→S.

Now the same difficulty arises with states as with whole objects in §32.3: the type "S<:{x:Nat}.S→S in our present language is inhabited only by the identity function. Again, to address this difficulty, we need some mechanism that permits a more precise form of bounded quantification; here, the most direct mechanism is to add a primitive for polymorphic update of record fields.^[3] If r is a record with a field x of type T and t is a term of type T, then we write r←x=t to mean "a record that is just like r except that its x field has the value t." Note that this is a purely functional form of update operation—it does not change r, but instead makes a clone with a different x field.

Using this record update primitive, a function that captures the intended behavior of the inc method body can be written roughly as follows:

   f = λX<:{a:Nat}. λr:X. r←a = succ(r.a);

However, we have to be a little careful. A naive typing rule for the update operator would be:

But this rule is unsound. For example, suppose we have:

   s = {x={a=5,b=6},y=true};

Since s : {x:{a:Nat,b:Nat},y:Bool}, and {x:{a:Nat,b:Nat},y:Bool} <: {x:{a:Nat}}, the above rule would allow us to derive

   s←x={a=8} : {x:{a:Nat,b:Nat},y:Bool},

which would be wrong, since s←x={a=8} reduces to {x={a=8},y=true}.

This problem was caused by the use of depth subtyping on the field x to derive {x:{a:Nat,b:Nat},y:Bool} <: {x:{a:Nat}}. Depth subtyping should not be allowed in fields that might be updated. We can achieve this by the simple expedient of annotating such fields with a special mark, written #.

The rules for these "updatable records" and for the update operation itself are given in Figure 32-1. We refine the syntax of record types so that every field is annotated with a variance tag that indicates whether depth subtyping is allowed—# to forbid subtyping in this field and the empty string to permit it (choosing the empty string here means that unmarked records will behave as they always have). The depth subtyping rule S-RCDDEPTH is refined to allow subtyping only in unmarked fields. Finally, we add a subtyping rule S-RCDVARIANCE that permits marks on fields to be changed from # to the empty string—in other words, to "forget" that a given field is updatable. The typing rule for the update primitive demands that the field being replaced is marked #. The E-UPDATE rule implements the update operation.

Figure 32-1: Polymorphic Update

The function f above is now written like this,

   f = λX<:{#a:Nat}. λr:X. r←a = succ(r.a); ▸ f : "X<:{#a:Nat}. X → X

and used like this:

   r = {#a=0, b=true};   f [{#a:Nat,b:Bool}] r; ▸ {#a=1, b=true} : {#a:Nat, b:Bool}

The soundness of the update operation rests on the following observation about the refined subtype relation:

32.7.1 Fact

If ⊢ R, <: {#⌉:T₁}, then R = {...# ⌉ :R₁ ...} with ⊢ R₁ <: T₁ and ⊢ T₁ <: R₁.

32.7.2 Exercise [Recommended, ⋆⋆⋆]

Does the minimal typing property hold for this calculus? If so, prove it. If not, find a way to repair it.

^[3]As before, there are actually several ways of achieving similar effects—by introducing different primitives (some are listed in §32.10), or by using polymorphism, as in Pierce and Turner (1994)—a notationally heavier but theoretically more elementary alternative. The one used here is chosen for its simplicity, and because it fits naturally with the examples that follow.

< Free Open Study >