The matching relation between types

  Our type-checking rules for methods need to accommodate the fact that methods can be inherited in subclasses, where the meanings of self and MyType are different from those in the original class. The difficulty, then, is that within a fixed object's type, MyType has a fixed meaning (the type of the object), yet inside a class it will have a more flexible meaning, because methods and instance variables from the class might also be inherited in a subclass. In this section we show how to cope with the changing meaning of self and MyType in classes.

Our goal is to type check methods in a class in such a way that they are guaranteed to be type-safe no matter how they are inherited. We saw in the previous section that we avoid typing problems if we replace the types of methods by subtypes in subclasses. The definition of matching captures exactly this change in method types between object types.

We say that object type ${\it {T'}}$ matches object type ${\it {T}}$, written ${\it {T' {\rm \, <\!\!\!\char93 \, } T}}$, iff for each method ${\it {m_i:\ T_i}}$ of ${\it {T}}$ there is a corresponding method ${\it {m_i:\ T'_i}}$ of ${\it {T'}}$ such that ${\it {T'_i {\rm \ <: \ }T_i}}$. Put slightly differently,

$${\rm{\it {ObjectType\{m_j:T'_j\}}}}_{1 \le j \le m} {\rm \, ... ...ch } i \le n,\ {\rm{\it {T'_i}}} {\rm \ <: \ }{\rm{\it {T_i}}}.$$

It follows that if ${\it {SC}}$ is a subclass of ${\it {C}}$ then ${\it {SCType {\rm \, <\!\!\!\char93 \, } CType}}$. We will see below that matching is weaker than subtyping. The difference between this and our earlier definition of subtyping for objects (which looked identical) is the presence of the keyword MyType.

One important point here: In determining whether two object types match in the above definition, we determine if ${\it {T'_i {\rm \ <: \ }T_i}}$without making any assumption on the meaning of MyType. As a result the two types will certainly be subtypes in any particular context where MyType stands for some fixed type.