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

[Greg Stein]

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.

Yes, it does :-)

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

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

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

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

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

In both cases, expression- and name-based type assertions, I think you
require type inferencing. So I don't think the problem is simplified by
virtue of using name-based assertions. All you really get is an
compile-time assertion at assignment time, which is also provided by an
expression-based typing.

In other words:

  Int a
  a = foo()

vs.

  a = foo() ! Int

In both cases, the compiler will throw a fit if it knows foo() always
returns a String.

Cheers,
-g

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