Xref: utzoo comp.object:3370 comp.lang.misc:7624 comp.lang.eiffel:1544
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!samsung!uunet!stanford.edu!leland.Stanford.EDU!leland.Stanford.EDU!craig
From: craig@leland.Stanford.EDU (Craig Chambers)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1991Apr26.203642.17387@leland.Stanford.EDU>
Date: 26 Apr 91 20:36:42 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP>
Sender: news@leland.Stanford.EDU (Mr News)
Reply-To: craig@self.stanford.edu
Organization: Stanford University
Lines: 47

In article <554@eiffel.UUCP>, bertrand@eiffel.UUCP (Bertrand Meyer) writes:
|> I don't know about ``most statically-typed object-oriented
|> languages'' but in Eiffel this does not appear particularly
|> difficult. Class COMPARABLE describes order relations;
|> one could define `min' in that class as
|> 
|> 	min (other: like Current): like Current is
|> 			-- Minimum of current element and `other'
|> 		do
|> 			if Current < other then
|> 				Result := Current
|> 			else
|> 				Result := other
|> 			end
|> 		end -- min
|> 
|> In COMPARABLE, the operator "<" means a call to the following
|> function:
|> 
|> 	infix "<" (other: like Current): BOOLEAN is
|> 			-- Is current element less than or equal to `other'?
|> 		deferred
|> 		end -- "<"
|> 
|> Then INT, FLOAT and SORTED_LIST (a generic class) may inherit
|> from COMPARABLE and provide an effective declaration for infix "<". 

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.

-- Craig Chambers