nick@lfcs.ed.ac.uk (Nick Rothwell) (03/12/90)
In article <264@eiffel.UUCP>, bertrand@eiffel (Bertrand Meyer) writes: > Every once in a while someone ``discovers'' that the Eiffel type >system is ``wrong''. The latest printed occurrence I know of is a letter >published in the last JOOP. > > The Eiffel type system is neither ``shakey'' nor wrong. >... > Denying the validity of Mr. Rothwell's statement would be >contradicting a matter on which he is better informed than I am: >his personal opinion regarding the Eiffel type system. >There is no reason to doubt that the statement is true, >although it provides information about Mr. Rothwell, not about Eiffel. ...touche... :-) I didn't make the claim that the Eiffel type system is "wrong". My statement was that it "seemed shakey" to me; I've only read the Software Construction book, which does not seem to give a good description of the type system. It may well be perfectly sound, and there may be other literature proving its soundness, but I was less than convinced based on my reading of the book. Perhaps I shouldn't have aired my views in public. > Unfortunately for the theoreticians, the Eiffel rule is the one that >makes sense in practice. To take a very simple example, take the generic >class Unfortunately, such statements do nothing to improve people's faith in the soundness of the type semantics. A thorough, semantic description of the type system would go a long way to banishing people's fears (mine included). >5. I have known for a long time Luca Cardelli's elegant work >(A Semantics of Multiple Inheritance, in Semantics of Data Types, >edited by Gilles Kahn, David B. McQueen and Gordon Plotkin, >Lecture Notes in Computer Science 173, Springer-Verlag, New York, >1984, pp. 51-67). This denotational model of some of >the properties of inheritance suggests a contrapositive rule. >Enamored as I may be of denotational semantics, however, I think that in >science theories should be made to fit reality, not the other way around. >Physicists are not supposed to change experimental results which do not >agree with the model. Could you explain what you mean here? The analogy with physics is not really valid; I don't see why a theory should be built to explain an existing (and perhaps totally ad-hoc) language; why not design a sound type system and implement a language which uses it? >-- Bertrand Meyer Nick. -- Nick Rothwell, Laboratory for Foundations of Computer Science, Edinburgh. nick@lfcs.ed.ac.uk <Atlantic Ocean>!mcvax!ukc!lfcs!nick ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ A prop? ...or wings? A prop? ...or wings? A prop?