[Types-sig] Static name checking

[Paul Prescod]

Martijn Faassen wrote:
> 
> [freezing system]
> > A frozen name checker would work by loading a document and parsing it
> > looking for every reference to the name "frozen". Then it would look at
> > the next line and verify that all referenced objects really are frozen.
> > Then it would check that frozen namespaces are not modified. Of course a
> > frozen name checker isn't trivial but it also isn't brain surgery.
> > Anyone bored and underworked out there?
> 
> But what do you do with lists (for instance)? You can't check at
> compile-time if an object that comes from a list is a string, and
> integer, or an object. If you then try to refer to a name in it
> (object.foo()) then you run into trouble with this concept. Or am I
> missing something?

Yes, but that's my fault, not yours. My static name checker is not
intended to work on attributes (including methods). Checking attributes
is inextricably tied to real *type checking*. In fact it is type
checking.

My assertion is that the first step is to statically check coherence
among Python's three (?) (function, module, builtin) runtime namespaces.
Until that nut is cracked, static *type* checking (and thus attribute
name checking) won't be possible.

Once we have name checking then we can design a syntax to statically
associate types with names. THEN we can do static type checking. I could
be wrong but it seems to me that once this is done, the definition of
swallow will be trivial: "A statically compilable Python module is a
file where every name is frozen and every name has a type declaration."

If you restrict yourself to that subset then you've essentially
re-invented Java. But of course the whole point (hi Gordon and Uche!) is
that you can choose WHEN to restrict yourself to that subset whereas
Java gives you no option...and neither does Perl. If Python is stuck[1]
between a rock (Perl) and a hard place (Java) then optional static type
checking is the dynamite that frees us up.

-- 
 Paul Prescod  - ISOGEN Consulting Engineer speaking for himself
Math -- that most logical of sciences -- teaches us that the truth can
be highly counterintuitive and that sense is hardly common.
	K.C.Cole, "The Universe and the Teacup"