First draft of an update to the Overloads chapter (DRAFT: DO NOT MERGE) #1839
Conversation
erictraut
commented
Aug 13, 2024
erictraut
commented
- Attempts to clearly define the algorithm for overload matching.
- Describes checks for overload consistency, overlapping overloads, and implementation consistency.
* Attempts to clearly define the algorithm for overload matching. * Describes checks for overload consistency, overlapping overloads, and implementation consistency.
…overloads * 'overloads' of https://github.com/erictraut/typing: [pre-commit.ci] auto fixes from pre-commit.com hooks # Conflicts: # docs/spec/overload.rst
…overloads * 'overloads' of https://github.com/erictraut/typing: [pre-commit.ci] auto fixes from pre-commit.com hooks
|
We typically wait for a proposed spec change to be accepted by the TC prior to writing conformance tests. In this case, I think it's advisable to write the conformance tests prior to acceptance. This will help us validate the proposed spec changes and tell us if (and to what extent) these changes will be disruptive for existing stubs and current type checker implementations. I would normally volunteer to write the conformance tests, but in this case I think it would be preferable for someone else to write the tests based on their reading of the spec update. If I write the tests, there's a real possibility that they will match what's in my head but not accurately reflect the letter of the spec. There's also a possibility that I'll miss some important cases in the tests. If someone else writes the tests, they can help identify holes and ambiguities in the spec language. Is there anyone willing to volunteer to write a draft set of conformance tests for this overload functionality? I'm thinking that there should be four new test files:
If this is more work than any one person wants to volunteer for, we could split it up. |
|
I am willing to work on conformance tests for this, but I probably can't get to it until the core dev sprint, Sept 23-27. I realize that implies a delay to moving forward with this PR. Happy for someone else to get to it first. |
| to "partially overlap". If two overloads partially overlap, the return type | ||
| of the former overload should be assignable to the return type of the | ||
| latter overload. If this condition doesn't hold, it is indicative of a | ||
| programming error and should be reported by type checkers. The purpose of | ||
| this check is to prevent unsoundness of this form:: | ||
|
|
||
| @overload | ||
| def is_one(x: Literal[0]) -> Literal[True]: ... | ||
| @overload | ||
| def is_one(x: int) -> Literal[False]: ... | ||
|
|
||
| reveal_type(is_one(int(1))) # Reveals Literal[False], but True at runtime |
There was a problem hiding this comment.
This unsoundness does not only constrain returns, but also other arguments. For example, let's consider PEP 728's __extra_items__.
For example, given this example from the PEP:
class Movie(TypedDict, closed=True):
name: str
__extra_items__: bool
we could imagine what the __setitem__ signature would be as an overload:
@overload
def __setitem__(self, key: Literal['name'], value: str) -> None: ...
@overload
def __setitem__(self, key: string, value: bool) -> None: ...
Where the unsoundness is exposed in a similar way as quoted, by exploiting Literal['name'] <: str.
key: str = 'name'
movie[key] = false
oops: str = movie['name']
Now, maybe this case would fall under the exemption below, as an exempted magic method. However, would we consider specifying that user-defined overloads constrain the arguments, like we have done for returns?
There was a problem hiding this comment.
I think in your example you wrote movie[str] = where you meant movie[key] =?
(Still thinking about the underlying issue.)
There was a problem hiding this comment.
I think for one thing, this suggests that the following line in PEP 728 requires more consideration:
Different from index signatures, the types of the known items do not need to be assignable to the extra_items argument.
There is a soundness reason for this restriction in index signatures, and perhaps we should re-consider whether it is advisable to discard this restriction in PEP 728.
I agree that this is also a soundness issue for user-defined overloads in general. I think in order to close this hole, we would need to specify that if any argument type overlaps between two overloads, then the latter overload must accept all calls that would be accepted by the earlier overload. Does that seem right to you?
I think we would need some empirical testing to understand what the impact of such a specification would be on real-world overloads. It might not be too bad. But I suspect this should be handled as a separate change to the spec, since I think it would be a significant change to current type-checker behavior, whereas I think this PR mostly intends to clarify and specify existing behavior.
