Matching is necessary in type checking classes

Our assumption that ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {CType}}}$ that was used in type checking the class ${\it {C}}$ is relatively weak. More method bodies would type check if we assumed that MyType = ${\it {CType}}$, but we now show that they would not necessarily remain type correct when inherited.

Figure 12 presents an example of a class/subclass pair in which a method (in this case ${\it {useEq}}$) of a class type checks fine under the assumption that MyType is exactly the type generated by the class (in this case ${\it {TestType}}$), but when inherited causes a run-time error due to a typing problem.

The subclass ${\it {Subtest}}$simply adds a new instance variable and method, and redefines the method, ${\it {eq}}$ (without changing the typing). If ${\it {s}}$ is an object generated by class ${\it {Subtest}}$ and ${\it {p}}$ is an element generated by ${\it {Test}}$ (and hence having type ${\it {TestType}}$), then the call ${\it {s.useEq(p)}}$ will cause a run-time error while within the body of the call of ${\it {s.eq(p)}}$ made from the body of ${\it {useEq}}$. The problem is that the receiver, ${\it {s}}$, is of type ${\it {SubTestType}}$,while the argument is of type ${\it {TestType}}$. Hence, when the version of ${\it {eq}}$ from ${\it {SubTest}}$ is called, it will send the message ${\it { getOtherval}}$ to the parameter, ${\it {p}}$, which does not have a corresponding method to handle the call, causing a run-time error.

Notice that the problem arises in the method ${\it {useEq}}$ which was not changed in ${\it {SubTest}}$.According to our type-checking rules, the type of ${\it {s.useEq}}$ should be Func(SubTestType): Bool (obtained from ${\it { ({\it Func({\rm{\it MyType}}):\ Bool})[SubTestType/{\rm{\it MyType}}]}}$). As a result, the application to a parameter of type ${\it {TestType}}$ is clearly an error.

How would the weaker type-checking assumption adopted in this section keep us from this error? If we type check the methods of ${\it {Test}}$ under the assumption that ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {TestType}}}$, then the body of the method ${\it {useEq}}$will not type check. The problem is that the message send ${\it { eq(pt)}}$ in the body of ${\it {useEq}}$ requires a parameter of type MyType, while ${\it {pt}}$ has type ${\it {TestType}}$. Because we only know that ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {TestType}}}$, we cannot deduce that ${\it {pt}}$ also has type MyType. Thus type checking the method body of ${\it {useEq}}$ results in a type error, keeping us out of the trouble illustrated above.

This subtleness of type checking may make the reader nervous about uses of MyType, but the arguments presented earlier in this section should be convincing for its safety. Moreover, formal proofs of the soundness of the type-checking rules exist, and can be found in [Bru94] and [BSvG95], for example.

  

Figure 12: Node class with MyType.

The appendix includes an example of a method that type checks under the strong assumption that MyType = ${\it {CType}}$, but that fails under the weaker assumption that ${\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }{\rm{\it {CType}}}$. As a result, ignoring the fact that the meaning of MyType changes in subclasses can result in broken code. Type-checking under the matching assumption guarantees that no type errors result during execution.