diff options
author | Jelle Zijlstra <jelle.zijlstra@gmail.com> | 2022-02-11 09:20:42 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2022-02-11 18:20:42 +0100 |
commit | 46094aa9a7cef3faf9344095db1feed31c77d176 (patch) | |
tree | 6b6a759ae8b62e3360539ffca15e05d62a8b19dc | |
parent | 77e79377a51e8cbb489daa9a7dca2b425aa62451 (diff) | |
download | typing-46094aa9a7cef3faf9344095db1feed31c77d176.tar.gz |
Add guide to unreachable code (#1065)
-rw-r--r-- | docs/source/guides.rst | 1 | ||||
-rw-r--r-- | docs/source/unreachable.rst | 148 |
2 files changed, 149 insertions, 0 deletions
diff --git a/docs/source/guides.rst b/docs/source/guides.rst index 9d435b7..c9af381 100644 --- a/docs/source/guides.rst +++ b/docs/source/guides.rst @@ -7,3 +7,4 @@ Type System Guides :caption: Contents: libraries + unreachable diff --git a/docs/source/unreachable.rst b/docs/source/unreachable.rst new file mode 100644 index 0000000..16c37d8 --- /dev/null +++ b/docs/source/unreachable.rst @@ -0,0 +1,148 @@ +.. _unreachable: + +******************************************** +Unreachable Code and Exhaustiveness Checking +******************************************** + +Sometimes it is necessary to write code that should never execute, and +sometimes we write code that we expect to execute, but that is actually +unreachable. The type checker can help in both cases. + +In this guide, we'll cover: + +- ``Never``, the primitive type used for unreachable code +- ``assert_never()``, a helper for exhaustiveness checking +- Directly marking code as unreachable +- Detecting unexpectedly unreachable code + +``Never`` and ``NoReturn`` +========================== + +Type theory has a concept of a +`bottom type <https://en.wikipedia.org/wiki/Bottom_type>`__, +a type that has no values. Concretely, this can be used to represent +the return type of a function that never returns, or the argument type +of a function that may never be called. You can also think of the +bottom type as a union with no members. + +The Python type system has long provided a type called ``NoReturn``. +While it was originally meant only for functions that never return, +this concept is naturally extended to the bottom type in general, and all +type checkers treat ``NoReturn`` as a general bottom type. + +To make the meaning of this type more explicit, Python 3.11 and +typing-extensions 4.1 add a new primitive, ``Never``. To type checkers, +it has the same meaning as ``NoReturn``. + +In this guide, we'll use ``Never`` for the bottom type, but if you cannot +use it yet, you can always use ``typing.NoReturn`` instead. + +``assert_never()`` and Exhaustiveness Checking +============================================== + +The ``Never`` type can be leveraged to perform static exhaustiveness checking, +where we use the type checker to make sure that we covered all possible +cases. For example, this can come up when code performs a separate action +for each member of an enum, or for each type in a union. + +To have the type checker do exhaustiveness checking for us, we call a +function with a parameter typed as ``Never``. The type checker will allow +this call only if it can prove that the code is not reachable. + +As an example, consider this simple calculator: + +.. code:: python + + import enum + from typing_extensions import Never + + def assert_never(arg: Never) -> Never: + raise AssertionError("Expected code to be unreachable") + + class Op(enum.Enum): + ADD = 1 + SUBTRACT = 2 + + def calculate(left: int, op: Op, right: int) -> int: + match op: + case Op.ADD: + return left + right + case Op.SUBTRACT: + return left - right + case _: + assert_never(op) + +The ``match`` statement covers all members of the ``Op`` enum, +so the ``assert_never()`` call is unreachable and the type checker +will accept this code. However, if you add another member to the +enum (say, ``MULTIPLY``) but don't update the ``match`` statement, +the type checker will give an error saying that you are not handling +the ``MULTIPLY`` case. + +Because the ``assert_never()`` helper function is frequently useful, +it is provided by the standard library as ``typing.assert_never`` +starting in Python 3.11, +and is also present in ``typing_extensions`` starting at version 4.1. +However, it is also possible to define a similar function in your own +code, for example if you want to customize the runtime error message. + +You can also use ``assert_never()`` with a sequence of ``if`` statements: + +.. code:: python + + def calculate(left: int, op: Op, right: int) -> int: + if op is Op.ADD: + return left + right + elif op is Op.SUBTRACT: + return left - right + else: + assert_never(op) + +Marking Code as Unreachable +======================= + +Sometimes a piece of code is unreachable, but the type system is not +powerful enough to recognize that. For example, consider a function that +finds the lowest unused street number in a street: + +.. code:: python + + import itertools + + def is_used(street: str, number: int) -> bool: + ... + + def lowest_unused(street: str) -> int: + for i in itertools.count(1): + if not is_used(street, i): + return i + assert False, "unreachable" + +Because ``itertools.count()`` is an infinite iterator, this function +will never reach the ``assert False`` statement. However, there is +no way for the type checker to know that, so without the ``assert False``, +the type checker will complain that the function is missing a return +statement. + +Note how this is different from ``assert_never()``: + +- If we used ``assert_never()`` in the ``lowest_unused()`` function, + the type checker would produce an error, because the type checker + cannot prove that the line is unreachable. +- If we used ``assert False`` instead of ``assert_never()`` in the + ``calculate()`` example above, we would not get the benefits of + exhaustiveness checking. If the code is actually reachable, + the type checker will not warn us and we could hit the assertion + at runtime. + +While ``assert False`` is the most idiomatic way to express this pattern, +any statement that ends execution will do. For example, you could raise +an exception or call a function that returns ``Never``. + +Detecting Unexpectedly Unreachable Code +======================================= + +Another possible problem is code that is supposed to execute, but that +can actually be statically determined to be unreachable. +Some type checkers have an option that enables warnings for code +detected as unreachable (e.g., ``--warn-unreachable`` in mypy). |