Xref: utzoo comp.object:3419 comp.lang.misc:7682 comp.lang.eiffel:1555
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!spool.mu.edu!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: <1991Apr30.213115.9990@leland.Stanford.EDU>
Date: 30 Apr 91 21:31:15 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU> <556@eiffel.UUCP> <1146@tetrauk.UUCP>
Sender: news@leland.Stanford.EDU (Mr News)
Reply-To: craig@self.stanford.edu
Organization: Stanford University
Lines: 98

In article <1146@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes:
|> The "holes" in Eiffel's current type system, pricipally resulting from
|> covariance, are that it may allow var to refer to an object which is a
|> supertype of A.  However, var's implicit type is also a supertype of A.
|> Provided no object is ever attached to var which is a supertype of var's
|> IMPLICIT type, then the system is type-safe.  This analysis is statically
|> feasible, and is what GTA sets out to do.

I don't think you are describing the proposal to fix Eiffel's typing
rules, at least as I understand it.  Bertrand has explicitly stated
that he isn't proposing complete flow analysis of the program to
detect type errors.  If there is a call to feature F *anywhere in the
program* then the type checker assumes that feature F will be called
for any variable declared to be a type that includes F.  This then
prevents the program you are describing to type-check (assuming that
all three features of the declared type in your example are called
somewhere in the program).

Put another way, the type system you describe completely ignores the
declared types of variables, using interprocedural flow analysis to
compute what you call the implicit type of a variable; see the above
quote for an example (the explicit type of "var" is never used).
Although I like the results of this kind of type system (nearly all
legal programs will type check with little effort on the part of the
programmer), I don't believe that the necessary flow analysis is
particularly feasible.  The Typed Smalltalk people do include a
type-checking system that uses flow-sensitive analysis like you
describe (abstract interpretation of the program in the type domain),
but the algorithm is exponential (double-exponential?) in the worst
case.

|> It should also be noted that GTA resolves the infamous polygon/rectangle
|> problem.  Here we have a class POLYGON, whose number of vertices can be
|> altered.  A descendant of POLYGON is RECTANGLE, which is intuitively a
|> sub-type, but clearly must have a fixed number of vertices.  Thus RECTANGLE
|> inherits POLYGON, but does not export the add_vertex feature (and probably some
|> other non-applicable ones as well).  The effect in terms of types is that
|> RECTANGLE is not a subtype of POLYGON is terms of complete types, but it is a
|> subtype of a particular set of POLYGON partial types - those which exclude the
|> features inapplicable to rectangles.  Thus a variable of type POLYGON may
|> safely have a RECTANGLE object assigned to it provided the implicit type of the
|> variable is a supertype of RECTANGLE.  A program which includes an assignment
|> of a RECTANGLE object to a POLYGON variable of an invalid implicit type will be
|> caught be the GTA system.

No.  If there is a call to add_vertex *anywhere in the program*, then
*all* assignments of rectangles to polygons will be declared illegal
by Eiffel's proposed type system.

|> This quite clearly does not "reduce Eiffel's type system to contravariance",
|> but allows covariance to be used completely safely.  It is worth noting that
|> Craig Chambers' "hard problem" is only irresolvable in a static type system if
|> you demand contravariance (which he did in his initial posting) - but then most
|> problems are irresolvable in a useful way with contravariance.

I admit I was a bit hasty in my implication that Eiffel's new rules
are nothing more than requiring contravariance.  I should have said
that the following rules will type-check the same programs, no more
and no less, as Eiffel's new rules:

1) Remove all features that are never invoked in the program.

2) Construct a type hierarchy from the class hierarchy such that one
class is a subtype of another iff it obeys the normal subtype
conformance rules using contravariance.

3) Disallow all assignments in the program where an expression of one
class is being assigned to a variable (or passed as a parameter) that
is declared to be a class that's not a legal supertype.

This phrasing of the rules make it easier to compare Eiffel's new type
system with those of other languages, and highlights the fact that
assignments from one type to another can only take place where normal
contravariant subtyping rules would allow.  This is only natural,
since some form of these rules is necessary to allow static type
safety.  But it does pose problems for existing Eiffel programs that
rely on covariant type checking (more akin to the implicit type
checking that you describe).

If I have misunderstood Eiffel's new rules (again), I'd appreciate
being set straight.  The easiest way to do that is to post an example
program that will type-check under Eiffel's new rules that won't under
the rules I've listed above.

|> His point
|> really seems to be that static type checking with covariance isn't type
|> checking at all, so dynamic typing is better.  However, GTA allows covariant
|> flexibility combined with static checking, which in fact checks exactly the
|> same things that a dynamically typed language checks at run-time.

No, I'm saying that covariance (by itself) isn't statically type safe,
so a better type system is needed.  Some fairly powerful type systems
have been developed for more theoretical languages and for functional
languages, and I'm sure that one could be developed to handle the
"min" example I posed.  The main point is that current popular OO
languages are a far cry from these type systems.

-- Craig Chambers