problems/risks due to programming language

[Bertrand Meyer]

>From <2628 at castle.ed.ac.uk> by nick at lfcs.ed.ac.uk (Nick Rothwell):

> The [Eiffel] type system seems a bit shakey to me.

>From <53012 at microsoft.UUCP> by jimad at microsoft.UUCP (Jim ADCOCK):

> How can the words 'strong type checking' be applied to a language
> [i.e. Eiffel] that gets its permissions on return types exactly
> backasswards?  Fix your *own* language, before throwing stones, Bertrand!


    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. I have
written a long paper (posted in comp.lang.eiffel as
<176 at eiffel.UUCP> and <177 at eiffel.UUCP> in July of 1989)
explaining why the type rules are what they are. This answered in
particular an earlier paper by William Cook. My paper has not been
published in print (for lack of time and because I will
reuse it as book chapter), but it has been fairly widely circulated
since it was first posted.

    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.

    It is not, however, a very pleasant statement, for impressions are
easy to spread and hard to fight.

    This is like when a person is being criticized: if Paul says Peter
has stolen Paul's car, Peter can defend himself; if Paul spreads
the rumor that Peter is a shady (or shaky) character, what can Peter do?
I have strong opinions, and have not been shy in publicizing what
I think of C++, but I have endeavored to focus on concrete technical
arguments addressing specific points. Reciprocality will be appreciated.

    Mr. Adcock's suggestion is gratefully acknowledged but
Eiffel's type system needs no fixing. I have had some trouble
understanding his message; first I do not know the word ``backasswards'',
although my limited but improving knowledge of English leads me to
gather that this word is not likely to carry an entirely favorable
connotation. Second, I have not heard anyone else criticize the
Eiffel rule for redefining the ``return type'' (which I understand
as the type of a function's result). In Eiffel this has to be a
descendant of the original type, not raising any problem that I know of.

    What has been criticized before (and I must assume this is what
Mr. Adcock really had in mind) is the rule for routine arguments,
which is the same as for results. This shocks many people who approach
the problem from a purely theoretical perspective; the absence of a
precise discussion of this topic in my book ``Object-Oriented Software
Construction'' did not help here. (Obviously I should have been more
careful.)

    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

    LIST [T]

with a procedure

    insert (x: T)

Assume a class and one of its heirs, for example STUDENT and its heir
UNIVERSITY_STUDENT. With the declarations

    sl: LIST [STUDENT] 
    usl: LIST [UNIVERSITY_STUDENT] 

the call ``sl.insert (s)'' should be valid for any s of type STUDENT,
but the call ``usl.insert (s)'' should be valid only for s of type
UNIVERSITY_STUDENT. The ``contrapositive'' rule advocated by some
would require that the version of ``insert'' for class
LIST [UNIVERSITY_STUDENT] take arguments whose types are *ancestors*
of STUDENT! This does not make sense - nor does the rule suggested by
the authors of the JOOP letter, according to whom it should not be
possible to change the argument types. They cite this as being the C++
rule. My congratulations to anyone who can write  useful software
in these conditions. (This is impossible, of course, and is one
of the reasons why undisciplined type casts are constantly needed
in such a context. I think this makes a mockery of
object-oriented ideas.)

    What the above simply means is that type checking in an
object-oriented language is more difficult than what a two-minute
peek at the problem might suggest.

    By the way, Eiffel's genericity (parameterized classes, such as
LIST [T]) only makes the problem more visible; the same argument could
be applied without any use of genericity.

A few more comments:

1. It would be immensely pleasurable if critics of the Eiffel type
rules would work under the assumption that Eiffel's designers,
although they have made mistakes and will undoubtedly make
more, are not *totally* incompetent.

2. In the same vein, our experience may have given us a perspective that
not all outside commentators enjoy. We have written tens of thousands of
lines of typed, reusable object-oriented software, including libraries
that are used daily by hundreds of people. Once again
this does not make us infallible, but I know of very, very few people in
the world today who have that kind of experience, and the appreciation
it gives for what works and what does not.

3. I have seen no one mention what I think is one of Eiffel's
significant contributions: a type system which is fully uniform, and
entirely based on the notion of class. Even integers and booleans are
theoretically based on classes (through ``expanded types''), with no
loss of efficiency at the implementation stage.

4. One thing that does need fixing is the amount of type checking done
by our current compiler, which misses some cases. The reason this has
not been done before is that these cases occur extremely rarely in
practice (for example there has not been a single recorded case in our
company), so that we have devoted our forces to more urgent tasks.
However the situation will be corrected in the next major release.

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.

This, of course, assumes somewhat arrogantly that Eiffel's rules
are ``the reality''. Quite frankly, I would prefer the
type rules to be as simple as Cardelli's work suggests but,
as mentioned above, I don't see any other usable solution than Eiffel's.
If someone can come up with a better suggestion, I will be the first
to embrace it. In the meantime, we'll have to live with a useful
practical solution even if it pains the theoreticians. Sorry.

6. Finally, our group does not just talk about Eiffel but also
implements it. The type rules that we use makes type checking more
difficult. Like everyone else we prefer easy jobs to hard jobs;
one more reason to welcome any simpler solution - provided it also
works.

-- Bertrand Meyer
bertrand at eiffel.com