Skip to content

Add additional examples about TypeIs #1814

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 77 additions & 1 deletion docs/guides/type_narrowing.rst
Original file line number Diff line number Diff line change
Expand Up @@ -195,15 +195,91 @@ This behavior can be seen in the following example::
else:
reveal_type(x) # Unrelated

There are also cases beyond just mutability. In some cases, it may not be
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This fits better under "Safety and soundness" below, probably as a new subheader.

The example could be made more convincing; I think it's not going to be clear to most readers why it's unsafe.

I think something like this would demonstrate it:


def takes_any_a(a: A[int | str]):
    if possible_problem(a):
        assert_type(a, A[int])  # OK because A[int] is a subtype of A[int | str]
        if isinstance(a, B):
            assert_type(a, B[int])  # A[int] & B -> B[int]
            print(b.j + 1)  # boom
takes_any_a(B(i=1, j="x"))

possible to narrow a type fully from information available to the ``TypeIs``
function. In such cases, raising an error is the only possible option, as you
have neither enough information to confirm or deny a type narrowing operation.
(Note: returning false (denying) results in unsafe negative narrowing in this
case) This is most likely to occur with narrowing of generics.

To see why, we can look at the following example::

from typing_extensions import TypeVar, TypeIs
from typing import Generic

X = TypeVar("X", str, int, str | int, covariant=True, default=str | int)

class A(Generic[X]):
def __init__(self, i: X, /):
self._i: X = i

@property
def i(self) -> X:
return self._i


class B(A[X], Generic[X]):
def __init__(self, i: X, j: X, /):
super().__init__(i)
self._j: X = j

@property
def j(self) -> X:
return self._j

def possible_problem(x: A) -> TypeIs[A[int]]:
return isinstance(x.i, int)

def possible_correction(x: A) -> TypeIs[A[int]]:
if type(x) is A:
# only narrow cases we know about
return isinstance(x.i, int)
raise TypeError(
f"Refusing to narrow Genenric type {type(x)!r}"
f"from function that only knows about {A!r}"
)

Because it is possible to attempt to narrow B,
but A does not have appropriate information about B
(or any other unknown subclass of A!) it's not possible to safely narrow
in either direction. The general rule for generics is that if you do not know
all the places a generic class is generic and do not check enough of them to be
absolutely certain, you cannot return True, and if you do not have a definitive
counter example to the type to be narrowed to you cannot return False.
In practice, if soundness is prioritized over an unsafe narrowing,
not knowing what you don't know is solvable by either
erroring out when neither return option is safe, or by making the class to be
narrowed final to avoid such a situation.

Safety and soundness
--------------------

While type narrowing is important for typing real-world Python code, many
forms of type narrowing are unsafe in the presence of mutability. Type checkers
forms of type narrowing are unsafe. Type checkers
attempt to limit type narrowing in a way that minimizes unsafety while remaining
useful, but not all safety violations can be detected.

One example of this tradeoff building off of TypeIs
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This also fits better as a new subparagraph instead of as part of the header


If you trust that users implementing the Sequence Protocol are doing so in a
way that is safe to iterate over, and will not be mutated for the duration
you are relying on it; then while the following function can never be fully
sound, full soundness is not necessarily easier or better for your use::

def useful_unsoundness(s: Sequence[object]) -> TypeIs[Sequence[int]]:
return all(isinstance(i, int) for i in s)

However, many cases of this sort can be extracted for safe use with an
alternative construction if soundness is of a high priority,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note this has other tradeoffs, e.g. potentially higher memory usage. For example, range(1000) is a Sequence, turning it into the equivalent tuple takes a lot more memory.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it really appropriate to maintain more than that there are examples of tradeoffs here and then allow people to use some basic thought from there? The runtime memory characteristics seem somewhat out of scope for typing soundness, and an exhaustive list would require further evaluation and possibly reevaluation on any sequence type added to the standard library

and the cost of a copy is acceptable::

def safer(s: Sequence[object]) -> Sequence[int]:
ret = tuple(i for i in s if isinstance(i, int))
if len(ret) != len(s):
raise TypeError
return ret


``isinstance()`` and ``issubclass()``
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Expand Down