18.4 Subtyping

---

18.4 Subtyping

One of the reasons for the popularity of object-oriented programming styles is that they permit objects of many shapes to be manipulated by the same client code. For example, suppose that, in addition to the Counter objects defined above, we also create some objects with an additional method that allows them to be reset to their initial state (say, 1) at any time.

   ResetCounter = {get:Unit→Nat, inc:Unit→Unit, reset:Unit→Unit};   newResetCounter =     λ_:Unit. let x = ref 1 in                 {get   = λ_:Unit. !x,                  inc   = λ_:Unit. x:=succ(!x),                  reset = λ_:Unit. x:=1}; ▸ newResetCounter : Unit → ResetCounter 

Since ResetCounter has all the fields of Counter (plus one more), the record subtyping rule tells us that ResetCounter <: Counter. This means that client functions like inc3 that take counters as arguments can also safely be used with reset counters:

   rc = newResetCounter unit; ▸ rc : ResetCounter   (inc3 rc; rc.reset unit; inc3 rc; rc.get unit); ▸ 4 : Nat 

---