[Python-Dev] Do PEP 526 type declarations define the types of variables or not?

[Guido van Rossum]

On Tue, Sep 6, 2016 at 8:25 AM, Mark Shannon <mark at hotpy.org> wrote:
> The "smartness" of checkers is not the problem (for this example, at least)
> the problem is that checkers must conform to the rules laid down in PEP 484
> and (in whatever form it finally takes) PEP 526.
> It sounds like mypy doesn't conform to PEP 526, as it ignoring the declared
> type of x and using the inferred type.
> In fact it looks as if it is doing exactly what I proposed, which is that
> the annotation describes the type of the expression, not the variable.

IMO neither PEP requires type checkers to behave this way. Maybe you
read it between the lines when you reviewed PEP 484 and neither of us
realized that we were interpreting the text differently? The words you
have quoted previously mean different things to me than you seem to
imply.

>> I guess this is a surprise if you think of type systems like Java's
>> where the compiler forgets what it has learned, at least from the
>> language spec's POV. But a Python type checker is more like a linter,
>> and false positives (complaints about valid code) are much more
>> problematic than false negatives (passing invalid code).

> The language of PEP 526 is strongly suggestive of a type system like Java.

That suggestion is really in your mind. The PEP also quite clearly
states that it does not specify what a type checker should do with the
"declarations".

> The extensive use of the term 'variable' rather than 'expression' and
> 'assignment' rather suggests that all definitions and uses of a single
> variable have the same type.

Maybe you believe that Python's use of the word 'variable', combined
with using `=` for assignment, also implies that Python's "variables"
should behave like Java's "variables"?

> The problem with using the term "variable" is that it is *not* vague.
> Variables in python have well defined scopes and lifetimes.

So? When a type checker can prove that in the expression `f(x)`, the
type of the *expression* `x` will be compatible with the argument type
expected by f, isn't that good enough? Why would the type given for
the *variable* `x` have to be the only input to the type check for
that expression?

-- 
--Guido van Rossum (python.org/~guido)