Xref: utzoo comp.object:3392 comp.lang.misc:7645 comp.lang.eiffel:1549
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!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: Followups to talk.religion
Message-ID: <556@eiffel.UUCP>
Date: 28 Apr 91 22:50:03 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU>
Organization: Interactive Software Engineering, Santa Barbara CA
Lines: 67

In <554@eiffel.UUCP> I offered a straightforward Eiffel solution
to Craig Chambers's problem, supposedly intractable by typed
languages.

In <51986@nigel.ee.udel.edu>, new@ee.udel.edu (Darren New) replies: 
	
	[Quoting from my solution]:
	>> one could define `min' in that class as
	>> 	min (other: like Current): like Current is

	[His comment]:
	> Doesn't look like you've answered the question here.  What's the
	> type of `min'?

Now let us repeat patiently: the type of `min' is `like Current'.
`like' is an Eiffel keyword whose meaning was explained in my message,
and the corresponding typing mechanism (declaration by association)
is makes static typing possible in practice. Thank you for your attention.

	> I don't even know Eiffel. Maybe the response would
	> be obvious if I *did* know Eiffel.

It is generally considered preferable to know first and then criticize.
But it is never too late to know.

Here now is the response by Craig Chambers:
> 
> Eiffel's rules allow this to be type checked by having broken type
> checking rules, in my opinion.  Covariant type-checking rules do not
> enure type safety statically (you mention this towards the end of your
> message).  The newer proposed rules (as yet unimplemented, I believe)
> do ensure type safety statically, but by effectively enforcing a
> contravariant typing discipline which then prevents this example from
> being type checked.  I suspect that the new type checking rules will
> never actually be implemented and widely adopted since they will
> disallow many existing Eiffel programs which have relied on the
> covariant type checking rule.
> 
> The main purpose of my example was to convince fans of static type
> checking as done in most existing OO languages that these type systems
> are not powerful enough to describe relatively simple, useful programs
> (and preserve static type safety), and that OO language designers
> should incorporate more powerful type systems if they really want to
> claim that their type systems do not reduce expressive power over what
> exists naturally in dynamically-typed OO languages.

I have quoted this text in full because I can't repress a feeling of
admiration for the skill it takes to accumulate so many
misrepresentations in so few lines. To call Eiffel's rules
``contravariant'', for example, is a quite remarkable achievement.

This forum has seen the same claims made time and again, and time and
again rebuked, but whenever you cut the dragon's head a new one
grows back. Rational debate is useless; dynamic typing is good,
and static typing is at once bad, useless, and impossible.

I have always felt sympathy towards the biologists who accept
to debate creationists. Now I also understand them better;
one can fight opinions, not articles of faith.

Not having the infinite amount of both time and patience which
it would take to continue, I quit, declaring total rhetorical
defeat.
-- 
-- Bertrand Meyer
Interactive Software Engineering Inc., Santa Barbara
bertrand@eiffel.com