Overload type hinting for empty sequences?

Typing
1

Based on the empty list type hinting discussion in How to annotate empty containers? · Issue #157 · python/typing · GitHub I hoped to be able to overload a function to indicate that only an empty input sequence could produce a None result (so if an explicitly non-empty sequence was passed in, the result would be known not to be None):

    @overload
    def add_elements(
        self, elements: Sequence[Never]
    ) -> None:
        ...
    @overload
    def add_elements(
        self, elements: Sequence[ElementInput]
    ) -> ElementData:
        ...
    def add_elements(
        self, elements: Sequence[ElementInput]
    ) -> ElementData | None:
        if not elements:
            return None
        ... actual produce and record the element data instance

The above doesn’t work (with the order shown, MyPy complains that the first two entries overlap with incompatible return types instead of always using the first option for the empty list case, while with the first two elements flipped, it complains that the Sequence[Never] option will never be matched).

Without this, even consuming code that passes in an explicitly non-empty sequence still needs to assert that the result won’t be None to keep the typechecker from complaining:

    def add_element(
        self, element: ElementInput
    ) -> ElementData:
        result = self.add_element([element])
        assert result is not None
        return result

I know I could make passing in an empty sequence an error and eliminate the None return outcome that way, but the current behaviour is useful for accepting optional elements in various places (the “add” operation simply does nothing if the sequence is empty, so the callers don’t need to check for that case themselves).

2

I don’t think this approach is going to be fruitful. The type system has a very limited ability of tracking whether a collection/sequence is empty or not - by design, since this is a question of values, not types.

2 Likes
3

The overload would be unsound.

l: list[ElementInput] = []
# both should be inferred as same
l = list[ElementInput]()

result = add_elements(l)
reveal_type(result)  # ElementData
assert result is not None  # error
1 Like
4

Summarising the problem (and the reason the overload ordering changes the error message):

  • Sequence[Never] is necessarily empty, since no value can match Never
  • however, there is no practical way to exclude the empty case for Sequence[ElementInput], thus the complaints about the overlap between the two signatures

I don’t need this badly enough to advocate for it (I was mostly curious if I had missed something), but I’ll note that it’s theoretically possible to model sequences as a union between the empty sequence and a non-empty sequence of the given element type (discriminated by boolean value checks in the code structure).

I doubt it would be worth ever actually doing that, though (as noted above, it blurs the boundary between type checking and value checking).

5

The tuple type includes length information in its annotation so you could include explicit overloads for the tuple case where the length is known:

from typing import overload, assert_type, Any

@overload
def foo(arg: tuple[()]) -> None:
    ...

@overload
def foo[T](arg: tuple[T, *tuple[T, ...]]) -> str:
    ...
@overload
def foo[T](arg: tuple[T, ...]) -> str | None:
    ...

def foo(arg: tuple[Any, ...]) -> str | None:
    ...

def bar[T](unk_arg: tuple[object, ...], e_arg: tuple[()], ne_arg: tuple[T, *tuple[T, ...]]) -> None:
    assert_type(foo(e_arg), None)
    assert_type(foo(unk_arg), str | None)
    assert_type(foo(ne_arg), str)

Working in MyPy and Pyright

2 Likes
6

In my particular case, I subsequently realised a slight tweak to the implementation would let it accept Iterable instead of only Sequence, so directly checking for the non-empty case is even further from plausible than it was originally.

The tuple overload approach technically still applies, though (zero-length tuple → None, non-empty tuple → expected result type, any other iterable → optional expected result type).

I also realised that even in my original example, the overloads would be more code than the extra assertion (since there was only one place where that assertion was needed).

1 Like