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

Guido van Rossum guido at python.org
Mon Sep 5 13:40:55 EDT 2016

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)

More information about the Python-Dev mailing list