[Python-Dev] Please reject or postpone PEP 526

[Guido van Rossum]

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)