[Types-sig] Static name checking

[Martijn Faassen]

Paul Prescod wrote:
> 
> 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.

What about classes referring to attributes of 'self', for instance,
though? I'm still not entirely clear on what you're trying to
accomplish, I'm afraid.

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

And every imported module has the same properties, including this one.
Though of course you may mean this with 'every name'. I don't think
it'll be that trivial, as you haven't defined 'type declaration'; you
run into complexities here, 
especially if you involve classes and objects.

Can't you go about it the other way around? First, you make a type
declaration for
all names in a module. Then you check (somehow) if there isn't code that
contradicts this type definition; that is, there should be no
assignments of one name to another that violates the static type
definitions, no attribute accesses to undefined attributes, and so on.
Of course you instantly produce errors if any name doesn't have a type
definition.

I don't see how your frozen idea helps a lot in this. A possible
intermediate drop-off point resembling frozen may simply a checker that
determines if all names in a module are known to the static type system,
without actually defining these types, though you run into trouble here
with attribute accesses.

The real hard part is the construction of the type checker. Somewhat
easier is the definition of a generic type system. I'm still proposing
to use standard Python objects such as dictionaries and tuples to define
these types in, initially. Later on we can look at syntax, but you can
get the type checker going without any syntax extensions. Another
prerequisite for a type checker is the determination of the Swallow
subset. For instance one can imagine that in Swallow it's illegal to
import modules except on the top. I imagine these limitations will
become more obvious after a type system has been developed.

I have two possible approaches for the type checker in mind currently
that leverage current Python; one is an AST based type checker, and
another is a bytecode based typechecker. I'm not sure which one would be
easier as I don't know enough about either Python's ASTs or bytecodes,
but in the happy abstract space of insufficient information I can wrap
my mind better around a bytecode based checker than around an AST based
checker. There are bytecodes for assignment and attribute access and the
various other operations that need the scrutity of a type checker. For
each such bytecode you'd need to write a type check. Checking a module
is then going through all bytecodes of the module to see if they do
legal things.

As an aside, another task would be the writing of an interface layer
between swallowed modules and non swallowed ones. Any name that enters a
swallowed module should have a static type description associated with
it. A run-time layer can check whether each python object that is sent
into Swallow conforms to the type definitions; a function expecting an
int must indeed be sent an int object. If not, somekind of exception
should be raised. 

Calling non-swallow modules from a Swallow module is more tricky, but
again the Swallowed module provides types definitions for any name used
in it, so it should provide interface definitions for any non-Swallow
function used in a Swallowed module as well. So you can make run-time
type checks on that interface as well. But I'm sure I'm missing a lot of
subtleties here. :)

Regards,

Martijn