32.4 Interface Types

---

32.4 Interface Types

Using type operators, we can express Counter as the combination of two pieces

   Counter = Object CounterM; 

where

   CounterM = λR. {get: R→Nat, inc:R→R}; 

is a type operator of kind *⇒* representing the specific method interface of counter objects and

   Object = λM::*⇒*. {$X, {state:X, methods:M X}}; 

is a type operator of kind (*⇒*)⇒* that captures the common structure of all object types. What we achieve by this reformulation is a separation of the varying part (the method interface), where we want to allow subtyping, from the fixed skeleton of objects (the existential packaging, and the pair of state and methods), where we do not because it gets in the way of the repackaging.

We need bounded quantification over a type operator to achieve this splitting because it allows us to pull out the method interface from an object type, even though the interface mentions the existentially bound state type X, by abstracting the method interface itself on X. The interface thus becomes a "parametric parameter." The iterated character of the parameterization here is reflected both in the kind of Object and in the steps by which the application Object CounterM is simplified: first, CounterM is substituted into the body of Object, yielding

   {$X, {state:X, methods:(λR. {get: R→Nat, inc:R→R}) X}} 

and then X is substituted into the body of CounterM, yielding

   {$X, {state:X, methods:{get:X→Nat,inc:X→X}}}. 

If we split ResetCounter in the same way,

   ResetCounterM = λR. {get: R→Nat, inc:R→R, reset:R→R};   ResetCounter = Object ResetCounterM; 

then we have not only

   ResetCounter <: Counter 

as before but also

   ResetCounterM <: CounterM 

by the rules above for subtyping between type operators. That is, our separation of object types into generic boilerplate plus a specific interface gives us a meaningful sense of interface subtyping that is separate from the subtype relations between complete object types.

Interface subtyping is closely related—both conceptually and technically—to the idea of matching introduced by Bruce et al. (1997) and further studied by Abadi and Cardelli (1995; 1996).

---