[Python-Dev] Please reject or postpone PEP 526

[Nick Coghlan]

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