Chapter 27: Case Study: Imperative Objects, Redux

---

Overview

Chapter 18 developed a collection of idioms in a simply typed calculus with records, references, and subtyping, modeling the core of an imperative object-oriented programming style. At the end of that chapter (in §18.12) we spent some effort in improving the run-time efficiency of our objects by moving the work of building an object's method table from method invocation time to object creation time. In this chapter, we use bounded quantification to further improve the efficiency of the model.

The key idea in §18.12 was to pass a reference to the "self method table" to a class when we call it. The class uses this reference in defining its own methods, and we later back-patch the reference to point to the completed method table returned by the class. For example, if SetCounter and SetCounterRep are the public interface and the internal representation type of a class of counter objects with get, set, and inc methods,

   SetCounter = {get:Unit→Nat, set:Nat→Unit, inc:Unit→Unit};   CounterRep = {x: Ref Nat}; 

then we can implement a class of set counters like this:

   setCounterClass =     λr:CounterRep. λself: Source SetCounter.       {get = λ_:Unit. !(r.x),        set = λi:Nat. r.x:=i,        inc = λ_:Unit. (!self).set                        (succ ((!self).get unit))}; ▸ setCounterClass : CounterRep → (Source SetCounter) → SetCounter 

We use the type Source SetCounter instead of Ref SetCounter for the self parameter because, when we define a subclass of setCounterClass, this new class's self will have a different type. For example, if InstrCounter and InstrCounterRep are the interface and representation types for a class of instrumented counter objects,^[1]

   InstrCounter = {get:Unit→Nat, set:Nat→Unit,                   inc:Unit→Unit, accesses:Unit→Nat};   InstrCounterRep = {x: Ref Nat, a: Ref Nat}; 

then we can define the class itself as follows:

   instrCounterClass =     λr:InstrCounterRep. λself: Source InstrCounter.     let super = setCounterClass r self in     {get = super.get,      set = λi:Nat. (r.a:=succ(!(r.a)); super.set i),      inc = super.inc,      accesses = λ_:Unit.                    !(r.a)}; ▸ instrCounterClass : InstrCounterRep →                       (Source InstrCounter) → InstrCounter 

The type of the self parameter here is Source InstrCounter, and we need to be able coerce from Source InstrCounter to Source SetCounter in order to pass this self as the self argument of setCounterClass when we build super. The covariant Source constructor permits this coercion, whereas the invariant Ref constructor would not.

However, as we observed at the end of §18.12, the efficiency of this model of classes is still not optimal. Since the same method table is associated with every object instantiated from a given class, we ought to be able to build this table just once, at class creation time, and re-use it every time an object is created. This would more accurately reflect the implementation conventions of real-world object-oriented languages, where an object does not carry any methods but just a pointer to a data structure representing its class, which is where the methods are actually stored.^[2]

Another way of saying the same thing is to observe that the order of parameters to the classes above (first instance variables, then self) is backwards: the self parameter is needed to build the class table, but the record of instance variables r is not used until a method is actually called. If self were the first argument, then we could compute the method table before being passed the r argument; we could partially apply the class, once, to its self argument, perform this computation once and for all, and make multiple copies of the resulting method table by applying it to multiple records of instance variables. Concretely, we would like to rewrite the setCounterClass like this:

   setCounterClass =     λself: Source (CounterRep→SetCounter).     λr:CounterRep.       {get = λ_:Unit. !(r.x),        set = λi:Nat. r.x:=i,        inc = λ_:Unit. (!self r).set                             (succ ((!self r).get unit))}; ▸ setCounterClass : (Source (CounterRep→SetCounter)) →                     CounterRep → SetCounter 

There are three significant differences between this version and the previous one. First, the new version takes self before r. Second, the type of self has changed from SetCounter to CounterRep→SetCounter. This change is forced by the first, since the type of self must be the same as the type of the method table returned by the class. And third, every use of !self in the body of the class becomes (!self r). This change is forced by the second one.

The instantiation function for our new counters is defined like this:

   newSetCounter =     let m = ref (λr:CounterRep. error as SetCounter) in     let m' = setCounterClass m in     (m := m';      λ_:Unit. let r = {x=ref 1} in m' r); ▸ newSetCounter : Unit → SetCounter 

Notice that the first three lines of this definition are evaluated just once, when newSetCounter is defined. Evaluation stops at the trivial abstraction on the last line, which can then be applied over and over to create objects; each time, it will allocate storage for a fresh record r of instance variables and instantiate the method table m′ with r to yield a fresh object.

Unfortunately, by rearranging setCounterClass in this way, we have introduced a contravariant occurrence of the state type CounterRep, and this comes back to haunt us when we try to define a subclass of setCounterClass.

   instrCounterClass =     λself: Source (InstrCounterRep→InstrCounter).     let super = setCounterClass self in     λr:InstrCounterRep.     {get = (super r).get,      set = λi:Nat. (r.a:=succ(!(r.a)); (super r).set i),      inc = (super r).inc,      accesses =  λ_:Unit. !(r.a)}; ▸ Error: parameter type mismatch 

The mismatch arises in the definition of super, where we instantiate the superclass setCounterClass with the same self that was passed to the subclass. Unfortunately, the present self is (a reference to) a function of type InstrCounterRep→InstrCounter, which is not a subtype of CounterRep→SetCounter because the left-hand sides of the arrows are the wrong way around.

We can address this difficulty by rewriting setCounterClass once more, this time using bounded quantification.

   setCounterClass =     λR<:CounterRep.     λself: Source(R→SetCounter).       λr: R.          {get = λ_:Unit. !(r.x),           set = λi:Nat.  r.x:=i,           inc = λ_:Unit. (!self r).set (succ((!self r).get unit))}; ▸ setCounterClass : "R<:CounterRep.                       (Source (R→SetCounter)) → R → SetCounter 

What this change accomplishes is that it makes setCounterClass a bit less demanding about the self parameter it is passed. Anthropomorphizing a little, we could characterize the previous version of setCounterClass as saying to its environment, "Please pass me a self parameter that accepts a CounterRep as a parameter, and I will use it to build a method table that also expects a CounterRep parameter." The new version, says, instead, "Please tell me the representation type R for an object that we are building; this type must have at least an x field, because I need to use it. Then give me a (reference to a) self that accepts R as a parameter and returns a method table with at least the methods of the SetCounter interface, and I will build and return another of the same kind."

We can see the effect of this change most clearly when we define the subclass instrCounterClass.

   instrCounterClass =     λR<:InstrCounterRep.     λself: Source(R→InstrCounter).       λr: R.         let super = setCounterClass [R] self in            {get = (super r).get,             set = λi:Nat. (r.a:=succ(!(r.a)); (super r).set i),             inc = (super r).inc,             accesses = λ_:Unit. !(r.a)}; ▸ instrCounterClass : "R<:InstrCounterRep.                         (Source (R→InstrCounter)) →                         R → InstrCounter 

The reason this definition works where the previous one failed lies in the different uses of subsumption in the expression bound to super, where we promote the type of self to make it acceptable to the superclass. Previously, we were trying to show

                  Source(InstrCounterRep→InstrCounter)             <:   Source(CounterRep→SetCounter), 

which was false. Now all we have to show is

          Source(R→InstrCounter) <: Source(R→SetCounter), 

which is true.

The object creation functions for our new encoding of classes are very similar to the old ones. For example, here is the creator for the instrumented counter subclass.

   newInstrCounter =     let m = ref (λr:InstrCounterRep. error as InstrCounter) in     let m' = instrCounterClass [InstrCounterRep] m in     (m := m';      λ_:Unit. let r = {x=ref 1, a=ref 0} in m' r); ▸ newInstrCounter : Unit → InstrCounter 

The only difference is that we need to instantiate instrCounterClass with the actual type InstrCounterRep of the instance variable record. As before, the first three lines are executed just once, at the point when the binding of newInstrCounter is made.

Finally, here are a few tests to demonstrate that our counters are behaving the way we expect.

   ic = newInstrCounter unit;   ic.inc unit;   ic.get unit; ▸ 2 : Nat   ic.accesses unit; ▸ 1 : Nat 

^[1]The examples in this chapter are terms of F_<: with records (Figure 15-3), and references (13-1). The associated OCaml implementation is fullfsubref.

^[2]In fact, real-world object oriented-languages go one step further. Rather than calculating and storing a complete method table, each class stores just the methods that it adds or overrides with respect to its superclass. So the method table in our sense never gets built at all-at method invocation time, we simply walk up the class hierarchy, starting from the actual class of the receiver object, until we find a definition of the method we want. This kind of run-time search poses tricky problems for a static type analysis, and we will not deal with it here.

---