cook@hplabsz.HPL.HP.COM (William Cook) (06/27/89)
*** These opinions are my own and must not be ***
*** taken to represent those of my employer. ***
Since Dr. Meyer has referred to my analysis of the Eiffel type system
several times, but it is not yet generally available, it seems
appropriate for me to summarize the paper here. I have been slow to
promote my analysis out of professional courtesy, so the ISE would
have time to prepare a response before the criticisms were publicly
presented. The analysis will be presented at ECOOP'89, and also
republished this fall in "The Computer Journal" of the British
Computing Society.
Ever since I first pointed out the "insecurities" in the Eiffel type
system, many of which have been discovered independently and posted to
this group, Dr. Meyer's response has been that these are not language
flaws but deficiencies in the implementation (the compiler misses some
things). This is imaginable, in that one could attempt to use global
data-flow analysis over complete Eiffel systems to find out whether a
given *potential* violation of the type-system will ever really
happen. With this point of view no type-system is ever incorrect,
because one could always claim that the surrounding system will patch
up any loop-holes. (In a recent posting an ISE employee seemed to
confirm that this is going to be their approach.)
Even so, these claims are of little value because this kind of program
analysis is neither theoretically possible nor pragmatically desirable.
It would completely prevent *local* determination of the type-safety
of classes. If one cannot know whether a given class is type-correct
except by reference to the programs in which it is used, then one can
never be sure that putting in a new assignment somewhere else in a
program will not make introduce type-errors in other classes. This is
in fact the situation in Eiffel as it currently stands.
A better argument that the insecurities are unimportant is simply that
one never runs into them in real programming. The experience of the
net seems to contradict this claim, because many problems were found
very quickly.
On the other hand, my overall impression is that the insecurities
could be fixed without seriously effecting the overall
"expressiveness" (as in availability of notation) of Eiffel. Nobody
wants to use insecure features unless they have to, so if there is a
secure formulation that provides the same effect, why not adopt it?
This question touches on commercial and political problems, so I will
leave it alone.
Dr. Meyer promised to send out a note on the consistency of the
Eiffel type system, but this has been delayed, as he mentioned in one
of his recent postings.
REDEFINITION
I focus first on the type redefinition rule OOSC page 263:
An attribute, a function result or a formal routine argument
declared in a class may be redeclared with a new type in a
descendant class, provided the new type conforms to the original
one.
The redefinition of attribute types and restriction of formal routine
argument types are both insecure. By insecure I mean roughly that it
is easy to write programs that type-check but produce core-dumps when
executed. Several examples are given (I don't feel like including
them here. Use your imagination.) I propose a simple correction to
the redefinition rule that solves these problems, but prohibits direct
attribute redefinition (this feature should be handled by rebinding a
local type variable, as discussed below):
A function result or a formal routine argument declared in a class
may be redeclared with a new type in a descendant class, provided
the new type conforms to the original one if it is a result type,
and the original one conforms to the new type if it is a formal
argument type.
DECLARATION BY ASSOCIATION
My intuition is that the redefinition rule is the way it is in order
to support declaration by association, and in particular formal
arguments of type "like current" which necessarily involve
type-restriction. However, I argue that the redefinition rule is too
crude to support the kind of typing that is implied by "like current"
and other associate types. In addition, the rules for conformance of
declaration by association are not very carefully defined (and do not
characterize the way the compiler behaves). The conformance relation
is defined on page 262.
A type Y is said to conform to a type X if and only if one of the
following applies:
1. X and Y are identical.
2. X and Y are class types, X has no generic parameters, and Y
lists X in its inheritance clause.
3. X and Y are class types, X is of the form P[U_1, U_2 ,..., U_n],
and the inheritance clause of Y lists P[V_1, V_2 ,..., V_n]
as parent, where every V_i conforms to the corresponding U_i.
4. Y is of the form "like anchor", and the type of anchor
conforms to X.
5. There is a type Z such that Y conforms to Z and Z conforms to X.
It is clear no type ever conforms to "like x" so that, for example,
the following assignment should be invalid:
x : T;
y : like x;
do
y := x;
Note that "like x" conforms to "T" because the type of "x", namely
"T", conforms to "T". Thus the assignment "x := y" is valid according
to the rules. (As Meyer points out in his book, rule 4 is carefully
designed to avoid a more subtle problem involving redefinition, but
the rule messes up the simple case shown here.)
Rather than try to patch up this confusing situation, I propose that
most cases of declaration by association (all but "like Current", see
below) be eliminated from the language, and replaced by explicit type
variables. Using this idea, the code above would become
t = T;
x : t;
y : t;
do
y := x;
x := y;
These type-variables can be "rebound" during inheritance. This
proposal eliminates the "asymmetry" that is the source of the problems
in defining correct type-rules, and also may eliminate the need for
"artificial anchors".
This reformulation of declaration brings out its clear connection to
genericity. We can rewrite the above as:
class proto[t <= T] feature
x : t;
y : t;
main is do
y := x;
x := y;
end
The rebinding of the type variable during inheritance is achieved by
simple generic application:
class actual inherit proto[T'] end
Note that Meyer's paper on "Genericity versus Inheritance" in
OOPSLA'86 should be reviewed in this light. Under my proposal this
the title would read "Genericity versus (Inheritance + Genericity)"
since his original definition of inheritance includes declaration by
association, which I claim is just genericity in disguise.
GENERICITY
The conformance rules for generic types are also very insecure. It is
assumed that a type G[T] conforms to G[S] if T conforms to S. This
can easily lead to type-violations. To achieve security, it is
necessary to examine the "polarity" of the occurrences of generic
parameters. If they are always used only to type attributes and
return-values (values of the generic type can only be "read" from the
objects), then the condition given above holds. If they are used only
as arguments (the object is "write-only" for that parameter) then the
opposite rule holds: G[T] conforms to G[S] if S conforms to T. If
the parameter is used both ways, then *no conformance is secure*.
For example, the cell class from the library does not allow any
conformance:
class Cell[T] feature
info : T;
change_info (x : T) is
do info := x end;
end
That is, Cell[A] should *never* conform to Cell[B], no matter how A
and B are related. One can split this type up, however, and get any
safe conformance that is needed:
class WriteCell[T] feature
change_info (x : T) is
do info := x end;
end
class ReadCell[T] feature
info : T;
end
class Cell[T] inherit WriteCell[T], ReadCell[T] end
Then one has, given A<=B (where <= means conforms to),
Cell[A] <= WriteCell[A]
Cell[A] <= ReadCell[A] <= ReadCell[B]
Cell[B] <= WriteCell[B] <= WriteCell[A]
Cell[B] <= ReadCell[B]
These relations seem rich enough for most situations. (oops, I am
glossing over the potential difficulty of writing "WriteCell" because
it doesn't know about "info". This example is off the top of my head,
so I am not sure what to do about it right now. Probably a hidden
variable and an explicit exported get operation would suffice.)
LIKE CURRENT
The form "like Current" cannot be handled by "type variables", and is
a truly novel and important feature of Eiffel. I note in passing that
conformance of classes using "like Current" must be determined in very
much the same way as classes with generic parameters (and in some
cases in a class A, the type A should not conform to "like Current").
SUMMARY
Replace declaration by association (except the special type "like
Current") with explicit type attributes, which act like bounded
generic parameters with default values.
Eliminate attribute type redefinition and invert the method argument
redefinition rule.
Use the variance ("polarity") of generic parameters, type attributes
and "like Current" to determine what conformance relations arise from
inheritance.
Eiffel is advertised as type-safe. It is not. It has some good
ideas, and brings together features that have not previously been
supported all at once. It has some novel contributions. But I think
the design is immature, and that experience will demonstrate that
these problems will only get worse if not addressed soon.
Comments are welcome. This note was extracted on line, so there may
be errors not found in the paper.
-william cook@hplabs.hp.com