[Types-sig] Non-conservative inferencing considered harmful

[Greg Stein]

On Wed, 22 Dec 1999, Paul Prescod wrote:
> Greg Stein wrote:
> > ...
> > I maintain that it could be declared type-safe. In fact, it is reasonably
> > straight-forward to generate the type information at each point, for each
> > value, and then to verify that the .doSomething is valid.
> 
> Greg, you are getting into exactly what I want to avoid. Let's say the
> first doSomething returns an int and the second doSomething returns a
> string. Now you are trying to statically bind it to an integer-bearing
> parameter. What's the appropriate error message:
> 
> > > a = [Foo(), Bar()]
> > > 
> > > ... 10,000 lines of code ...
> > > 
> > > for el in a:
> > >    j = el.doSomething()
> > > 
> > > ... 10,000 lines of code ...
> > > decl k: Int
> > > k = j
> 
> "Warning: integer|string cannot be assigned to integer."
> 
> Note also that the point where the error message occurs may be miles
> from the place where you did the funky thing that allowed the variable
> to take two types. 

That is *exactly* what would happen in my proposal.

Yes, the error is located at the assignment, and that is a good distance
from the assignments to "a" and "j". If you want to tighten up the code,
then declare "a" or "j". It will fail at whatever point you feel the code
is "wrong".

BUT!! -- you never said what the error in the program was, and what the
type-checker was supposed to find:

1) was "a" filled in with inappropriate types of values?
2) was "j" assigned a type it wasn't supposed to hold?
3) was "k" declared wrong?

In the absence of knowing which of the three cases is wrong, I *strongly*
maintain that the error at the "k = j" assignment is absolutely correct.
How is the compiler to know that "a" or "j" is wrong? You didn't tell it
that their types were restricted (and violated).

In other words, the error message is NOT "miles away". It is exactly where
it should be. When that error hit, the programmer could have went "oops! I
declared k wrong. I see that j is supposed to be an Int or a String.
okay... lemme fix that..."

Find another example -- this one doesn't support your position that
inferencing is harmful.

> This is EXACTLY the sort of error message that made me run screaming
> from the last language that tried to "help" me with data flow analysis
> and type inferencing. To put this is in the strongest possible terms,
> this sort of data flow analysis/inferencing "helps" me like MS Word's
> guessing what I mean when I "misspell" happy face (e.g. Python code) and
> Word fixes it for me. We are trying too hard and the result will be
> non-intuitive. There is no need to complicate our system in order to
> handle these corner cases. If the user wants a to be a List of (Foo|Bar)
> then they can darn well SAY SO.

Sure. And in the absence of saying so, the inferencer above did exactly
what it was supposed to do. You have one of three problems in your code,
yet no way for any compiler to know which one you meant.

If you want to sprinkle declarations throughout your code, then be my
guest. But you don't have to. Python has very clean and rigorous execution
semantics that we can easily and deterministically determine type
information.

I hate the thought that people are going to start feeling that they should
put declarations into their code. We will lose one of the best things of
Python -- the ability to toss out and ignore all that declaration crap
from Algol-like languages. If you give a means to people to declare their
variables, then they'll start using it. "But it's optional!" you'll say.
Well, that won't be heard. People will just blindly follow their C and
Java knowledge and we will lose the cleanliness of syntax that Python has
enjoyed for so long.

> It is because of this experience that I am strongly of the belief that
> we should do NO flow analysis in the normative part of our type system.

I disagree, and your example does not support that position.

Cheers,
-g

-- 
Greg Stein, http://www.lyra.org/