🚀 go-pugleaf

sommar@enea.se (Erland Sommarskog) writes:

>Also sprach Urs Hoelzle (hoelzle@leland.Stanford.EDU):
>>	type T = "some type"
>>	type SubT = "subtype of T"
>>
>>  [ List[SubT] is *not* a subtype of List[T] ]

>In which type system? If you imply the type system in any statically
>typed language, I have news for you. The Eiffel code below compiles 
>and executes just fine. 
> [Eiffel code]

It is a well-known fact that Eiffel does not strictly enforce
contravariance, and it is equally well-known that there are (very
simple) programs which type-check in ISE's implementation but bomb at
runtime because of a type error [programs available on request; you
can find them yourself in the ECOOP'89 proceedings].  Thus, Eiffel (in
its current implementation) is not a statically-typed language because
there may be run-time type errors.

There are two points that I should mention in Eiffel's defense:

1) Last year, Bertrand Meyer described a solution to the current type
   holes sometime last year.  The newest Eiffel release might
   implement this.

2) Eiffel does indeed try to overcome the restrictions of
   contravariance (which is basically what I'm calling for), but it
   does it by totally abolishing contravariance, and I'm not sure this
   is the right way to go.

   Furthermore, the proposed fix to Eiffel's type holes is very
   strict.  Informally speaking, you can have either assignments of
   the form aListOfComparable := aListOfString OR calls of
   aListOfComparable.append(aComparable) *in your entire system*.
   Since any non-trivial system (which actually uses covariance) will
   have both, the program will not type-check and we're back to
   contravariance.
   
So: either Eiffel isn't type-safe, or any actual use of covariance in
a realistic program will not type-check.  Or, to put it differently:
in *any* type system, one of the following two assertions is true:

(I)  List[SubT] is not a subtype of List[T] (i.e. you cannot *always*
     substitute a List[SubT] for a List[T]).

(II) The type system is safe, i.e. there will be no run-time type errors
     if a program passes the type checking.

Since (at least in the context of this discussion) we're only
interested in type-safe languages where (II) is false, it follows that
(I) must be true.

-Urs
   
-- 
------------------------------------------------------------------------------
Urs Hoelzle                                            hoelzle@cs.stanford.EDU
Center for Integrated Systems, CIS 42, Stanford University, Stanford, CA 94305