python / typing

Python static typing home. Hosts the documentation and a user help forum.
https://typing.readthedocs.io/
Other
1.6k stars 234 forks source link

Union of empty tuple should return `Never` #1362

Closed randolf-scholz closed 9 months ago

randolf-scholz commented 1 year ago

It is mathematically consistent to have an empty union be equal to the Never-type. Currently, Union[()] raises

TypeError: Cannot take a Union of no types.

Never is the singular correct value to assign to empty union types, essentially since in set-theory the empty union is the empty set, but it also matches well with intuition:

def foo(x: str | int | float) -> ...:
    # x ≤ Union[str, int, float]
    if isinstance(x, str):
        return ...
    # x ≤ Union[int, float]
    if isinstance(x, float):
        return ...
    # x ≤ Union[int] = int
    if isinstance(x, int):
        return ...
    # x ≤ Union[] = Never
    raise TypeError(...)  # unreachable
JelleZijlstra commented 1 year ago

We already have two ways to spell the bottom type, NoReturn and Never. Why should we add a third?

randolf-scholz commented 1 year ago

Internal consistency of the union type. Same reason why sum([]) should return 0 and math.prod([]) returns 1.

randolf-scholz commented 1 year ago

There might also be some interactions with TypeVarTuple when the tuple is empty

from typing import TypeVarTuple, Union

Items = TypeVarTuple('Items')

class MyTuple(Generic[*Items]): 
   def random_element(self) -> Union[*Items]: ...

x = MyTuple([])
y = x.random_element()  # Type Checker should return Union[()] = Never
erictraut commented 1 year ago

When a type is narrowed to include no subtypes, the resulting type is Never, which is a synonym for NoReturn. I agree with Jelle that there's no need to introduce a third way to express this concept. If you really want to use a Union to express Never, you could use Union[*tuple[()]].

randolf-scholz commented 1 year ago

I wouldn't expect anyone to manually type this, to be honest. That would be equally weird as seeing sum([]) or math.prod([]) explicitly spelled out in code. Again it's more of a consistency thing. On the flipside - since we have the Never type, why shouldn't Union[()] just return Never? It just makes sense that it would.

erictraut commented 1 year ago

What do you mean by "return Never"? Union[()] isn't a function, so it doesn't return anything. Are you saying that you want Union[()] to be a valid expression form that can be used in a type annotation, and you want type checkers to treat it the same as Never?

If you don't expect anyone to type Union[()], then why do you care how that expression will be evaluated?

carljm commented 1 year ago

I suppose the example with TypeVarTuple is the best motivating example here. I don't see how type checkers would reasonably handle this other than to resolve the empty union to Never.

I agree that there's no particular value to permitting the explicit spelling Union[()].

hauntsaninja commented 1 year ago

See also https://github.com/python/mypy/issues/9998

randolf-scholz commented 1 year ago

If you don't expect anyone to type Union[()], then why do you care how that expression will be evaluated?

I'm not sure what to tell you other than that it feels awkward and incomplete that mathematical edge cases are not included. To me it seems analogous to asking why sum should support an empty iterable. Well, it's just that sum([])==0 is the only definition possible that is consistent with its algebraic properties. Why does it matter if anyone needs it? Looking at it from the other way around: are there any good reasons to raise a TypeError when Never is the singular value which is consistent with the Union-Type properties? Why raise an unnecessary error?

But I could imagine that it could come into play when dynamically generating code, for example.

NeilGirdhar commented 1 year ago

Isn't Union on its way towards deprecation? Many linters flag you to stop using and some automatically replace Union with |. This problem will disappear on its own.

randolf-scholz commented 9 months ago

Seems like mypy recognizes this in static analysis post version 1.7.0. Still gives a TypeError at runtime though.

from typing import reveal_type, Union

def foo(x: Union[()]):
    reveal_type(x)  # <Never> for mypy≥1.70 else <nothing>

https://mypy-play.net/?mypy=1.7.0&python=3.12&gist=bf95a7501e0453e68b8a99d1ce129ae3

gvanrossum commented 9 months ago

Why reopen? If you want it changed at runtime that's an issue for the cpython repo.

erictraut commented 9 months ago

Also, this would require a change to the typing spec — one that I would personally not be in favor of. I don't think you've made a compelling case for it. The current typing spec (and conformant test suite) disallow this usage.

randolf-scholz commented 9 months ago

@erictraut I suppose as long as Union can be combined with TypeVarTuple it shouldn't come up. Although it seems like this is not supported by either mypy or pyright at the moment. (playground)

from typing import Union, Never, TypeVarTuple, assert_type
import random

Ts = TypeVarTuple("Ts")

def rng(*elements: *Ts) -> Union[*Ts]:  # Union cannot include unpacked TypeVarTuple
    return random.choice(elements)

x: bool = True
y: int = 1
z: str = "1"

assert_type(rng(x, y, z), bool | int | str)
assert_type(rng(x, y), bool | int)
assert_type(rng(x), bool)
assert_type(rng(), Never)

Do you think this is a type-checker issue, or does it belong to this repo?

erictraut commented 9 months ago

The notation Union[*Ts] was described in an early draft of PEP 646, but it was removed from the draft that was accepted. I recently removed support for it (or rather put it behind the enableExperimentalFeatures flag) in pyright since it's not part of the official typing spec. There is a discussion about formally adding it. If you're in favor of that, please post your thoughts there.