Add additional examples about TypeIs - #1814
Conversation
Sorry, something went wrong.
|
I'm not sure why the typing council decision label was added to this, this is purely an extended example of existing behavior to help better document the sharp edges that already exist on a typing feature and not a specification change, which does not appear to need one. Quoting: https://github.com/python/typing-council/blob/main/README.md
If there's anything I need to do to have this proceed, please let me know. |
Sorry, something went wrong.
|
This PR is to the spec, but I'm not sure why this text needs to be in the spec; it doesn't seem to specify any additional behavior. It might be a better fit for the guide on type narrowing that I added recently. |
Sorry, something went wrong.
|
Reviewing the proposed addition, I don't think this belongs in the typing spec. The typing spec is intended to specify how the type system works and how type checkers must behave. The proposed addition doesn't serve this purpose. It is instead directed at users of TypeIs. It therefore belongs in the typing guide, not the typing spec. |
Sorry, something went wrong.
|
Hmm. I thought placing it next to the existing example of behavior around TypeIs would make more sense, but I can retool the PR to move it to the guide, thanks for the feedback. |
Sorry, something went wrong.
| else: | ||
| reveal_type(x) # Unrelated | ||
|
|
||
| There are also cases beyond just mutability. In some cases, it may not be |
There was a problem hiding this comment.
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"))
Sorry, something went wrong.
| 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.
This also fits better as a new subparagraph instead of as part of the header
Sorry, something went wrong.
| 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.
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.
Sorry, something went wrong.
There was a problem hiding this comment.
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
Sorry, something went wrong.
|
I appreciate that you have other priorities, but if the scope of the changes after 9 months since last interaction are that you want additional tradeoffs noted (which I've noted a specific disagreement with) and slightly different organization, if the organization is that big a deal, please just provide a suggested change, merge it yourself and then amend organization, or close it, I don't want to spend the time for a continued back and forth for a minor change in organizing this months later, and you clearly have something in mind here that you could do more quickly yourself than the back and forth on it would require. |
Sorry, something went wrong.
This is a followup from discussion on discourse, and specifically this example which was constructed with the help of many going back and forth to determine a situation that could have a parallel in real world code, and which was possibly unsound. To not overly deter users from using this when it is appropriate, counter examples of "tolerably safe" narrowing functions that operate on generic types are included.