- Notifications
You must be signed in to change notification settings - Fork263
Description
Thetyping spec states that, whenA andB are potentially overloaded methods
If a callable
Bis overloaded with two or more signatures, it isassignable to callableAif at least one of the overloaded signatures inBis assignable toAIf a callable
Ais overloaded with two or more signatures, callableBis assignable toAifBis assignable to all of the signatures inA
However, this definition seems to be too strict. Consider the following example:
fromtypingimportProtocol,Self,overloadclassIntScalarOurs(Protocol):def__add__(self,other:int|Self,/)->Self: ...classIntScalarTheirs(Protocol):@overloaddef__add__(self,other:int,/)->Self: ...@overloaddef__add__(self,other:Self,/)->Self: ...
These two protocols specify the exact same runtime behavior. Yet, following the rules of the spec,IntScalarOurs is assignable toIntScalarTheirs, butIntScalarTheirs is not assignable toIntScalarOurs.
Case 1:A=IntScalarOurs,B=IntScalarTheirs.
If a callable B is overloaded with two or more signatures, it is assignable to callable A if at least one of the overloaded signatures in B is assignable to A
- Is
(self, int) -> Selfassignable to(self, int | Self) -> Self? No, becauseintis not a supertype ofint | Self(contravariance) - Is
(self, Self) -> Selfassignable to(self, int | Self) -> Self? No, becauseSelfis not a supertype ofint | Self(contravariance)
Thus,IntScalarTheirs is not assignable toIntScalarOurs.
Case 2:A=IntScalarTheirs,B=IntScalarOurs.
If a callable A is overloaded with two or more signatures, callable B is assignable to A if B is assignable to all of the signatures in A
- Is
(self, int | Self) -> Selfassignable to(self, int) -> Self? Yes. - Is
(self, int | Self) -> Selfassignable to(self, Self) -> Self? Yes.
Thus,IntScalarOurs is assignable toIntScalarTheirs.
From a pure set-theoretic POV, it seems that subtyping functions should follow a very simply rule based onthe domain.
What is currently specced appears to be a lemma for a sufficient condition, but not a necessary one.
Individual type-checkers can of course use such lemmas if the general case is too difficult to check/implement (and communicate that to their users), but shouldn't the spec be biased towards the theoretically principled point of view, when applicable?