On 05/09/16 18:40, Guido van Rossum wrote:
On Mon, Sep 5, 2016 at 8:26 AM, Mark Shannon <m...@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.
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.
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. 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.
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".
The problem with using the term "variable" is that it is *not* vague.
Variables in python have well defined scopes and lifetimes.
Cheers,
Mark.
_______________________________________________
Python-Dev mailing list
Python-Dev@python.org
https://mail.python.org/mailman/listinfo/python-dev
Unsubscribe:
https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com
