32.5 Sending Messages to Objects

---

32.5 Sending Messages to Objects

We can now repair the broken version of sendinc from §32.3 by abstracting over sub-interfaces of CounterM rather than sub-types of Counter.

   sendinc =     λM<:CounterM. λc:Object M.       let {X, b} = c in         {*X,          {state = b.methods.inc(b.state),           methods = b.methods}}          as Object M; ▸ sendinc : "M<:CounterM. Object M → Object M 

Intuitively, the type of sendinc can be read "give me an object interface refining the interface of counters, then give me an object with that interface, and I'll return you another object with the same interface."

32.5.1 Exercise [⋆]

Why is this sendinc well typed whereas the previous one was not?

To invoke the methods of counter and reset counter objects, we instantiate the polymorphic method invocation functions with the appropriate interface signature, CounterM or ResetCounterM (assuming sendget and sendreset have been defined analogously).

   sendget [CounterM] (sendinc [CounterM] c); ▸ 6 : Nat   sendget [ResetCounterM]               (sendreset [ResetCounterM]                  (sendinc [ResetCounterM] rc)); ▸ 0 : Nat 

32.5.2 Exercise [Recommended, ⋆⋆]

Define sendget and sendreset.

---