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

[Koos Zevenhoven]

On Sun, Sep 4, 2016 at 2:33 AM, Koos Zevenhoven <k7hoven at gmail.com> wrote:
> On Sun, Sep 4, 2016 at 2:22 AM, Chris Angelico <rosuav at gmail.com> wrote:
>> On Sun, Sep 4, 2016 at 7:44 AM, Koos Zevenhoven <k7hoven at gmail.com> wrote:
>>>> 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.
>>
>> I think you missed the sum() call there. Most likely, the sum of
>> List[Union[anything]] would be Union[anything], so these would all be
>> the same (which was my original point).
>>
>
> Oh, you're right, I missed the sum.
>
> Suitable @overloads in the stubs for sum should lead to that being
> inferred as Union[int, float]. But if the annotations are not that
> precise, that might become just List (or List[Any]), and the
> programmer may want to annotate x or improve the stubs.
>

Let me try explaining this once more. If list.__add__ is imprecisely
annotated, one may end up with just List or list. But the annotation
is not that complicated. In the stubs you might have

T1 = TypeVar('T1')
T2 = TypeVar('T2')

def __add__(self : List[T1], other : List[T2]) -> List[Union[T1,T2]]: ...

And sum is also implemented in c, so no inference there (unless stubs
can provide a reference Python implementation in the future, but I'm
not sure I want to propose that).

For sum, there could be an overload to handle this case:

@overload
def sum(iterable : Iterable[Union[int, float]], start : Union[int,
float] = 0) -> Union[int, float]: ...

In general the following is not strictly true:

đef sum(iterable : Iterable[T], start: T) -> T: ...

because sum uses __add__ which can return anything. However, the
counterexamples are probably very rare.

-- Koos


> -- Koos
>
>> ChrisA
>> _______________________________________________
>> Python-ideas mailing list
>> Python-ideas at python.org
>> https://mail.python.org/mailman/listinfo/python-ideas
>> Code of Conduct: http://python.org/psf/codeofconduct/
>
>
>
> --
> + Koos Zevenhoven + http://twitter.com/k7hoven +



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