[Python-Dev] Please reject or postpone PEP 526

[Guido van Rossum]

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 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:
>
> * 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 _conforms_to_type(x: ANNOTATION): -> None
>         pass
>     _conforms_to_type(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)