[Types-sig] expression-based type assertions (was: Static typing considered ...UGLY)

[Jeremy Hylton]

>>>>> "GS" == Greg Stein <gstein@lyra.org> writes:

  GS> On Tue, 14 Dec 1999, Paul Prescod wrote:
  >> ...  > Please Greg/Fred/Sjoerd, can you write a proposal which
  >> starts where >
  >> http://www.foretec.com/python/workshops/1998-11/greg-type-ideas.html
  >> > ends (reading the first 9/10 of that was ... illuminating in
  >> hindsight, > but off-putting on the way there).  It looks pretty
  >> promising ...
  >> 
  >> Let me point out again that while that approach is interesting,
  >> it doesn't solve the problem I was recruited to solve: a *static*
  >> *compile-time* checker.

[I was in starting a response to Paul when Greg's mail arrived, so I
merged the responses.  Hoping to maximize confusion.]

Perhaps we need a charter revision.  We need to formally define a type
system for Python.  It may or may not be statically checkable --
that's just the way type systems work, e.g. Java does array bounds
checks at runtime because it can't at compile time.  The fact that
array bounds are checked at runtime doesn't mean that Java's type
system forbids referencing past the end of an array; it just can be
statically checked (or at least no one has figured out a practical way
to check it).  The point of this digression is to argue that saying
you only do "compile-time" checks is a bit of a cop out.

  GS> Yes, it does :-)

I agree.

  GS> As I mentioned in my note to Eddy just now, the compiler can use
  GS> the assertions to determine an expression's type (assuming it
  GS> isn't already available through inference). The type can then be
  GS> used in the checks.

  GS> Specifically, the "GFS proposal" would lead to the following
  GS> types of compile-time checks:

  GS> * is the type correct for each parameter of a function call?  
  GS> * is the type correct for the function return value(s)?  
  GS> * will a type assertion (the '!' operator) possibly fail?

These sounds like exactly the right place to start!

  GS> And to reiterate a point from my last note: I believe checks
  GS> associated with shoving a value into a name are not as
  GS> interesting, as 99% of the errors will occur at code boundaries
  GS> (function calls), which are handled by the above mechanism.

  GS> In fact, I would even say that the only type declarations used
  GS> would be associated with function params and returns (and not
  GS> variable). If you are implementing a function and want to ensure
  GS> that a result has a proper type, then the '!' operator can be
  GS> used (shoving it into a typed variable isn't going to help
  GS> you!).

I think I agree with you as far as local variables.  It becomes quite
interesting when you're talking about attributes of objects, e.g. what
is the type of the closed attribute of a builtin file object.  (For
that matter, what is the type of the builtin open function and how
does it differ from a function that returns a StringIO object?)

Jeremy