PEP 742: Expand "How to Teach This" (#3683)

Example sections on:
- When to use TypeIs
- How to write a safe TypeIs
- TypeIs vs. TypeGuard

Also note the implementations in typing-extensions, pyright, and pyanalyze.

peps/pep-0742.rst

@@ -253,14 +253,170 @@ along with discussion of other narrowing constructs such as :py:func:`isinstance
 documentation should emphasize ``TypeIs`` over :py:data:`typing.TypeGuard`; while the
 latter is not being deprecated and its behavior is occasionally useful, we expect that the
 behavior of ``TypeIs`` is usually more intuitive, and most users should reach for
-``TypeIs`` first.
+``TypeIs`` first. The rest of this section contains some example content that could
+be used in introductory user-facing documentation.
 
+When to use ``TypeIs``
+----------------------
+
+Python code often uses functions like ``isinstance()`` to distinguish between
+different possible types of a value. Type checkers understand ``isinstance()``
+and various other checks and use them to narrow the type of a variable. However,
+sometimes you want to reuse a more complicated check in multiple places, or
+you use a check that the type checker doesn't understand. In these cases, you
+can define a ``TypeIs`` function to perform the check and allow type checkers
+to use it to narrow the type of a variable.
+
+A ``TypeIs`` function takes a single argument and is annotated as returning
+``TypeIs[T]``, where ``T`` is the type that you want to narrow to. The function
+must return ``True`` if the argument is of type ``T``, and ``False`` otherwise.
+The function can then be used in ``if`` checks, just like you would use ``isinstance()``.
+For example::
+
+    from typing import TypeIs, Literal
+
+    type Direction = Literal["N", "E", "S", "W"]
+
+    def is_direction(x: str) -> TypeIs[Direction]:
+        return x in {"N", "E", "S", "W"}
+
+    def maybe_direction(x: str) -> None:
+        if is_direction(x):
+            print(f"{x} is a cardinal direction")
+        else:
+            print(f"{x} is not a cardinal direction")
+
+Writing a safe ``TypeIs`` function
+----------------------------------
+
+A ``TypeIs`` function allows you to override your type checker's type narrowing
+behavior. This is a powerful tool, but it can be dangerous because an incorrectly
+written ``TypeIs`` function can lead to unsound type checking, and type checkers
+cannot detect such errors.
+
+For a function returning ``TypeIs[T]`` to be safe, it must return ``True`` if and only if
+the argument is compatible with type ``T``, and ``False`` otherwise. If this condition is
+not met, the type checker may infer incorrect types.
+
+Below are some examples of correct and incorrect ``TypeIs`` functions::
+
+    from typing import TypeIs
+
+    # Correct
+    def good_typeis(x: object) -> TypeIs[int]:
+        return isinstance(x, int)
+
+    # Incorrect: does not return True for all ints
+    def bad_typeis1(x: object) -> TypeIs[int]:
+        return isinstance(x, int) and x > 0
+
+    # Incorrect: returns True for some non-ints
+    def bad_typeis2(x: object) -> TypeIs[int]:
+        return isinstance(x, (int, float))
+
+This function demonstrates some errors that can occur when using a poorly written
+``TypeIs`` function. These errors are not detected by type checkers::
+
+    def caller(x: int | str, y: int | float) -> None:
+        if bad_typeis1(x):  # narrowed to int
+            print(x + 1)
+        else:  # narrowed to str (incorrectly)
+            print("Hello " + x)  # runtime error if x is a negative int
+
+        if bad_typeis2(y):  # narrowed to int
+            # Because of the incorrect TypeIs, this branch is taken at runtime if
+            # y is a float.
+            print(y.bit_count())  # runtime error: this method exists only on int, not float
+        else:  # narrowed to float (though never executed at runtime)
+            pass
+
+Here is an example of a correct ``TypeIs`` function for a more complicated type::
+
+    from typing import TypedDict, TypeIs
+
+    class Point(TypedDict):
+        x: int
+        y: int
+
+    def is_point(x: object) -> TypeIs[Point]:
+        return (
+            isinstance(x, dict)
+            and all(isinstance(key, str) for key in x)
+            and "x" in x
+            and "y" in x
+            and isinstance(x["x"], int)
+            and isinstance(x["y"], int)
+        )
+
+``TypeIs`` and ``TypeGuard``
+----------------------------
+
+``TypeIs`` and :py:data:`typing.TypeGuard` are both tools for narrowing the type of a variable
+based on a user-defined function. Both can be used to annotate functions that take an
+argument and return a boolean depending on whether the input argument is compatible with
+the narrowed type. These function can then be used in ``if`` checks to narrow the type
+of a variable.
+
+``TypeIs`` usually has the most intuitive behavior, but it
+introduces more restrictions. ``TypeGuard`` is the right tool to use if:
+
+* You want to narrow to a type that is not compatible with the input type, for example
+  from ``list[object]`` to ``list[int]``.  ``TypeIs`` only allows narrowing between
+  compatible types.
+* Your function does not return ``True`` for all input values that are compatible with
+  the narrowed type. For example, you could have a ``TypeGuard[int]`` that returns ``True``
+  only for positive integers.
+
+``TypeIs`` and ``TypeGuard`` differ in the following ways:
+
+* ``TypeIs`` requires the narrowed type to be a subtype of the input type, while
+  ``TypeGuard`` does not.
+* When a ``TypeGuard`` function returns ``True``, type checkers narrow the type of the
+  variable to exactly the ``TypeGuard`` type. When a ``TypeIs`` function returns ``True``,
+  type checkers can infer a more precise type combining the previously known type of the
+  variable with the ``TypeIs`` type. (Technically, this is known as an intersection type.)
+* When a ``TypeGuard`` function returns ``False``, type checkers cannot narrow the type of
+  the variable at all. When a ``TypeIs`` function returns ``False``, type checkers can narrow
+  the type of the variable to exclude the ``TypeIs`` type.
+
+This behavior can be seen in the following example::
+
+    from typing import TypeGuard, TypeIs, reveal_type, final
+
+    class Base: ...
+    class Child(Base): ...
+    @final
+    class Unrelated: ...
+
+    def is_base_typeguard(x: object) -> TypeGuard[Base]:
+        return isinstance(x, Base)
+
+    def is_base_typeis(x: object) -> TypeIs[Base]:
+        return isinstance(x, Base)
+
+    def use_typeguard(x: Child | Unrelated) -> None:
+        if is_base_typeguard(x):
+            reveal_type(x)  # Base
+        else:
+            reveal_type(x)  # Child | Unrelated
+
+    def use_typeis(x: Child | Unrelated) -> None:
+        if is_base_typeis(x):
+            reveal_type(x)  # Child
+        else:
+            reveal_type(x)  # Unrelated
 
 Reference Implementation
 ========================
 
-A draft implementation for mypy `is available <https://github.com/python/mypy/pull/16898>`__.
+The ``TypeIs`` special form `has been implemented <https://github.com/python/typing_extensions/pull/330>`__
+in the ``typing_extensions`` module and will be released in typing_extensions 4.10.0.
 
+Implementations are available for several type checkers:
+
+- Mypy: `pull request open <https://github.com/python/mypy/pull/16898>`__
+- Pyanalyze: `pull request <https://github.com/quora/pyanalyze/pull/718>`__
+- Pyright: `added in version 1.1.351 <https://github.com/microsoft/pyright/releases/tag/1.1.351>`__
 
 Rejected Ideas
 ==============