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

[Koos Zevenhoven]

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 <k7hoven at gmail.com> 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 <k7hoven at gmail.com> 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 +