A new definition of subtyping for object types

Because the meaning of MyType depends on its context, our new definition of subtyping will have to consider the different meanings of MyType in the type expressions being compared.

We say that a type ${\it {T}}$ is monotonic in type identifier ${\it {S}}$ iff ${\it {S {\rm \ <: \ }S'}}$ implies that ${\it {T {\rm \ <: \ }T[S'/S]}}$ for all ${\it {S'}}$ not occurring in ${\it {T}}$. For example, by our subtyping rules, the function type ${\it {{\it Func(S):\ U}}}$ is monotonic in ${\it {U}}$, but fails to be monotonic in ${\it {S}}$.

A correct definition of subtyping for object types is:

${\it {ObjectType\{m_j:T'_j\}_{1 \le j \le m} {\rm \ <: \ } ObjectType\{m_i:T_i\}_{1 \le i \le n}}}$ if the two types are equivalent or

1.

$n \le m$ and for each $i \le n$, ${\it {T'_i {\rm \ <: \ }T_i}}$, and

2.

each method type ${\it {T_{j}}}$ in ${\it {T}}$ is monotonic in MyType.

It follows from this definition that ${\it {ObjectType\{m_i:T_i\}_{1 \le i \le n}}}$has no proper subtypes if any of the ${\it {m_i}}$ has a parameter of type MyType.

Notice that the only difference between matching and subtyping is the addition of the second clause in the definition of subtyping. Thus if two object types are subtypes, they match, but not vice-versa. However, if all of the method types are monotonic in MyType, then the two types match iff they are subtypes.

${\it {DoubleNodeType}}$ is not a subtype of ${\it {NodeType}}$, because ${\it {attachRight}}$ has a parameter of type MyType. However, ${\it {DoubleNodeType {\rm \, <\!\!\!\char93 \, }NodeType}}$. In contrast, there is no difficulty with subtyping in classes containing methods like the ${\it {ShallowClone}}$ and ${\it {DeepClone}}$ methods discussed earlier, since MyType only occurs as the result type.

This new definition of subtypes for object types is based on the definition of subtyping for recursive types in [AC93], as type expressions with MyType can be interpreted as being implicitly recursively defined. The rules in that paper would actually allow more types to be subtypes than can be determined with the above rule. The reason is that the general rules given there allow arbitrary ``unfolding'' of recursively defined types. We do not allow that here because of complications that would arise in typing expressions. It is possible to strengthen the above definition by using the assumption ${\it {{\rm{\it MyType}}{\rm \, <\!\!\!\char93 \, }ObjectType\{m_i:T_i\}_{1 \le i \le n}}}$ to prove ${\it {T'_i {\rm \ <: \ }T_i}}$ in the first part of the definition.