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

Guido van Rossum guido at python.org
Tue Sep 6 00:04:59 EDT 2016

I'm sorry, but we're not going to invent new syntax this late in the game. The syntax proposed by the PEP has been on my mind ever since PEP 484 with very minor variations; I first proposed it seriously on python-ideas over a month ago, we've been debating the details since then, and it's got a solid implementation based on those debates by Ivan Levkivskyi. In contrast, it looks like you just made the "assert x: T" syntax up last night in response to the worries expressed by Mark Shannon, and "assert" sounds a lot like a run-time constraint to me.

Instead, I encourage you to participate in the writing of a separate PEP explaining how type checkers are expected to work (since PEP 526 doesn't specify that). Ivan is also interested in such a PEP and we hope Mark will also lend us his expertise.

On Mon, Sep 5, 2016 at 8:46 PM, Nick Coghlan <ncoghlan at gmail.com> wrote:

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: * for 3.6, push everything into a new form of assert statement and define those assertions as syntactic sugar for PEP 484 constructs * for 3.7 (and provisionally in 3.6), consider blessing some of those assertions with the bare annotation syntax 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: - on parameters, they assert "I am expecting this argument to be of this type" - on assignments, they assert "I an expecting this initialiser to be of this type" 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 isT(arg: T) -> None: pass isT(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: * for a local variable, "all future bindings in the current scope". * for a class or module variable, "all future bindings in the current scope, and all future bindings via attribute access". 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: * Introduce "assert TARGET: ANNOTATION" as a new noop-at-runtime syntactic primitive that typechecks as semantically equivalent to: def conformstotype(x: ANNOTATION): -> None pass conformstotype(TARGET) * Introduce "assert all(TARGET): ANNOTATION" as a way to declaratively annotate future assignments to a particular target * Define variable annotations in terms of those two new primitives * Make it clear that there's currently still room for semantic variation between typecheckers in defining precisely what "assert all(TARGET): ANNOTATION" means 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

-- --Guido van Rossum (python.org/~guido)

More information about the Python-Dev mailing list