32.2 Subtyping

 < Free Open Study > 



32.2 Subtyping

A pleasant feature of this existential encoding of objects is that the subtype inclusions that we expect between object types follow directly from the subtyping rules for existentials and records. To check this, recall (from 26-3) the subtyping rule for existential types.[2]

This rule tells us immediately that if we define an object type with more methods than Counter, e.g.,

   ResetCounter =     {$X, {state:X, methods:{get: XNat, inc:XX, reset:XX}}}; 

then it will be a subtype of Counter, i.e., ResetCounter <: Counter. This means that, if we define a reset counter object,

   rc = {*CounterR,         {state = {x=0},          methods = {get = λr:CounterR. r.x,                     inc = λr:CounterR. {x=succ(r.x)},                     reset = λr:CounterR. {x=0}}}} as ResetCounter;  rc : ResetCounter 

we can use subsumption to pass this object to functions defined on Counter, such sendget, sendinc, and addthree:

   rc3 = addthree rc;  rc3 : Counter 

Notice, though, that we lose type information when we do this: the type of rc3 here is just Counter, not ResetCounter.

[2]We use only the kernel variant of the rule here; the power of the full version is not needed. In fact, we do not need bounded existentials at all in this chapterthe bounds of all our existentials are Top.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net