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

[Koos Zevenhoven]

Below I respond to Chris Angelico's post in the python-dev thread.

On Sat, Sep 3, 2016 at 2:01 AM, Chris Angelico <rosuav at gmail.com> wrote:
>>>>
>>>> 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]
>>>
>
> 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.

In the first case it would indeed again be Union[int, float] (the code
is basically equivalent after all).

In the second case, the checker would infer List[Union[int, float]].
No magic involved, assuming that list.__add__ is annotated precisely
enough.

> 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.

Agreed. However, I think it completely depends on the context, which
types are "compatible" in the way that 1 and 1.5 often are. Numbers
are just a very typical example. But it could as well be Animal and
Person. It's just a matter of whether the code base is written in a
way that it's ok to pass on either type.

> 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.
>

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