-
Notifications
You must be signed in to change notification settings - Fork 258
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
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 | ||
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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe 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, There was a problem hiding this comment. Choose a reason for hiding this commentThe 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()`` | ||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | ||
|
||
|
There was a problem hiding this comment.
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: