PEP 724: Stricter TypeGuard

.github/CODEOWNERS

@@ -601,6 +601,7 @@ pep-0720.rst  @FFY00
 pep-0721.rst  @encukou
 pep-0722.rst  @pfmoore
 pep-0723.rst  @AA-Turner
+pep-0724.rst  @jellezijlstra
 pep-0725.rst  @pradyunsg
 pep-0726.rst  @AA-Turner
 pep-0727.rst  @JelleZijlstra

pep-0724.rst

@@ -0,0 +1,306 @@
+PEP: 724
+Title: Stricter Type Guards
+Author: Rich Chiodo <rchiodo at microsoft.com>, 
+        Eric Traut <erictr at microsoft.com>, 
+        Erik De Bonte <erikd at microsoft.com>
+Sponsor: Jelle Zijlstra <[email protected]>
+Discussions-To: https://mail.python.org/archives/list/[email protected]/thread/EMUD2D424OI53DCWQ4H5L6SJD2IXBHUL/
+Status: Draft
+Type: Standards Track
+Topic: Typing
+Content-Type: text/x-rst
+Created: 28-Jul-2023
+Python-Version: 3.13
+Post-History: 
+
+
+Abstract
+========
+
+:pep:`647` introduced the concept of ``TypeGuard`` functions which return
+``True`` if their input parameter matches their target type. For example, a
+function that returns ``TypeGuard[str]`` is assumed to return ``True`` if and
+only if its input parameter is a ``str``. This allows type checkers to narrow
+types when a ``TypeGuard`` function returns ``True``.
+
+This PEP further refines :pep:`647` by allowing type checkers to also narrow
+types when a ``TypeGuard`` function returns ``False``.
+
+Motivation
+==========
+
+``TypeGuard``\ s are used throughout Python libraries to allow a type checker
+to narrow the type of something when the ``TypeGuard`` returns ``True``.
+
+However, in the ``False`` case, :pep:`647` doesn't prescribe what the type
+might be:
+
+.. code-block:: python
+
+    def is_str(val: str | int) -> TypeGuard[str]:
+        return isinstance(val, str)
+
+    def func(val: str | int):
+        if is_str(val):
+            # Type checkers can assume val is a 'str' in this branch
+        else:
+            # Type here is not narrowed. It is still 'str | int' 
+
+
+Specification
+=============
+
+Given a ``TypeGuard`` and a calling function like so:
+
+.. code-block:: python
+
+    def guard(x: P) -> TypeGuard[R]: ...
+
+    def func1(val: A):
+        if guard(val):
+            reveal_type(val) # NP
+        else:
+            reveal_type(val) # NN
+
+Each use of a ``TypeGuard`` involves five types:
+
+* P = ``TypeGuard`` parameter type
+* R = ``TypeGuard`` return type
+* A = Argument type (pre-narrowed)
+* NP = Narrowed type (positive)
+* NN = Narrowed type (negative)
+
+
+This PEP proposes some modifications to :pep:`647` in order to allow a type
+checker to further narrow what a ``TypeGuard`` returns when the ``R`` type is
+consistent [#isconsistent]_ with the ``P`` type.
+
+* When the output type ``R`` of a ``TypeGuard`` is consistent [#isconsistent]_
+  with the type of its first input parameter (``P``), type checkers will apply
+  stricter type semantics:
+
+.. code-block:: python
+
+    # Stricter TypeGuard possible (Kangaroo | Koala is consistent with Animal)
+    def is_marsupial(val: Animal) -> TypeGuard[Kangaroo | Koala]: 
+        return isinstance(val, Kangaroo | Koala)
+
+    # Stricter TypeGuard not possible (list[T] is not consistent with 
+    # list[T | None])
+    def has_no_nones(val: list[T | None]) -> TypeGuard[list[T]]: 
+        return None not in val
+
+* When stricter semantics are possible, the output type for the ``False`` or
+  ``NN`` case can be determined:
+
+.. code-block:: python
+
+    def is_str(val: str | int) -> TypeGuard[str]: # Stricter mode possible
+        return isinstance(val, str)
+
+    def func(val: str | int):
+        if is_str(val):
+            # Type checkers can assume val is a 'str' in this branch
+        else:
+            # Type checkers can assume val is an 'int' in this branch
+
+* When the output type of the ``TypeGuard`` is a union, the type checker can
+  apply additional type narrowing based on the type of the first input
+  argument, eliminating union elements that are impossible given the input
+  argument type:
+
+.. code-block:: python
+
+    def is_cardinal_direction(val: str) -> TypeGuard[Literal["N", "S", "E", "W"]]:
+        return val in ("N", "S", "E", "W")
+
+    def func(direction: Literal["NW", "E"]):
+        if is_cardinal_direction(direction):
+            # Literal["E"] The type cannot be "N", "S" or "W" here because of
+            # argument type
+        else:
+            # Literal["NW"]
+
+
+This logic can be summed up in a table:
+
+============ ======================= ===================
+|space|      Non strict TypeGuard    Strict TypeGuard
+============ ======================= ===================
+Applies when R not consistent with P R consistent with P
+NP is ..     :math:`R`               :math:`A \land R`
+NN is ..     :math:`A`               :math:`A \land \neg{R}`
+============ ======================= ===================
+
+Intersection of types and type negation are not defined and are left up to the
+type checker to decide on how to implement. Future `extensions`__ to the type
+system may change this behavior though.
+
+__ https://github.com/CarliJoy/intersection_examples/blob/main/specification.rst
+
+.. |space| unicode:: 0x2008
+
+Additional Examples
+===================
+
+Any
+---
+
+``Any`` is consistent [#isconsistent]_ with any other type, which means
+stricter semantics can be applied. 
+
+.. code-block:: python
+
+    def is_a(x: Any) -> TypeGuard[A]: # Stricter TypeGuard possible
+        return isinstance(x, A)
+
+    def test(x: A | B):
+        if is_a(x):
+            # x is of type A here
+        else:
+            # x is of type B here
+
+Degenerate case
+---------------
+
+It is possible to break the type checker by making a ``TypeGuard`` that is
+incorrect:
+
+.. code-block:: python
+
+    def is_positive_int(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int) and val > 0
+
+    def func(val: int | str):
+        if is_positive_int(val):
+            # Type checker assumes int here
+        else:
+            # Type checker assumes str incorrectly here
+
+As :pep:`647 <647#enforcing-strict-narrowing>` stated, users can create invalid
+``TypeGuard``\ s. The same thing applies to this PEP. If the user is not
+careful the type checker may flag things incorrectly.
+
+Backwards Compatibility
+=======================
+
+The new ``False`` case for a ``TypeGuard`` breaks backwards compatibility.
+
+.. code-block:: python
+
+    def is_int(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int)
+
+    def func(val: int | str):
+        if is_int(val):
+            # Type checker assumes int here
+        else:
+            # Type checker assumes str here
+
+A type checker will assume in the ``False`` case that the value is ``str``.
+
+This is a change in behavior from :pep:`647`.
+
+Although this is different behavior, existing code would likely have further
+checks for a ``str`` in the ``False`` case. Since the previous behavior was to
+assume ``str | int``, existing code would have had to further refine the type
+to get a type checker to behave the expected way.
+
+Something like so:
+
+.. code-block:: python
+
+    def is_int(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int)
+
+    def is_str(val: int | str) -> TypeGuard[int]:
+        return isinstance(val, int)
+
+    def func(val: int | str):
+        if is_int(val):
+            # Code does something with int here
+        else is_str(val): # This check would have been necessary before
+            # Code does something with str here
+
+
+This means existing code should continue to work with the ``False`` narrowing.
+
+As a proof of this concept, we ran the `experimental Pyright changes`__
+against `mypy primer`__ to see if there were any differences in the output.
+Changing ``TypeGuard`` to be more strict had a small effect on the ``mypy
+primer``. Mostly indicating that some ``# type: ignore`` comments were no longer
+necessary.
+
+__ https://github.com/microsoft/pyright/pull/5832
+__ https://github.com/hauntsaninja/mypy_primer
+
+
+How to Teach This
+=================
+
+We assert that users unfamiliar with ``TypeGuard`` will expect the behavior
+outlined in this PEP, therefore making ``TypeGuard`` easier to teach and
+explain.
+
+
+Reference Implementation
+========================
+
+A reference `implementation`__ of this idea exists in Pyright.
+
+__ https://github.com/microsoft/pyright/commit/9a5af798d726bd0612cebee7223676c39cf0b9b0
+
+
+Rejected Ideas
+==============
+
+StrictTypeGuard
+---------------
+
+Originally a new ``StrictTypeGuard`` construct was proposed. A
+``StrictTypeGuard`` would be similar to a ``TypeGuard`` except it would
+explicitly state that output type was consistent [#isconsistent]_ with the
+input type. Type checkers would validate that the output type was consistent
+[#isconsistent]_ with the input type.
+
+See this comment: `StrictTypeGuard proposal`__
+
+__ https://github.com/python/typing/discussions/1013#discussioncomment-1966238
+
+This was rejected because for most cases it's not necessary. Most people assume
+when the ``TypeGuard`` returns ``False``, that the input type has been narrowed
+to its other type. Why not just change the specification to match their
+assumptions?
+
+TypeGuard with a second output type
+-----------------------------------
+
+Another idea was also proposed where a ``TypeGuard`` could have a second output
+type. Something like so:
+
+.. code-block:: python
+
+    def is_int(val: int | str) -> TypeGuard[int, str]:
+        return isinstance(val, int)
+
+
+The second output type tells a type checker what type is returned in the ``False``
+case. It was originally proposed `here.`__ 
+
+__ https://github.com/python/typing/issues/996
+
+This idea was rejected because of the negative feedback it received.
+Specifically this `thread.`__
+
+__ https://mail.python.org/archives/list/[email protected]/thread/EMUD2D424OI53DCWQ4H5L6SJD2IXBHUL
+
+Footnotes
+=========
+
+.. [#isconsistent] :pep:`PEP 483's discussion of is-consistent <483#summary-of-gradual-typing>`
+
+Copyright
+=========
+
+This document is placed in the public domain or under the CC0-1.0-Universal
+license, whichever is more permissive.