, our extension of 
taken from 
,
where 
is the recursion abstractor
and 
a type variable.
The dependence of 
on 
is made explicit
by writing 
.
We will use the type expressions 
to
type object specifications of the form
as indicated by the type assignment rule below.
Object specifications may be regarded as class descriptions
in C++ or Eiffel.
if we can prove that
assuming that 
.
An object specification 
is a function
with the type of the actual object as its domain and (naturally)
also as its range.
For convenience we will write an object specification
as 
, where F denotes the object record,
and the type of an object specification as 
,
where 
denotes the (abstract) type of the record F.
To obtain from an object specification 
the object that it specifies,
we need to find some type 
that types the record
specification F as being of type 
precisely
when we assign the expression self in F
the type 
.
Technically, this means that the object of type 
is a fixed point of the object specification
which is of type 
.
We write this as 
,
which says that the object corresponding to the object
specification is of type 
.
See slide 9-recursion.
as 
.
Notice that unrolling is valid, precisely because of
the fixed point property.
Namely, the object type 
is equal to 
,
due to the type assignment rule, and we have that
.
See slide 9-ex-recursive.
Unrolling allows us to reason on the level of types
and to determine the subtyping relation between recursive
subtypes.
Consider, for example, the type declarations T and 
above.
Based on the refinement rules for object records, functions
and recursive types, we may establish that 
,
but 
.
To see that 
, it suffices to substitute T
for 
in F, where 
.
Since 
we immediately see that 
only extends T with the field 
,
hence 
.
A similar line of reasoning is involved to determine that
, only we need to unroll 
as well.
We must then establish that 
, which follows
from an application of the refinement rule.
To show that 
, let
and 
.
Then, by unrolling,
.
Now, suppose that 
, then 
and consequently 
must refine 
.
But from the latter requirement it follows that 
and that 
(by the contravariance rule for function
subtyping).
However, this leads to a contradiction since T is clearly
not equal to 
because 
contains a field
that does not occur in T.
Although analyses of this kind are to some extent
satisfactory in themselves, the reader may wonder
where this all leads to.
In the following we will apply these techniques
to show the necessity of dynamic binding
and to illustrate that inheritance may easily violate
the subtyping requirements.
we may characterize this
more precisely, by regarding a derived object specification
C as the result of applying the modifier M
to the object specification P.
We employ
the notation 
to characterize derivation by inheritance,
and we assume the modifier M corresponding with
to extend the record
associated with P in the usual sense.
See slide 9-self-inheritance.
, that is
.
Now when we assume that the object specification is of type
(and hence 
of type 
),
and that C is of type 
(and hence 
of type
), then we must require that 
to obtain
a properly typed derivation.
We write 
whenever 
.
A first question that arises when we characterize inheritance
as incremental modification is how we obtain the meaning
of the composition of two object specifications.
is 
then we may simply characterize 
as being
of type 
.
However, when we delay the typing of the P
component (by first composing the record specifications
before abstracting from self)
then we may obtain 
as the type of 
.
By employing the refinement rule and unrolling we can
show that 
.
Hence, delayed typing clearly provides more information
and must be considered as the best choice.
Note, however, that both 
and 
hold.
See slide 9-self-dynamic.
A second, important question that emerges
with respect to inheritance is how
self-reference affects the subtyping relation between
object specifications related by inheritance.
Consider the object specifications P and C given
in slide 9-self-contravariance.
In the (derived) specification C, the method eq
is redefined to include an equality test for the b
component.
However, when we determine the object types corresponding
to the specifications P and C
we observe that 
.
and 
, we have
that 
which is (by unrolling) equal to 
.
Now suppose that 
, then we have that
is a subtype of
which is true when 
and hence (by contravariance) when 
.
Clearly, this is impossible. Hence 
.
We have a problem here,
since the fact that 
means that the type checker
will not be able to accept the derivation of C from P,
although C is clearly dependent on P.
The solution to our problem
lies in making the type dependency involved in deriving
C from P explicit.
Notice, in this respect, that in the example above we
have omitted the type of the abstraction variable
in the definition of eq,
which would have to be written as 
(and in a similar way for C ) to do it properly.
.
Let 
stand for 
as before.
We may regard 
as a type function, in the sense
that for some type 
the expression 
results in a type.
To determine the type of an object specification
we must find a type 
that satisfies both
and 
.
,
which is typed as 
.
The constraint that 
, which is called
an F-bounded constraint, requires
that the subtype substituted for 
is
a (structural) refinement of the record type 
.
As before, we have that 
with 
,
which differs from our previous definition only
by making the type dependency in P explicit.
See slide 9-dependency.
Now, when applying this extended notion of object
specification to the characterization of inheritance,
we may relax our requirement that 
must be a subtype
of 
into the requirement that 
for any 
, where F is the record specification
of P and G the record specification of C.
and 
as in slide 9-self-constraint,
we have that 
for every value for 
.
However, when we find types 
and 
such that 
and 
we (still) have that 
.
Conclusion, inheritance allows more than subtyping.
In other words, our type checker may guard
the structural application of inheritance, yet will
not guarantee that the resulting object types
behaviorally satisfy the subtype relation.
Eiffel
class C inherit P redefine eq
feature
b : Boolean is true;
eq( other : like Current ) : Boolean is
begin
Result := (other.i = Current.i) and
(other.b = Current.b)
end
end C
p,v:P, c:C v:=c; v.eq(p);error p has no b
class C : public P {
int b;
public:
C() { ... }
bool eq(C& other) { return other.i == i && other.b == b; }
bool eq(P& other) { return other.i == i; }
};
|
Hush Online Technology
hush@cs.vu.nl
12/29/99 |
|
|