[Python-Dev] Please reject or postpone PEP 526 (original) (raw)
Guido van Rossum guido at python.org
Mon Sep 5 14:15:17 EDT 2016
- Previous message (by thread): [Python-Dev] Please reject or postpone PEP 526
- Next message (by thread): [Python-Dev] Please reject or postpone PEP 526
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
On Mon, Sep 5, 2016 at 10:24 AM, Ethan Furman <ethan at stoneleaf.us> wrote:
On 09/05/2016 06:46 AM, Nick Coghlan wrote:
[an easy to understand explanation for those of us who aren't type-inferring gurus] Thanks, Nick. I think I finally have a grip on what Mark was talking about, and about how these things should work. Much appreciated!
There must be some misunderstanding. The message from Nick with that
timestamp (https://mail.python.org/pipermail/python-dev/2016-September/146200.html)
hinges on an incorrect understanding of the intention of annotations
without value (e.g. x: Optional[int]), leading to a -1 on the PEP.
I can't tell if this is an honest misunderstanding or a strawman, but I want to set the intention straight.
First of all, the PEP does not require the type checker to interpret anything in a particular way; it intentionally shies away from prescribing semantics (other than the runtime semantics of updating annotations or verifying that the target appears assignable).
But there appears considerable fear about what expectations the PEP has of a reasonable type checker. In response to this I'll try to sketch how I think this should be implemented in mypy.
There are actually at least two separate cases: if x is a local
variable, the intention of x: <type> is quite different from when x
occurs in a class.
When found in a class, all uses (which may appear in modules far away from the definition) must be considered to conform to the stated type -- as must all assignments to it, but I believe that's never been in doubt. There are just too many edge cases to consider to make stricter assumptions (e.g. threading, exceptions, signals), so that even after seeing
self.x = 42; use(self.x)the call to use() cannot assume that self.x is still 42.But when found inside a function referring to a local variable, mypy should treat the annotation as a restriction on assignment, and use its own inference engine to type-check uses of that variable. So that in this example (after Mark's):
def bar() -> Optional[int]: ...
def foo() -> int: x: Optional[int] x = bar() if x is None: return -1 return x
there should not be an error on return x because mypy is smart
enough to know it cannot be None at that point.
I am at a loss how to modify the PEP to avoid this misunderstanding, since it appears it is entirely in the reader's mind. The PEP is not a tutorial but a spec for the implementation, and as a spec it is quite clear that it leaves the type-checking semantics up to individual type checkers. And I think that is the right thing to do -- in practice there are many other ways to write the above example, and mypy will understand some of them, but not others, while other type checkers may understand a different subset of examples. I can't possibly prescribe how type checkers should behave in each case -- I can't even tell which cases are important to distinguish.
So writing down "the type checker should not report an error in the following case" in the PEP is not going to be helpful for anyone (in contrast, I think discussing examples on a mailing list is useful). Like a linter, a type checker has limited intelligence, and it will be a quality of implementation issue as to how useful a type checker will be in practice. But that's not the topic of PEP 526.
-- --Guido van Rossum (python.org/~guido)
- Previous message (by thread): [Python-Dev] Please reject or postpone PEP 526
- Next message (by thread): [Python-Dev] Please reject or postpone PEP 526
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]