Xref: utzoo comp.object:3431 comp.lang.misc:7691 comp.lang.eiffel:1560
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.object,comp.lang.misc,comp.lang.eiffel
Subject: Re: A Hard Problem for Static Type Systems
Message-ID: <1150@tetrauk.UUCP>
Date: 1 May 91 10:43:16 GMT
References: <1991Apr20.010347.28984@leland.Stanford.EDU> <554@eiffel.UUCP> <1991Apr26.203642.17387@leland.Stanford.EDU> <556@eiffel.UUCP> <1146@tetrauk.UUCP> <1991Apr30.213115.9990@leland.Stanford.EDU>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 58

In article <1991Apr30.213115.9990@leland.Stanford.EDU> craig@self.stanford.edu writes:
} 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.

We clearly have a different interpretation of the proposal.

} 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 is where we disagree.  The proposal as I read it (I have just gone
through my copy again) clearly relates the application of a feature to the
variable used to apply it.  Your interpretation would be no more complex to
implement than the existing checker, just a lot more restrictive.  If this were
the case, I would also consider it to be unusable.

} 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).

Not quite.  The use of simple type conformance based on inheritance as a
starting point enables the full type checking to be done without actually
indulging in flow analysis.  I will not attempt to formally justify this, as I
am not a language theoretician;  I am merely explaining my understanding of
Bertrand Meyer's description of how it will work.

} 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.

This I can believe, but since Smalltalk starts off with no explicit types or
simple static type conformance rules, this is the only way to work it out.
I believe it _can_ be done in Eiffel, and without flow analysis per-se.

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.
-- 
Rick Jones, Tetra Ltd.  Maidenhead, Berks, UK
rick@tetrauk.uucp

Any fool can provide a solution - the problem is to understand the problem