Mailman 3 Semantics for type checking (was: What should a good type checker do?) - Python-ideas

3 Sep 2016

      On Friday, while replying to a post on python-dev about PEP 526
(variable annotations), I ended up mentioning things that I think a
good type checker should do, which seem to differ from the general
understanding. The discussion should continue here, though, because
the aim of PEP 526 is not to define type-checking semantics.

I'll recap the thoughts in this post, but here are links to the
original posts, for reference:
[1] https://mail.python.org/pipermail/python-dev/2016-September/146069.html
[2] https://mail.python.org/pipermail/python-dev/2016-September/146090.html

Quoting [1], with added explanations in between:

On Fri, Sep 2, 2016 at 1:10 PM, Koos Zevenhoven  wrote:
[...]
...
The more you infer types, the less you check them. It's up to the
programmers to choose the amount of annotation.
[...]
...
I'm also a little worried about not being able to reannotate a name.
IOW, this should be allowed:
x : int = 1
foo(x)
x : float = 0.5
bar(x)

It turns out that disallowing this was not the PEP's intention,
because type-checking semantics is up to the type checker. This has
now been clarified in the PEP. Good.

[...]
...
...
def eggs(cond:bool):
    x: Optional[List[int]]
    if cond:
        x = None # Now legal
    else:
        x: = []
    spam(x)
The above is an example from Mark Shannon's email, and below is my response:
...
A good checker should be able to infer that x is a union type at the
point that it's passed to spam, even without the type annotation. For
example:
def eggs(cond:bool):
    if cond:
        x = 1
    else:
        x = 1.5
    spam(x)   # a good type checker infers that x is of type Union[int, float]
Here, there are two inferred types for x, but in different branches of
the if statement. So x, which is dynamically typed at runtime, becomes
a Union at "static-check time".
...
Or with annotations:
def eggs(cond:bool):
    if cond:
        x : int = foo() # foo may not have a return type hint
    else:
        x : float = bar() # bar may not have a return type hint
    spam(x)   # a good type checker infers that x is of type Union[int, float]
Two explicit annotations, and again neither of them "wins". The
inferred type after the if statement is therefore a Union.

Below, I'm quoting [2], my response to an email that disagreed with me
about the above being something "a good type checker" would do:

On Fri, Sep 2, 2016 at 6:49 PM, Koos Zevenhoven  wrote:
...
...
...
A good checker should be able to infer that x is a union type at the
point that it's passed to spam, even without the type annotation. For
example:
def eggs(cond:bool):
    if cond:
        x = 1
    else:
        x = 1.5
    spam(x)   # a good type checker infers that x is of type Union[int, float]
Oh I really hope not. I wouldn't call that a *good* type checker. I
would call that a type checker that is overly permissive.
I guess it's perfectly fine if we disagree about type checking ideals,
and I can imagine the justification for you thinking that way. There
can also be different type checkers, and which can have different
modes.
But assume (a) that the above function is perfectly working code, and
spam(...) accepts Union[int, float]. Why would I want the type checker
to complain?
Then again, (b) instead of that being working code, it might be an
error and spam only takes float. No problem, the type checker will
catch that.
In case of (b), to get the behavior you want (but in my hypothetical
semantics), this could be annotated as
def eggs(cond:bool):
    x : float
    if cond:
        x = 1  # type checker says error
    else:
        x = 1.5
    spam(x)
So here the programmer thinks the type of x should be more constrained
than what spam(...) accepts.
The reasoning here is that x is explicitly annotated without an
assignment, so the inferred types subsequently assigned to it (int and
float) must be compatible with the annotation. Therefore "the good
type checker" would say assigning 1 is an error.
...
Or you might have something like this
def eggs(cond:bool):
    if cond:
        x = 1
    else:
        x = 1.5
    # type checker has inferred x to be Union[int, float]
    x : float  # type checker finds an error
    spam(x)
Here, the same error is found, but at a different location.
Here, x is explicitly annotated as float while its value remains a
Union[int, float], as inferred by "the good type checker". Therefore
this is an error. One could consider this a type assertation (at
static-check time).

"The good type checker" should also be able to tell the programmer
that it's "x = 1" that made the subsequent "type assertion" fail.

In addition to being type *hints*, the annotations can also be
considered as "check points".

-- Koos

-- 
+ Koos Zevenhoven + http://twitter.com/k7hoven +

Semantics for type checking (was: What should a good type checker do?)

Koos Zevenhoven

Koos Zevenhoven

Chris Angelico

Koos Zevenhoven

Koos Zevenhoven

Steven D'Aprano

Koos Zevenhoven

tags

participants (3)