32.8 Adding Instance Variables

---

32.8 Adding Instance Variables

Using the features from the previous section, we can write a counterClass that is polymorphic in the type of the internal state.

   CounterR = {#x:Nat};   counterClass =      λR<:CounterR.         {get = λs:R. s.x,          inc = λs:R. s←x=succ(s.x)}         as CounterM R; ▸ counterClass : "R<:CounterR. CounterM R 

To build an object from the new counterClass, we simply supply CounterR as the representation type:

   c = {*CounterR,        {state = {#x=0},         methods = counterClass [CounterR]}}       as Object CounterM; ▸ c : Counter 

Note that objects built from the new class have the same type Counter = Object CounterM as the ones above: the changes to the treatment of instance variables are entirely internal to the classes. The method invocation functions above can also be used with objects instantiated from the new classes.

We can write resetCounterClass in the same style.

   resetCounterClass =      λR<:CounterR.        let super = counterClass [R] in          {get = super.get,           inc = super.inc,           reset = λs:R. s←x=0}          as ResetCounterM R; ▸ resetCounterClass : "R<:CounterR. ResetCounterM R 

Finally, we can write a backupCounterClass, this time abstracting over a subtype of BackupCounterR (which was the point of the whole exercise).

   BackupCounterM = λR. {get:R→Nat,inc:R→R,reset:R→R,backup:R→R};   BackupCounterR = {#x:Nat,#old:Nat};   backupCounterClass =      λR<:BackupCounterR.      let super = resetCounterClass [R] in       {get = super.get,        inc = super.inc,        reset = λs:R. s←x=s.old,        backup = λs:R. s←old=s.x}       as BackupCounterM R; ▸ backupCounterClass : "R<:BackupCounterR. BackupCounterM R 

---