🚀 go-pugleaf

There have been a number of recent postings in comp.lang.eiffel
pointing to purported deficiencies in the Eiffel type system.
(I am referring here in particular to postings by David Robbins
and Jos Warmer; there was also an earlier one which I cannot
trace at the moment.) The problems have also been addressed in
two documents that I know of:

	-  A review of my book ``Object-Oriented Software
Construction'' (OOSC) by Pierre America from Philips Eindhoven,
to appear (or perhaps having already appeared) in
``Science of Computer Programming''.

	- A report (somewhat equivalent to a Master's Thesis)
by Philippe Elinck, a student at the Universite Libre de Bruxelles.
(This report is in French and includes much more, in particular an
Eiffel-to-Ada translation scheme; I only received it yesterday,
although I was aware this work was going on. The report as a
whole is a very interesting piece of work and I hope the author
gets something published out of it.)

Finally there is also a (so far private) technical report that
was recently sent to me.

These various documents and newsgroup postings to apparent holes
in the Eiffel type system. Some suggest solutions.

This note is a brief statement of my view of the problems
discussed. I am in the process of writing a longer discussion
which should be ready by next week (third week of January); I
will post a draft to this newsgroup as soon as I have a showable one.
Here I will just summarize what I believe are the key points.

1. The problems raised by the contributions mentioned address
inconsistencies that can arise essentially for two reasons:

	- The Eiffel rule that attributes and routine arguments
	may be redefined, in a descendant class, to a descendant
	of their original type.

	- The orthogonality of the inheritance and information
	hiding mechanisms

Some variants of these problems arise because of genericity and
the mechanism of declaration by association; however I don't
think these introduce anything conceptually new.

2. The Eiffel rule with respect to type redefinition is
incompatible with the ``contravariant rule'' found in
some formal semantics models, especially the
Cardelli model of inheritance. Since I have been following
Cardelli's work for several years (and in fact included a
description of it in a forthcoming book to be published by
Prentice-Hall, ``Introduction to the Theory of Programming
Languages''), this departure from ``accepted wisdom'' was by no
means accidental. The motive was clear - a pragmatic one: the
contravariant rule essentially makes inheritance-based typing
useless. The Eiffel ``covariant'' rule is the only one that
works in practice. I believe that anyone who writes serious
software in Eiffel (as opposed to experiments with the language)
will have realized this very quickly.

3. The covariant rule makes the definition
of typing constraints more subtle than indicated in OOSC.
The reason for this is simply that I had not understood all the
subtleties of the issue when I wrote the book. Clearly this will
be corrected in future editions.
(Actually I am envisioning a
whole chapter on typing to discuss the issue thoroughly, perhaps
starting from the brief discussion which will appear in the Eiffel
column for the March issue of the Journ. of O-O Prog.).

4. Although OOSC does not mention the potential problems
(because its definition of type is not sufficient), they are
documented in the Eiffel User's Manual as cases of incorrect
type combinations that will escape the vigilance of the
type checker (and yield a run-time exception).

5. Interestingly enough, these problems occur extremely rarely
in practice; in our experience of several hundred thousand lines
with Eiffel we have never encountered them. User experience
seems to confirm this completely.

6. This is not satisfactory, however; Eiffel is meant to be
fully statically checked.

7. The problems can be corrected fairly easily by making the
type system much more restrictive than it is now; essentially
this would mean disallowing assignments of the form x := y
whenever D (the class type of y) inherits from C (the class type
of x) but there is ``something suspicious'' in D (such as a type
redefinition according to the covariant rule, or hiding of a
previously exported feature).

8. The preceding solution (which has been recommended by some
contributors) is easy to implement but seems far too drastic.
It excludes what seems to be legitimate software texts, which
would not raise any problem at execution time.

9. We believe that the Eiffel type system is sound, although the
type rules given by OOSC need to be refined. We have
formulated what we believe are correct rules, which
are still simple and can be taught fairly easily.
The forthcoming paper will detail these rules.

10. We also think that we have found a way to integrate the
checking of these rules into the Eiffel automatic, modular
recompilation mechanism (the ec/es commands) without
significantly impairing performance. In the absence of a formal
proof of correctness it is impossible to make a final
commitment, but I am confident that within a few months (and, I
hope, with the forthcoming version 2.2) all examples of
incorrect behavior exhibited by the various contributors
will give rise to compilation errors - without any significant
loss in the expressive power of the language.



To summarize: I am convinced there is nothign wrong with the Eiffel
type policy, even though the rules
have not been stated rigorously enough, especially in OOSC.
The problem is not with the language but with the current tools:
they fail to detect certain violations, which is annoying even
though these violations hardly occur in practical usage of
Eiffel. The tools will be fixed soon.

More details will be given in the forthcoming article. I am
grateful to the various contributors to this discussion
for bringing out the problems in a much clearer fashion than I
had.

-- Bertrand Meyer, Interactive Software Engineering

bertrand@eiffel.com