Xref: utzoo comp.object:3432 comp.lang.misc:7692 comp.lang.eiffel:1562
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!asuvax!ncar!elroy.jpl.nasa.gov!sdd.hp.com!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: <1991May1.194620.1141@leland.Stanford.EDU>
Date: 1 May 91 19:46:20 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> <1150@tetrauk.UUCP>
Sender: news@leland.Stanford.EDU (Mr News)
Reply-To: craig@self.stanford.edu
Organization: Stanford University
Lines: 50

In article <1150@tetrauk.UUCP>, rick@tetrauk.UUCP (Rick Jones) writes:
|> We clearly have a different interpretation of the proposal.
|> 
|> In article <1991Apr30.213115.9990@leland.Stanford.EDU> craig@self.stanford.edu writes:
|> } 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.

I just finished reading through my copy again, and I think I have to
retract what I said about Eiffel's new rules.  There is some sort of
analysis more precise than "any assignment in the program" that
Bertrand calls "alias analysis" in the proposal.  This analysis tracks
which variables have been assigned to which other variables or formal
parameters, and then does checking of feature application based on the
statically declared types of any variable/parameter which could be
assigned/passed to the receiver of the message and the parameter to
the message.  It's not as precise as the Typed Smalltalk type
inference and checking algorithm, though.  I don't know if your GTA is
closer to (my new interpretation of) Bertrand's proposal or to the
Typed Smalltalk approach.

It's hard for me to guess what the results of Bertrand's proposal are
likely to be in practice.  Will most Eiffel programs type-check, or
will most not type-check (in the interesting cases)?  It's hard to
say.  It's also hard for me to say how long the alias analysis will
take in practice.  Since these rules are much more complex than my
earlier interpretation of them, I'm no longer sure that they guarantee
static type safety, either.

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

I think that's probably a wise idea.  But I wish there were some more
illustrative discussion of these new typing rules, complete with
examples.  Perhaps this will be included in the new Eiffel language
book?

To relate these last few messages then to the subject line, I'm no
longer sure whether Eiffel's new rules will handle the "min" example.

-- Craig Chambers