18.7 Adding Instance Variables

---

18.7 Adding Instance Variables

It happens that our counter and reset counter objects use exactly the same internal representation. However, in general a subclass may need to extend not only the methods but also the instance variables of the superclass from which it is derived. For example, suppose we want to define a class of "backup counters" whose reset method resets their state to whatever value it has when we last called the method backup, instead of resetting it to a constant value:

   BackupCounter = {get:Unit→Nat, inc:Unit→Unit,                    reset:Unit→Unit, backup: Unit→Unit}; 

To implement backup counters, we need an extra instance variable to store the backed-up value of the state.

   BackupCounterRep = {x: Ref Nat, b: Ref Nat}; 

Just as we derived resetCounterClass from counterClass by copying the get and inc methods and adding reset, we derive backupCounterClass from resetCounterClass by copying get and inc and providing reset and backup.

   backupCounterClass =     λr:BackupCounterRep.       let super = resetCounterClass r in          {get    = super.get,           inc    = super.inc,           reset  = λ_:Unit. r.x:=!(r.b),           backup = λ_:Unit. r.b:=!(r.x)}; ▸ backupCounterClass : BackupCounterRep → BackupCounter 

Two things are interesting about this definition. First, although the parent object super includes a method reset, we chose to write a fresh implementation because we wanted a different behavior. The new class overrides the reset method of the superclass. Second, subtyping is used in an essential way here in typing the expression that builds super: resetCounterClass expects an argument of type CounterRep, which is a supertype of the actual type, BackupCounterRep, of the argument r. In other words, we are actually providing the parent object with a larger record of instance variables than its methods require.

18.7.1 Exercise [Recommended, ⋆⋆]

Define a subclass of backupCounterClass with two new methods, reset2 and backup2, controlling a second "backup register." This register should be completely separate from the one added by backupCounterClass: calling reset should restore the counter to its value at the time of the last call to backup (as it does now) and calling reset2 should restore the counter to its value at the time of the last call to backup2. Use the fullref checker to test your class.

---