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 under the assumption that self: MyType and
. This will ensure that inherited methods are still
type safe since the meaning of MyType in any subclass of
will
match
. (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, , of type
with a method,
, whose type
involves
MyType. What is the type of
? The obvious answer is
that its type is
, modified so that all free occurrences of
MyType are replaced by
, 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
represent the type
in which all free
occurrences of MyType have been
replaced by the type
. Then
has type
if
has type
and
has type
. For example,
if function
is given type
then
=
.
Suppose
, the type of method
in
is
, and that the type of
in
is
. By the definition of matching we know that
. If
is an object of type
then the type of
is
. But when we determined that
, we made no assumptions about MyType. As a result, it is possible to
show that
, 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,
also has type
by subsumption.
Let us examine how we would type check the node example in
Figure 10. The type correctness of
and
are obvious. The methods
and
are type correct because
has type MyType.
Only the typing of the body of
requires more careful
analysis. As stated above, we assume self has type MyType and
. Because
, we know
that self has a
method whose type is a subtype of
. We conclude that the type of
is a
subtype of
=
since the
substitution of MyType for itself has no effect. By the subsumption
rule of section 2.1,
can be treated
as if it has the type
. Because
has type MyType, the expression
is well typed.
We now type check the subclass in Figure 11.
The assumptions we used in type checking
(i.e.,
that self has type MyType, and
) remain true in
the subclass. (In fact, in the subclass we are allowed to assume
, which implies
by
transitivity since
.) Hence we have
no need to go back and re-examine any inherited methods for type
correctness. The type correctness of methods
and
follow easily from the fact that
has type MyType.
Thus we need only concern ourselves with the redefined method .
In order to attach
to the
right of self, first
is assigned to the receiver's
field via the call to
. Then the parameter,
, is asked to set self to its
field via the message
send of
to
with parameter self. The
first message send to self is type correct for the same reasons as
in
. The type correctness of the second message send
follows by the same reasoning since
and self both have type
MyType. Note that the method would not type check if the actual
parameter to
were of type
rather
than MyType.
In summary, if