[Types-sig] Implementability

[Tim Peters]

[Tim]
> making this [global type inference] all run efficiently (in either
> time or space) is a Professional Pain in the Professional Ass.

[Paul Prescod]
> According to the principle of "from each according to their
> talents"

I'm afraid you've mistaken Benevolent Dictatorship for some variant of
Communism <wink>.

> you should be writing this optimizing, static type checker.

Guido is the one interested in magical type inference; I'm not.  I'm happy
to explicitly declare the snot out of everything when I want something from
static typing.  Merely checking that my declared types match my usage is
much easier (doesn't require any flow analysis).  The good news is that I
couldn't make time to write an inferencer even if I wanted to; if I had
time, I'd be much more likely to write something that *used* explicit
declarations to generate faster code.

>> Because of this, global analysis never works out in practice
>> unless you invent an efficient database format to cache the
>> results of analysis, keeping that in synch with the source
>> base under mutation.

> Bah. The scope of compilation is the module. The scope of inference is
> a namespace defining suite (e.g. a module, class body or method, but
> not an "if" or "try").

"Bah"?  I didn't say anything about the granularity of the cached analysis.
For general Python use, module level sounds good to me too.  But note that
in the msg I was responding to, Guido was blue-skying a type checker for
IDLE:  for interactive use, he'll probably want quicker feedback than that
(if a newbie breaks the type correctness of an "if" test with an edit, they
should probably be told about it as soon as they move the cursor off the
line!).

>> ...
>> If you can, in addition, avoid needing to deduce the types of
>> most globals, it could actually fly before we're all dead <wink>.

> The types of globals from other modules should be explicitly declared.

A global type inferencer can usually figure that out on its own.  There's
more than one issue being discussed here, alas -- blame Guido <0.9 wink>.

> If they aren't, they are presumed to have type PyObject or to return
> PyObject. Or they just aren't available if you are in strict static
> type check mode.

In the language of the msg to which you're replying, they're associated with
the universal set (the set of all types) -- same thing.  Then e.g.

    declared_int = unknown

is an error, but

    unknown1 = unknown2

is not.  Whether

    unknown = declared_int

should be an error is a policy issue.  Many will claim it should be an
error, but the correct answer <wink> is that it should not.  Types form a
lattice, in which "unknown" is the top element, and the basic rule of type
checking is that the binding

    lhs = rhs

is OK iff

    type(lhs) >= type(rhs)

where ">=" is wrt the partial ordering defined by the type lattice (or, in
English <wink>, only "widening" bindings are OK; like assigning an int to a
real, or a subclass to a base class etc, but not their converses).

phrase-it-that-way-or-not-you-end-up-with-the-same-rules-ly y'rs  - tim