Type checking classes using matching

As discussed earlier, when defining subclasses we will insist that the types of redefined methods be subtypes of their types in the superclass. As a result the types of objects generated by subclasses will always match the type generated by the superclass. Thus we can type check methods of a class ${\it {C}}$ under the assumption that self: MyType and ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {CType}}}$. This will ensure that inherited methods are still type safe since the meaning of MyType in any subclass of ${\it {C}}$ will match ${\it {CType}}$. (A proof of this can be found in [Bru94] or [BSvG95].)

We have one more puzzle to solve before we can type check classes. Suppose that there is an object, ${\it { o}}$, of type ${\it {S}}$ with a method, ${\it {m}}$, whose type ${\it {T}}$ involves MyType. What is the type of ${\it {o.m}}$? The obvious answer is that its type is ${\it {T}}$, modified so that all free occurrences of MyType are replaced by ${\it {S}}$, the type of the receiver. After all, MyType was designed to represent the type of the receiver.

We can make this more precise as follows. Let the notation ${\it {T[S/{\rm{\it MyType}}]}}$ represent the type ${\it {T}}$ in which all free occurrences of MyType have been replaced by the type ${\it {S}}$. Then ${\it {o.m}}$ has type ${\it {T[S/{\rm{\it MyType}}]}}$ if ${\it {m}}$ has type ${\it {T}}$ and ${\it { o}}$ has type ${\it {S}}$. For example, if function ${\it {equal}}$ is given type ${\it {{\it Func({\rm{\it MyType}}):\ Bool}}}$ then ${\it {({\it Func({\rm{\it MyType}}):\ Bool})[Ctype/{\rm{\it MyType}}]}}$ = ${\it {{\it Func(CType):\ Bool}}}$.

Suppose ${\it {SCType {\rm \, <\!\!\!\char93 \, } CType}}$, the type of method ${\it {m}}$ in ${\it {CType}}$ is ${\it {T}}$, and that the type of ${\it {m}}$ in ${\it {SCType}}$ is ${\it {ST}}$. By the definition of matching we know that ${\it {ST {\rm \ <: \ } T}}$. If ${\it { o}}$ is an object of type ${\it {SCType}}$ then the type of ${\it {o.m}}$ is ${\it {ST[SCType/{\rm{\it MyType}}]}}$. But when we determined that ${\it {ST {\rm \ <: \ } T}}$, we made no assumptions about MyType. As a result, it is possible to show that ${\it {ST[SCType/{\rm{\it MyType}}] {\rm \ <: \ }T[SCType/{\rm{\it MyType}}]}}$, because uniform substitution of a type expression for a type variable does not affect subtyping. (See the subtyping rules in [Bru94], for example.) In particular, then, ${\it {o.m}}$ also has type ${\it { T[SCType/{\rm{\it MyType}}]}}$ by subsumption.

Let us examine how we would type check the node example in Figure 10. The type correctness of ${\it {getValue}}$ and ${\it {setValue}}$ are obvious. The methods ${\it {getNext}}$ and ${\it {setNext}}$ are type correct because ${\it {next}}$ has type MyType. Only the typing of the body of ${\it {setNext}}$ requires more careful analysis. As stated above, we assume self has type MyType and ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {NodeType}}}$. Because ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {NodeType}}}$, we know that self has a ${\it {setNext}}$ method whose type is a subtype of ${\it {Proc({\rm{\it MyType}})}}$. We conclude that the type of ${\it {self.setNext}}$ is a subtype of ${\it {Proc({\rm{\it MyType}})[{\rm{\it MyType}}/{\rm{\it MyType}}]}}$ = ${\it {Proc({\rm{\it MyType}}),}}$ since the substitution of MyType for itself has no effect. By the subsumption rule of section 2.1, ${\it {self.setNext}}$ can be treated as if it has the type ${\it {Proc({\rm{\it MyType}})}}$. Because ${\it {newNext}}$has type MyType, the expression ${\it {{\rm{\it self}}.setNext(newNext)}}$ is well typed.

We now type check the subclass ${\it {DoubleNode}}$ in Figure 11. The assumptions we used in type checking ${\it {Node}}$ (i.e., that self has type MyType, and ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {NodeType}}}$) remain true in the subclass. (In fact, in the subclass we are allowed to assume ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {DoubleNodeType}}}$, which implies ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {NodeType}}}$ by transitivity since ${\it {DoubleNodeType {\rm \, <\!\!\!\char93 \, }NodeType}}$.) Hence we have no need to go back and re-examine any inherited methods for type correctness. The type correctness of methods ${\it {getPrev}}$ and ${\it {setPrev}}$ follow easily from the fact that ${\it {prev}}$ has type MyType.

Thus we need only concern ourselves with the redefined method ${\it {attachRight}}$. In order to attach ${\it {newNext}}$ to the right of self, first ${\it {newNext}}$ is assigned to the receiver's ${\it {next}}$ field via the call to ${\it {setNext}}$. Then the parameter, ${\it {newNext}}$, is asked to set self to its ${\it {prev}}$ field via the message send of ${\it {setPrev}}$ to ${\it {newNext}}$ with parameter self. The first message send to self is type correct for the same reasons as in ${\it {Node}}$. The type correctness of the second message send follows by the same reasoning since ${\it {newNext}}$ and self both have type MyType. Note that the method would not type check if the actual parameter to ${\it {newNext.setPrev}}$ were of type ${\it {DoubleNodeType}}$ rather than MyType.

In summary, if

1.

redefined methods in subclasses are constrained to have types which are subtypes of those given in the superclass, and

2.

we type check methods of a class under the assumptions that self: MyType and MyType matches the type of object generated by the class,

then we will be guaranteed that the inherited methods remain type safe in subclasses.