Exhaustiveness checking in match statements
I’d like to gather some opinions or suggestions on exhaustiveness checking on match statements, stemming from https://github.com/python/mypy/pull/10191 (though most future discussion should happen on https://github.com/python/mypy/issues/12010). I’m especially interested in any experience from working with this already, such as in pyright. # case _: assert False would trigger a type check error if reachable. This would allow users to mark match statements as exhaustive. This would require assert False to be treated specially by type checkers in a “match all” case statement, but it’s inline with a common usage of assert false at the end of an if chain today, and wouldn’t introduce new constructs. # --exhaustive-match flag for checkers like mypy This would be a new “strict' flag added to mypy “strict” that would force match statements to be statically exhaustive - this is not (and maybe could not) be enforced at runtime by Python, but could for a static type checker, and would force case _: pass to be added if fallthrough was expected - to make it explicit, and avoid forgetting to add case _: assert False. At some some codebases would likely benefit from this flag. I assume this could be done by other checkers too. It would be a normal mypy strictness flag, so could be enabled/disabled per module, etc. # Current workaround The current workaround for this is to have a function assert_never that takes a NoReturn - NoReturn happens to be (the only) way to spell an empty Union (at least in mypy?). This also works with type narrowing in if statements, so is usable before requiring 3.10+. Until one or both of the above are implemented, it’s the only way to check pattern matching for exhaustiveness, too. Personally, I’d like a slightly nicer way to write this as well, with assert_unreabable or something, or at least a Nothing/EmptyUnion spelling for NoReturn. I think the current leaning is to implement the first two, and do nothing on the third. Thoughts? Especially on the exhaustive-match flag. - Henry
One clarification: On Wed, Jan 19, 2022 at 8:39 AM Henry F. Schreiner <henryfs@princeton.edu> wrote:
It could have been, but the PEP 634 authors chose not to require it, so it should not be enforced at runtime.
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-c...>
Pattern matching support has been implemented in pyright for about a year now. We have received one or two requests for a way to enforce exhaustion through a configuration option. So far, we've resisted adding this because there are valid use cases of `match` that don't involve exhaustion. Our viewpoint is that it's better to indicate exhaustion explicitly if that's your intent. If there's sufficient interest in a configuration option (similar to the proposed "--exhaustive-match" switch in mypy), we might be compelled to add this in pyright as well. I don't think we would enable it by default, even in strict mode. I'm pretty negative on having a static type checker generate errors on an `assert False` statement, even if (especially if) it's only in this specific context. It's a non-obvious special case, it's too specific (e.g. does it work if you also provide an error string?), and this statement has nothing to do with type checking. I'd be reluctant to implement such as solution in pyright even if mypy chose to add this special case. I'd strongly prefer to standardize on `assert_never`. Regardless of what statement we choose here, we need to train users how to express that they want to enforce exhaustive testing, and `assert_never` is the proper way to do that using types. Furthermore, `assert_never` already works in all type checkers and has utility outside of match statements. It would be nice to include `assert_never` in one of the typeshed stdlib stubs so users don't need to implement it in their own code. -Eric -- Eric Traut Contributor to Pyright & Pylance Microsoft
I agree with Eric, `assert_never` is a good feature on its own. And it is a helper I re-implement in almost every project. I believe that standardizing will benefit many use-cases and many people. And it completely solved exhaustiveness checking with something like `case _unreachable: typing.assert_never(_unreachable)` ср, 19 янв. 2022 г. в 20:25, Eric Traut <eric@traut.com>:
Spoiler alert: I agree with Eric. There are two different things you may want to express with a statement like `assert False`: (1) This code is believed to be unreachable, but I can't convince the type checker that it is. This can be spelled with `assert False`. (2) This code is unreachable, and I want the type checker to tell me if it's not. This can be spelled with the `NoReturn` hack. Making `assert False` mean (2) in match statements would be inconsistent and would leave no way to express (1). I'm also not a fan of adding a flag for changing this behavior. Flags are usually for increasing or decreasing the strictness of the type checker, and users will generally want to work towards turning a flag on globally. But with this behavior, you'd want some match statements to enforce exhaustiveness and not others, maybe even in the same file. I'm also supportive of adding something like `typing.assert_never(x: NoReturn)`. I'm happy to work on implementing this at runtime. It's starting to look like enough new typing functions to write a PEP :). El mié, 19 ene 2022 a las 8:39, Henry F. Schreiner (<henryfs@princeton.edu>) escribió:
Okay, Jelle and Eric have convinced me. On Wed, Jan 19, 2022 at 11:10 AM Jelle Zijlstra <jelle.zijlstra@gmail.com> wrote:
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-c...>
This flag would mean only exhaustive match statements would be allowed to not have a catch-all statement at the end. I don’t think that’s a bad thing for a strict code base - you are forcing match statements that could possibly fall through to explicitly acknowledge the fall through. Yes, some match statements in a codebase have fall through, but those can have a `case _: pass` to tell the reader they might fall through. It’s a little more verbose, but clear and safe. It’s not the end of the world if there wasn’t such a flag, though. You could instead use a flake8 sort of a check that simply forces _all_ match statements to have a catch-all case, and then hope that the exhaustive ones use assert_never instead of pass. You just lose the cleanliness of being able to drop the catch-all for statically checked types; now all match’s need catch-alls in your codebase. The mypy flag does not interfere with a final catch-all assert_never clause, as well, it only affects match’s with no catch-all. - Henry
On Jan 19, 2022, at 2:09 PM, Jelle Zijlstra <jelle.zijlstra@gmail.com> wrote:
I'm also not a fan of adding a flag for changing this behavior. Flags are usually for increasing or decreasing the strictness of the type checker, and users will generally want to work towards turning a flag on globally. But with this behavior, you'd want some match statements to enforce exhaustiveness and not others, maybe even in the same file.
Am 19.01.22 um 20:09 schrieb Jelle Zijlstra:
(2) This code is unreachable, and I want the type checker to tell me if it's not. This can be spelled with the `NoReturn` hack.
Since various "NoReturn" hacks have come up in the past: I suggest to rename NoReturn to typing.Never and leave NoReturn as an alias. Having a bottom type has several uses, and we should use a name that reflects is usage clearly. - Sebastian
I'm a +100 on this the current name makes no sense to newbies (and myself until like a month ago) outside of return types, seeing x: NoReturn makes no sense whereas x: Never is much clearer as to whats actually going on. This is also something pyright already does.
I'm also +1 to introducing a typing.Never alias to typing.NoReturn, and clarifying (in a PEP) the various kinds of exhaustiveness checks that can be done with it. TypeScript already uses the spelling "never" for this concept [1] (so we would be consistent), and I think "never" would likely make sense for typing newcomers as well. [1]: https://www.typescriptlang.org/docs/handbook/2/narrowing.html#the-never-type On 1/19/22 11:09 AM, Jelle Zijlstra wrote:
Great ^_^ -- David Foster | Seattle, WA, USA Contributor to TypedDict support for mypy
One clarification: On Wed, Jan 19, 2022 at 8:39 AM Henry F. Schreiner <henryfs@princeton.edu> wrote:
It could have been, but the PEP 634 authors chose not to require it, so it should not be enforced at runtime.
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-c...>
Pattern matching support has been implemented in pyright for about a year now. We have received one or two requests for a way to enforce exhaustion through a configuration option. So far, we've resisted adding this because there are valid use cases of `match` that don't involve exhaustion. Our viewpoint is that it's better to indicate exhaustion explicitly if that's your intent. If there's sufficient interest in a configuration option (similar to the proposed "--exhaustive-match" switch in mypy), we might be compelled to add this in pyright as well. I don't think we would enable it by default, even in strict mode. I'm pretty negative on having a static type checker generate errors on an `assert False` statement, even if (especially if) it's only in this specific context. It's a non-obvious special case, it's too specific (e.g. does it work if you also provide an error string?), and this statement has nothing to do with type checking. I'd be reluctant to implement such as solution in pyright even if mypy chose to add this special case. I'd strongly prefer to standardize on `assert_never`. Regardless of what statement we choose here, we need to train users how to express that they want to enforce exhaustive testing, and `assert_never` is the proper way to do that using types. Furthermore, `assert_never` already works in all type checkers and has utility outside of match statements. It would be nice to include `assert_never` in one of the typeshed stdlib stubs so users don't need to implement it in their own code. -Eric -- Eric Traut Contributor to Pyright & Pylance Microsoft
I agree with Eric, `assert_never` is a good feature on its own. And it is a helper I re-implement in almost every project. I believe that standardizing will benefit many use-cases and many people. And it completely solved exhaustiveness checking with something like `case _unreachable: typing.assert_never(_unreachable)` ср, 19 янв. 2022 г. в 20:25, Eric Traut <eric@traut.com>:
Spoiler alert: I agree with Eric. There are two different things you may want to express with a statement like `assert False`: (1) This code is believed to be unreachable, but I can't convince the type checker that it is. This can be spelled with `assert False`. (2) This code is unreachable, and I want the type checker to tell me if it's not. This can be spelled with the `NoReturn` hack. Making `assert False` mean (2) in match statements would be inconsistent and would leave no way to express (1). I'm also not a fan of adding a flag for changing this behavior. Flags are usually for increasing or decreasing the strictness of the type checker, and users will generally want to work towards turning a flag on globally. But with this behavior, you'd want some match statements to enforce exhaustiveness and not others, maybe even in the same file. I'm also supportive of adding something like `typing.assert_never(x: NoReturn)`. I'm happy to work on implementing this at runtime. It's starting to look like enough new typing functions to write a PEP :). El mié, 19 ene 2022 a las 8:39, Henry F. Schreiner (<henryfs@princeton.edu>) escribió:
Okay, Jelle and Eric have convinced me. On Wed, Jan 19, 2022 at 11:10 AM Jelle Zijlstra <jelle.zijlstra@gmail.com> wrote:
-- --Guido van Rossum (python.org/~guido) *Pronouns: he/him **(why is my pronoun here?)* <http://feministing.com/2015/02/03/how-using-they-as-a-singular-pronoun-can-c...>
This flag would mean only exhaustive match statements would be allowed to not have a catch-all statement at the end. I don’t think that’s a bad thing for a strict code base - you are forcing match statements that could possibly fall through to explicitly acknowledge the fall through. Yes, some match statements in a codebase have fall through, but those can have a `case _: pass` to tell the reader they might fall through. It’s a little more verbose, but clear and safe. It’s not the end of the world if there wasn’t such a flag, though. You could instead use a flake8 sort of a check that simply forces _all_ match statements to have a catch-all case, and then hope that the exhaustive ones use assert_never instead of pass. You just lose the cleanliness of being able to drop the catch-all for statically checked types; now all match’s need catch-alls in your codebase. The mypy flag does not interfere with a final catch-all assert_never clause, as well, it only affects match’s with no catch-all. - Henry
On Jan 19, 2022, at 2:09 PM, Jelle Zijlstra <jelle.zijlstra@gmail.com> wrote:
I'm also not a fan of adding a flag for changing this behavior. Flags are usually for increasing or decreasing the strictness of the type checker, and users will generally want to work towards turning a flag on globally. But with this behavior, you'd want some match statements to enforce exhaustiveness and not others, maybe even in the same file.
Am 19.01.22 um 20:09 schrieb Jelle Zijlstra:
(2) This code is unreachable, and I want the type checker to tell me if it's not. This can be spelled with the `NoReturn` hack.
Since various "NoReturn" hacks have come up in the past: I suggest to rename NoReturn to typing.Never and leave NoReturn as an alias. Having a bottom type has several uses, and we should use a name that reflects is usage clearly. - Sebastian
I'm a +100 on this the current name makes no sense to newbies (and myself until like a month ago) outside of return types, seeing x: NoReturn makes no sense whereas x: Never is much clearer as to whats actually going on. This is also something pyright already does.
I'm also +1 to introducing a typing.Never alias to typing.NoReturn, and clarifying (in a PEP) the various kinds of exhaustiveness checks that can be done with it. TypeScript already uses the spelling "never" for this concept [1] (so we would be consistent), and I think "never" would likely make sense for typing newcomers as well. [1]: https://www.typescriptlang.org/docs/handbook/2/narrowing.html#the-never-type On 1/19/22 11:09 AM, Jelle Zijlstra wrote:
Great ^_^ -- David Foster | Seattle, WA, USA Contributor to TypedDict support for mypy
participants (8)
-
David Foster -
Eric Traut -
Guido van Rossum -
Henry F. Schreiner -
James H-B -
Jelle Zijlstra -
Sebastian Rittau -
Никита Соболев