[Python-Dev] Please reject or postpone PEP 526 (original) (raw)

Nick Coghlan ncoghlan at gmail.com
Mon Sep 5 23:46:29 EDT 2016

On 6 September 2016 at 04:15, Guido van Rossum <guido at python.org> wrote:

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.

Short version of below: after sleeping on it, I'd be OK with the PEP again if it just added the explicit type assertions, such that the shorthand notation could be described in those terms.

Specifically, "x: T = expr" would be syntactic sugar for:

x = expr
assert x: T

While the bare "x: T" would be syntactic sugar for:

assert all(x): T

which in turn would imply that all future bindings of that assignment target should be accompanied by a type assertion (and typecheckers may differ in how they define "all future bindings").

Even if everyone always writes the short forms, the explicit assertions become a useful aid in explaining what those short forms mean.

The main exploratory question pushed back to the typechecking community to answer by 3.7 would then be to resolve precisely what "assert all(TARGET): ANNOTATION" means for different kinds of target and for different scopes (e.g. constraining nonlocal name rebindings in closures, constraining attribute rebinding in modules, classes, and instances).

I can't tell if this is an honest misunderstanding or a strawman, but I want to set the intention straight.

I'm pretty sure I understand your intentions (and broadly agree with them), I just also agree with Mark that people are going to need some pretty strong hints that these are not Java/C/C++/C# style type declarations, and am suggesting a different way of getting there by being more prescriptive about your intended semantics.

Specifically:

Folks are already comfortable with the notion of assertions not necessarily being executed at runtime, and they're also comfortable with them as a way of doing embedded correctness testing inline with the code.

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

Unfortunately, the ordering problem the PEP introduces means it pushes very heavily in a particular direction, such that I think we're going to be better off if you actually specify draft semantics in the PEP (in terms of existing PEP 484 annotations), rather than leaving it completely open to interpretation. It's still provisional so you can change your mind later, but the notion of describing a not yet bound name is novel enough that I think more guidance (even if it's provisional) is needed here than was needed in the case of function annotations.

(I realise you already understand most of the background I go through below - I'm spelling out my reasoning so you can hopefully figure out where I'm diverging from your point of view)

If we look at PEP 484, all uses of annotations exist between two pieces of code: one that produces a value, and one that binds the value to a reference.

As such, they act as type assertions:

Typecheckers can then use those assertions in two ways: as a constraint on the value producer, and as a more precise hint if type inference either isn't possible (e.g. function parameters, initialisation to None), or gives an overly broad answer (e.g empty containers)

The "x: T = expr" syntax is entirely conformant with that system - all it does is change the spelling of the existing type hint comments.

Allowing "assert x: T" would permit that existing kind of type assertion to be inserted at arbitrary points in the code without otherwise affecting control flow or type inference, as if you had written:

 # PEP 484
 def is_T(arg: T) -> None:
     pass

is_T(x)

Or:

# PEP 526
x: T = x

By contrast, bare annotations on new assignment targets without an initialiser can't be interpreted that way, as there is no preceding value to constrain.

That inability to interpret them in the same sense as existing annotations means that there's really only one plausible way to interpret them if a typechecker is going to help ensure that the type assertion is actually true in a given codebase: as a constraint on future bindings to that particular target.

Typecheckers may differ in how they enforce that constraint, and how the declared constraint influences the type inference process, but that "explicit declaration of implicit future type assertions" is core to the notion of bare variable annotations making any sense at all.

That's a genuinely new concept to introduce into the language, and the PEP quite clearly intends bare annotations to be used that way given its discussion of class invariants and the distinction between instance variables with a class level default and class variables that shouldn't be shadowed on instances.

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.

This is where I think the "assert all(x): T" notation is useful, as it changes that core semantic question to "What does 'all' mean for a type assertion?"

Based on your stated intentions for mypy, it provisionally means:

Both initialised and bare variable annotations can then be defined as syntactic sugar for explicit type assertions:

# Initialised annotation
x: T = expr

x = expr
assert x: T # Equivalent type assertion

# Bare annotation
x: T
x = expr

assert all(x): T # Equivalent type assertion
x = expr
assert x: T # Assertion implied by all(x) above

(A full expansion would also show setting annotations, but that's not my main concern here)

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.

Providing an easier path to decomposing the new syntax into pre-existing PEP 484 semantics would definitely help me, and I suspect it would help other folks as well.

Recapping:

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

Yeah, I've come around to agreeing with you on that point.

Cheers, Nick.

-- Nick Coghlan | ncoghlan at gmail.com | Brisbane, Australia

More information about the Python-Dev mailing list