Annotating exhaustiveness of if-elif and match
Hello, currently when people want to annotate that a if-elif check should be exhaustive and have a type-checker like mypy verify the exhaustiveness they have to resort to a clever hack that looks like this (This works in mypy. I haven't verified any other type-checkers): ```| from typing import NoReturn | |def assert_never(x: NoReturn) -> NoReturn: raise AssertionError(f"Invalid value: {x!r}") from typing import Union def type_checking_ok(foo: Union[str, int]) -> None: if isinstance(foo, str): print("str") elif isinstance(foo, int): print("int") else: assert_never(foo) def type_checking_ko(foo: Union[str, int]) -> None: if isinstance(foo, str): print("str") else: assert_never(foo) ``` This works by abusing the fact that mypy doesn't typecheck unreachable code and assert_never can't be called by a valid function call (*except for corner cases I will discuss later). Mypy also won't report it as unreachable if it is unreachable, as it returns `NoReturn`. If it can be reached mypy will complain about incompatible parameter types. This has a few problems: * It can be broken by `Any`. For example if `foo` is of type `Union[int, Any]` and you only check for `int` mypy won't show an error * According to PEP 484 `NoReturn` is only valid as a return type and should be considered an error if it appears in any other positions. * Some type-checkers might report the error, even if it is unreachable This is used in the wild for example by pytest. Due to python 3.10 introducing the match statement there will probably also be renewed interest in checking exhaustiveness. Therefor I would really like to see an official way to annotate this. There have already been discussions. There have already been multiple discussions of this topic on both the mypy github and the typing github: https://github.com/python/typing/issues/735 https://github.com/python/mypy/issues/5818 (https://github.com/python/mypy/issues/9748) Discussed solutions/improvements include: * Changing how `Any` and `NoReturn` interact https://github.com/python/mypy/issues/3194 * Changing PEP 484 to lift restrictions on `NoReturn` * Introducing `typing.Never` as an alias for `NoReturn` and not holding it to the same restrictions * Using a self-defined class `Impossible` as parameter type for `assert_never` and just not creating instances of it (Also has the Any problem) * Reporting reachable `assert False` as error (Might lead to a lot of false positives, where a `assert False` is unreachable but it can't be statically determined) My suggestion would be |adding |`assert_exhaustive(x: Any)`| to |typing|. The implementation could raise a fitting exception (Just |assert False| would of course also work, but I would argue that it's helpful to also give more details if it fails at runtime. Not only if it fails during type-checking). Type-checkers can then just be hardcoded to handle `assert_exhaustive()`. They could also make sure that `assert_exhaustive()` is only used within `else` blocks (and maybe `case _` blocks in the future). PS: Starting in April I will be writing my bachelors thesis on the topic of "Exhaustiveness check for Structural Pattern Matching in Python 3.10". My work will most likely be based on mypy and I'm planing to contribute the code back to upstream. Having an "official" way to annotate exhaustiveness would be really useful for me. -- Adrian Freund ||
It looks like my thunderbird messed up the plain text of the email. The html version looks fine. Here's the text again: Hello, currently when people want to annotate that a if-elif check should be exhaustive and have a type-checker like mypy verify the exhaustiveness they have to resort to a clever hack that looks like this (This works in mypy. I haven't verified any other type-checkers): ``` from typing import NoReturn def assert_never(x: NoReturn) -> NoReturn: raise AssertionError(f"Invalid value: {x!r}") from typing import Union def type_checking_ok(foo: Union[str, int]) -> None: if isinstance(foo, str): print("str") elif isinstance(foo, int): print("int") else: assert_never(foo) def type_checking_ko(foo: Union[str, int]) -> None: if isinstance(foo, str): print("str") else: assert_never(foo) ``` This works by abusing the fact that mypy doesn't typecheck unreachable code and assert_never can't be called by a valid function call (*except for corner cases I will discuss later). Mypy also won't report it as unreachable if it is unreachable, as it returns `NoReturn`. If it can be reached mypy will complain about incompatible parameter types. This has a few problems: * It can be broken by `Any`. For example if `foo` is of type `Union[int, Any]` and you only check for `int` mypy won't show an error * According to PEP 484 `NoReturn` is only valid as a return type and should be considered an error if it appears in any other positions. * Some type-checkers might report the error, even if it is unreachable This is used in the wild for example by pytest. Due to python 3.10 introducing the match statement there will probably also be renewed interest in checking exhaustiveness. Therefor I would really like to see an official way to annotate this. There have already been discussions. There have already been multiple discussions of this topic on both the mypy github and the typing github: https://github.com/python/typing/issues/735 https://github.com/python/mypy/issues/5818 (https://github.com/python/mypy/issues/9748) Discussed solutions/improvements include: * Changing how `Any` and `NoReturn` interact https://github.com/python/mypy/issues/3194 * Changing PEP 484 to lift restrictions on `NoReturn` * Introducing `typing.Never` as an alias for `NoReturn` and not holding it to the same restrictions * Using a self-defined class `Impossible` as parameter type for `assert_never` and just not creating instances of it (Also has the Any problem) * Reporting reachable `assert False` as error (Might lead to a lot of false positives, where a `assert False` is unreachable but it can't be statically determined) My suggestion would be adding `assert_exhaustive(x: Any)` to typing. The implementation could raise a fitting exception (Just assert False would of course also work, but I would argue that it's helpful to also give more details if it fails at runtime. Not only if it fails during type-checking). Type-checkers can then just be hardcoded to handle `assert_exhaustive()`. They could also make sure that `assert_exhaustive()` is only used within `else` blocks (and maybe `case _` blocks in the future). PS: Starting in April I will be writing my bachelors thesis on the topic of "Exhaustiveness check for Structural Pattern Matching in Python 3.10". My work will most likely be based on mypy and I'm planing to contribute the code back to upstream. Having an "official" way to annotate exhaustiveness would be really useful for me. -- Adrian Freund
Pyright has an internal type called `Never` that is effectively an alias for `NoReturn` (and is semantically equivalent to an empty union). Pyright supports `NoReturn` for input parameter annotations to allow for functions like `assert_never`. I can't speak for pyre or pytest, but I'm guessing that they also ignore the restriction in PEP 484 to allow for this mechanism. That said, I'd be in favor of introducing a `typing.Never` alias as you've suggested. I think it would add clarity with little or no additional complexity. Your note is timely. I just finished implementing a new feature in the latest version of Pyright that I refer to as "implied else narrowing". It's used in cases where an "if" or "elif" clause is missing a corresponding "else" clause and the conditional expression in the "if" or "elif" can be narrowed to a "Never" type in the negative (else) case. It allows for automatic exhaustiveness checking without the introduction of an explicit `asser_never` call. See here for [documentation and samples](https://github.com/microsoft/pyright/blob/master/docs/type-concepts.md#narro...). This feature was relatively straightforward to implement once I worked out the rules, but I don't know enough about mypy's architecture to say whether it will be similarly straightforward to implement there. The rules can get a little complicated if you want to support composite conditional expressions — those that include `and`, `or`, and `not` modifiers. For reference, here's [the commit that introduces the feature in Pyright](https://github.com/microsoft/pyright/commit/c53cadf07039bb3911ff7dc9c42cae62...). My initial implementation had a measurable impact on pyright's analysis performance (about a 15% perf regression in typical code, and significantly more in the worst case) because of the additional code flow nodes it introduced to the graph. I've made some subsequent changes (heuristics) to claw back most of that perf loss. -- Eric Traut Contributor to Pyright & Pylance Microsoft Corp.
participants (2)
-
Adrian Freund -
Eric Traut