[Python-Dev] Please reject or postpone PEP 526

[Nick Coghlan]

On 4 September 2016 at 21:51, Steven D'Aprano <steve at pearwood.info> wrote:
> On Sun, Sep 04, 2016 at 12:31:26PM +0100, Mark Shannon wrote:
>
>> In other words PEP 484 specifically states that annotations are to help
>> with type inference. As defined in PEP 526, I think that type
>> annotations become a hindrance to type inference.
>
> I'm pretty sure that they don't.
>
> Have you used any languages with type inference? Any type-checkers? If
> so, can you give some actual concrete examples of how annotating a
> variable hinders type inference? It sounds like you are spreading FUD at
> the moment.

Steven, this kind of credential checking is uncalled for - Mark is
significantly more qualified than most of us to comment on this topic,
since he actually works on a shipping software quality analysis
product that does type inference on Python code (hence
https://semmle.com/semmle-analysis-now-includes-python/ ), and was
nominated as the BDFL-Delegate for PEP 484 because Guido trusted him
to critically review the proposal and keep any insurmountable problems
from getting through.

Getting accused of spreading FUD when a topic is just plain hard to
explain (due to the large expert/novice gap that needs to be bridged)
is one of the reasons python-dev and python-ideas can end up feeling
hostile to domain experts. We have the SIG system to help mitigate
that problem, but it's vastly preferable if such folks also feel their
expertise is welcomed on the main lists, rather than having it be
rejected as an inconvenient complication.

> The whole point of type annotations is that you use them to deliberately
> over-ride what the checker would infer (if it infers the wrong thing, or
> cannot infer anything). I cannot see how you conclude from this that
> type annotations will be a hindrance to type inference.

The problem arises for the "bare annotation" case, as that looks a
*lot* like traditional declarations in languages where initialisation
(which can specify a type) and assignment (which can't) are different
operations.

Consider this case:

    if arg is not None:
        x = list(arg)
        # Type of "x" is inferred as List[Any] or something more specific here
        if other_arg is not None:
            # This is fine, we know "x" is a list at this point
            x.extend(other_arg)
    else:
        x = None
        # Type of "x" is inferred as type(None) here
    # Type of "x" is inferred as Optional[List[Any]] from here on out

Now, consider that case with PEP 526:

    x: Optional[List[Any]]
    # Oops, this is the type of "x" *after* the if statement, not *during* it
    if arg is not None:
        x = list(arg)
        if other_arg is not None:
            # If we believe the type declaration here, this code will
(incorrectly) be flagged
            # (as None has no "extend" method)
            x.extend(other_arg)
    else:
        x = None

The "pre-declaration as documentation" proposal turns out to be
problematic in this case, as it misses the fact that different
branches of the if statement contribute different types to what
ultimately becomes a Union type for the rest of the code.

In order to cover the entire code block, we have to make the
pre-declaration match the state after the if statement, but then it's
overly broad for any *particular* branch.

So in this case, attempting to entirely defer specification of the
semantics creates a significant risk of type checkers written on the
assumption of C++ or Java style type declarations actively inhibiting
the dynamism of Python code, suggesting that the PEP would be well
advised to declare not only that the PEP 484 semantics are unchanged,
but also that a typechecker that flags the example above as unsafe is
wrong to do so.

Cheers,
Nick.

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