[Types-sig] Type Inference I

[Tim Peters]

> ... the _expression_ x+1 can only be an integer, we _can_ deduce that

> ... You can't deduce/infer anything from x+1.

> ["Yes! No!" * 10 <wink>]

We can deduce that x+1 will blow up at runtime with a TypeError (perhaps
spelled by some other name <wink>) unless type(x) supports an __add__ method
which in turn accepts (at least, and besides self) a single argument of type
Int.

If type(x) does support an __add__ method which in turn etc, we have no idea
whether it will blow up at runtime.  But the current incarnation of the
Types-SIG (TCIOTTS) doesn't care about that:  it's trying (only!) to
determine at compile-time when it's certain that type(x) *does* support etc.
Toward that end, TCIOTTS assumes that type(x) and all relevant information
about type(x).__add__ has been handed to it on a silver platter.

The type of x+1 is the union of all the types that T.__add__(1) may return
across all types T in the set of possible types for x, and that info
constitutes the "silver platter" handed to x+1's context.  Bottom-up, all
the way, with oracles at the base.

AFAIK, TCIOTTS doesn't yet have an explicit policy about what to do in the
presence of try/except blocks.  Everyone has clearly assumed that, for
purposes of type-checking, the possibility of an *up*-level handler will be
ignored (and if a user can't live with that, fine, then they can't enable
type-checking).

Given that this SIG self-destructed the last time it tried to take on too
much, and currently has a goal to produce genuinely useful code in a matter
of months, I doubt TCIOTTS will be persuaded to move beyond that for now.

Indeed, I think it should forget inferencing *entirely* at the start, even
for cases like

def unity() -> Int:
    a = 1   # compile-time error in type-check mode -- a not declared
    return a

Inferencing (ya, ya -- *useful* inferencing) is harder than mere checking
(indeed, checking is easy enough to write in K&R C <wink>).

one-man's-opinion-ly y'rs  - tim