bertrand@hub.ucsb.edu (Bertrand Meyer) (01/11/89)
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
bertrand@hub.ucsb.edu (Bertrand Meyer) (01/18/89)
The article reference above mentioned that I was working on a paper explaining and justifying the Eiffel type system. The paper expands on the ideas sketched in the previous message, and gives a precise definition of the Eiffel type rules, complementing the rules stated in ``Object-Oriented Software Construction''. It was announced for this week but will not be ready until early February. (I will be away from my Santa Barbara office until then and have ``almost'' been able to complete the paper before departing in a few hours.) The paper is too big to be posted on the net (and anyway includes math symbols and other features that make it impractical for this medium). I will be glad to send a paper copy to anyone who requests it. Please send a message to queries@eiffel.com with a subject header saying just ``Type paper'' and a message text that gives your postal address. You should expect to get the paper by February 15. Bertrand Meyer bertrand@eiffel.com