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

[Guido van Rossum]

On Mon, Sep 5, 2016 at 8:26 AM, Mark Shannon <mark at hotpy.org> wrote:
> PEP 526 states that "This PEP aims at adding syntax to Python for annotating
> the types of variables" and Guido seems quite insistent that the
> declarations are for the types of variables.
>
> However, I get the impression that most (all) of the authors and proponents
> of PEP 526 are quite keen to emphasise that the PEP in no way limits type
> checkers from doing what they want.
>
> This is rather contradictory. The behaviour of a typechecker is defined by
> the typesystem that it implements. Whether a type annotation determines the
> type of a variable or an expression alters changes what typesystems are
> feasible. So, stating that annotations define the type of variables *does*
> limit what a typechecker can or cannot do.
>
> Unless of course, others may have a different idea of what the "type of a
> variable" means.
> To me, it means it means that for all assignments `var = expr`
> the type of `expr` must be a subtype of the variable,
> and for all uses of var, the type of the use is the same as the type of the
> variable.
>
> In this example:
>
>     def bar()->Optional[int]: ...
>
>     def foo()->int:
>         x:Optional[int] = bar()
>         if x is None:
>             return -1
>         return x
>
> According to PEP 526 the annotation `x:Optional[int]`
> means that the *variable* `x` has the type `Optional[int]`.
> So what is the type of `x` in `return x`?
> If it is `Optional[int]`, then a type checker is obliged to reject this
> code. If it is `int` then what does "type of a variable" actually mean,
> and why aren't the other uses of `x` int as well?

Oh, there is definitely a problem here if you interpret it that way.
Of course I assume that other type checkers are at least as smart as
mypy. :-) In mypy, the analysis of this example narrows the type x can
have once `x is None` is determined to be false, so that the example
passes.

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

So a Python type checker that is to gain acceptance of users must be
much smarter than that, and neither PEP 484 not PEP 526 is meant to
require a type checker to complain about `return x` in the above
example.

I'm not sure how to change the language of the PEP though -- do you
have a suggestion? It all seems to depend on how the reader interprets
the meaning of very vague words like "variable" and "type".

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