[Python-Dev] What should a good type checker do? (was: Please reject or postpone PEP 526)

[Chris Angelico]

On Sat, Sep 3, 2016 at 8:49 AM, Koos Zevenhoven <k7hoven at gmail.com> wrote:
> On Fri, Sep 2, 2016 at 9:04 PM, Steven D'Aprano <steve at pearwood.info> wrote:
>> On Fri, Sep 02, 2016 at 08:10:24PM +0300, 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?

I wonder if it would be different if you wrote that as a single expression:

x = 1 if cond else 1.5

x = sum([1] + [0.5] * cond)

What should type inference decide x is in these cases? Assume an
arbitrarily smart type checker that can implement your ideal; it's
equally plausible to pretend that the type checker can recognize an
if/else block (or even if/elif/else tree of arbitrary length) as a
single "assignment" operation. IMO both of these examples - and by
extension, the if/else of the original - should be assigning a Union
type. Lots of Python code assumes that smallish integers [1] are
entirely compatible with floats. Is Python 4 going to have to deal
with the int/float distinction the way Python 3 did for bytes/text, or
are they fundamentally compatible concepts? Is the "small integer"
like the "ASCII byte/character" as a kind of hybrid beast that people
treat as simultaneously two types? (Personally, I don't think it's
anything like bytes/text. But I'm open to argument.)

Forcing people to write 1.0 just to be compatible with 1.5 will cause
a lot of annoyance. I leave it to you to decide whether there's a
fundamental difference that needs to be acknowledged, or just
subtleties of representational limitations to be ignored until they
become a problem.

ChrisA

[1] And by "smallish" I mean less than 2**53. Big enough for a lot of
purposes. Bigger (by definition) than JavaScript's integers, which cap
out at 2**32.