Xref: utzoo comp.object:3434 comp.lang.misc:7695 comp.lang.eiffel:1564
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!casbah.acns.nwu.edu!ucsd!hub.ucsb.edu!eiffel!bertrand
From: bertrand@eiffel.UUCP (Bertrand Meyer)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Summary: Plus Very Boring Ramblings On The Great Virtues Of Static Typing
Message-ID: <566@eiffel.UUCP>
Date: 2 May 91 06:03:19 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991May1.194620.1141@leland.Stanford.EDU>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 159

First I would like to thank Rick Jones for a very clear expose
of system-level type rules, and Craig Chambers for not overreacting
to my somewhat overreacting response to his message. That was
very classy of him. I forgot my Net Rule #1 -
if you are going to post anything negative, let
a night pass first. True, I was rather irritated by Mr. Chambers's
message, since I had the impression that it ignored my earlier answer
and was starting on the old route again. But then Rule #2 says
either you don't join the net or you have to accept that
repeating things is part of the game.
I apologize for the heated reaction. (What worries me is that I did
not receive the usual hate mail this time, only one gentle note
of reproach; am I doing something wrong?)

Now about message <1991May1.194620.1141@leland.Stanford.EDU>
by craig@leland.Stanford.EDU (Craig Chambers):

[!! indicates Mr. Chambers's quotations from message by Rick Jones.
Question numbers in square brackets added by BM.]

> It's hard for me to guess what the results of [system-level checking] are
> going to be in practice. [1]  Will most Eiffel programs type-check, or
> will most not type-check (in the interesting cases)?  It's hard to
> say. [2]  It's also hard for me to say how long the alias analysis will
> take in practice.  Since these rules are much more complex than my
> earlier interpretation of them, I'm no longer sure that they guarantee
> static type safety, either.

> !! [3] Since we seem to be debating different understandings of Bertrand Meyer's
> !! description, perhaps the simplest thing would be for Bertrand to comment on
> !! which of us (if either!) has got it right.

> I think that's probably a wise idea. [4]  But I wish there were some more
> illustrative discussion of these new typing rules, complete with
> examples. [5] Perhaps this will be included in the new Eiffel language
> book?

> [6] To relate these last few messages then to the subject line, I'm no
> longer sure whether Eiffel's new rules will handle the "min" example.

Some partial answers:

[1] I am convinced that 99.5% of Eiffel systems will typecheck
under the complete rules. (I don`t like to talk about the ``new
rules'' because for me they were always there implicitly,
although not completely stated.) The 0.5% that will not
typecheck will be rejected because of actual inadequacies
which could have led to incorrect situations at run time;
full checking will thus be beneficial in this case.

[2] Clearly we are working hard to make the full type analysis
very efficient. I'd rather refrain from any more boasting until
we have actual timing figures to announce, but I am very optimistic.

[3] I think Rick Jones has presented a quite clear picture
of the system-level type validity rules.

[4] Yes, there is a need for more examples. I have tried to
be as clear as possible in the chapter on Type Checking in the
forthcoming revised version of ``Eiffel: The Language''.
I'd like to be able to extract a subset of that chapter
and post it on comp.lang.eiffel, but frankly I don't see
how I can find the time to do this in the next few weeks.
On the other hand, the paper ``Static Typing for Eiffel'',
which was posted twice (either on comp.object or comp.lang.eiffel,
I forgot), presents a reasonably coherent view in spite of a few
material errors. (I have not published that paper in a widely
available printed form because I couldn't think of a publication
or conference that would have accepted it. It is part of a book
that our company distributes, ``An Eiffel Collection''.)

[5] Yes, to some extent. See above.

[6] The complete rules certainly handle the `min' example.
Don't forget, they are the same as the old rules; they simply exclude
certain erroneous cases which would have escaped the incomplete
rules. But they certainly don't limit the expressive power
of the language.

Let me expand. (Since my earlier message conceded defeat,
just consider this as just playing for sheer fun once the ball
game is over.) My fundamental disagreement with Mr. Chambers
is that I do *not* think the problem of static vs. dynamic
typing is one of expressive power. If the type system has
been designed properly then types help you, rather than
constraining you. They make your software much more clear
(through declarations, i.e. useful redundancy); they help the compiler
generate good code; and they enable a static checker (usually
a part of the compiler) to catch errors early rather than late in the
development cycle.

This is only true, of course, if the type system is complete enough;
this means the presence of genericity, constrained and
unconstrained, of the reverse assignment attempt for
forcing a type on a known object,
and of anchored declarations (the `like something'
type construct). Without these mechanisms, static typing in
an object-oriented language is, as believe,
either impossible or simply a joke (as in C extensions when you spend
your time casting back and forth between pointer types).
Furthermore, although this is more controversial, I am convinced by
my experience, confirmed by that of many Eiffel users
and by the absence of any practical argument to the contrary,
that for typing to work in practice with inheritance requires a 
covariant redefinition policy. If the mathematical models for
contravariance are simpler, then that's too bad for mathematics.
Denotational semantics 0, software engineering 1.
(By the way I love denotational semantics, even wrote a book on it,
but I believe that scientists should build theories to fit the practice,
not the other way around.)

As a consequence I believe that *conceptually* a good statically typed
O-O languages is *always* better than a dynamically typed one,
because you don't lose anything: if what you want is a fast,
non-type-checking interpreter or compiler, then you can always build one
for a statically typed languages; programmers then won't lose anything as
compared to Smalltalk or CLOS, save for the effort needed to write a
few declarations, which they'll probably find helpful anyway.
But the reverse is not true: if you have a dynamically typed language,
you will *never* be able to write a type checker for it because it
would lack the necessary information. (ML fans might disagree here,
but we'll have to wait until they have produced OOML.)

Does this mean that static typing is always good and dynamic
typing always bad? (I can hear the rumblings: who is the creationist
here?) The answer would be yes except for one strong argument in
favor of dynamically typed languages: they can be processed very
quickly, enabling developers to try out new ideas without the
interference of a static type checker, which may take some time to
perform its duties. If speed of development is more important than
reliability and efficiency of the resulting product, this makes
dynamically typed languages attractive if they are backed by tools
ensuring a fast turnaround.

In other words, I don't think, as Mr. Chambers does, that the static
vs. dynamic debate is a conceptual discussion at all.
Conceptually, static wins hands down every time.
What the debate is about is much more mundane:

	It's purely a question of implementation.

If we were able to build static checkers that were totally
unobtrusive performance-wise, and did their work in - say -
ten seconds after a comparatively small change even to a very large
system, then who in the world would forsake the extra benefits of type
checking?

Solving this problem - that is to say, a Very Fast Reexecution Cycle,
comparable to the change-to-reexecute cycle of the best interpreters,
without sacrificing any of the fantastic advantages of full type checking -
has been our obsession for several years. We are convinced we now have
the technology to do it, but no one has to believe this until the day
it's out on the desks of Eiffel users. You can count on us for
not sparing our time to make this happen as quickly as possible,
and for not being too shy about it then.
-- 
-- Bertrand Meyer
Interactive Software Engineering Inc., Santa Barbara
bertrand@eiffel.uucp