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 <k7ho...@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 <k7ho...@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 + _______________________________________________ Python-ideas mailing list Python-ideas@python.org https://mail.python.org/mailman/listinfo/python-ideas Code of Conduct: http://python.org/psf/codeofconduct/
