-
Notifications
You must be signed in to change notification settings - Fork 2
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
Intersections with Callable
, in particular Any
& Callable
#16
Comments
EDIT: There is possibly also a sort of middle ground option: Ⓒ Only subtyping rules of
Under this approach, |
If all of these are accurate:
x: A & B = ... # Here, we have to still check that x is both A and B
def f(x: A & B):
x.foo() # here, we have to check that this is consistent use with definitions for all existing defintions of foo in A & B
f(something) # here we check that something is both A and B No special case needed. |
Wait a second, I think this actually means that this whole example from earlier should already work fine, we don't even need
from where import UntypedLibraryType
from typing import Protocol
class Mine(Protocol):
def foo(self, x: int, /) -> int: ...
def fn(x: UntypedLibraryType & Mine):
x.foo(1) # this is how I expect it to be used
x.foo("blah") # this works because UntypedLibraryType is Any, and I would intend this as an error The type-checker will test whether the signature from typing import Protocol
class Mine(Protocol):
def foo(self, x: int, /) -> int: ...
def fn(x: Mine):
x.foo(1)
x.foo("blah") I think this really does mean that we can simplify |
It need only be consistent with one of |
@diabolo-dan why only with one of them? |
Here's how type checkers handle calls on unions today in Python: When
By symmetry, I would think that the rule for intersections would be: When
And yes, this means that if an Interestingly, TypeScript deviates from the above slightly in the case of intersections. If interface A {
y: (val: string) => number;
z: () => number;
}
interface B {
y: (val: number) => string;
z: () => string;
}
function f(c: A & B) {
const x = c.x(); // Error
const y1 = c.y(0); // string
const y2 = c.y(''); // number
const z = c.z(); // number (but becomes string if A and B interface names are swapped)
} The behavior in TypeScript seems inconsistent to me, and the "undocumented sorting algorithm" means that it cannot be replicated from a spec unless that spec fully documents the way types should be sorted. I'd prefer to avoid that for Python. |
Edit: The following was a response to an earlier post that was deleted. I'll leave it here, but it's probably no longer valid. @randolf-scholz, good point. That means my proposed rule above is flawed. "If A and B are both callable with args, the return result is the intersection of the return results from A and B" doesn't hold. This would explain TypeScript's behavior. It is effectively creating an overload from the two callables. The challenge is that overloads depend on ordering, but intersections are order-independent. That means some deterministic order must be imposed, which explains the sorting behavior in TypeScript. In TypeScript, overloads are simple. The first matching overload is always selected. In Python, thanks to mypy's implementation, overloads are extremely complex and involve a bunch of special casing for union expansion and handling of If A and B are both callable with args, the return result comes from the return type of Sort(A, B) where Sort is a sorting algorithm that deterministically chooses either A or B. We would then need to define the sorting algorithm. (Yuck.) I have a type sorting algorithm in pyright that I added in an attempt to make union-related operations more deterministic and order-independent, but I consider this algorithm to be an implementation detail. I presume that mypy has a similar sorting algorithm. Maybe it's OK to leave the sorting algorithm out of the spec and say that it's up to each type checker to implement this? But this will lead to different behaviors across type checkers. |
Hm, I think there is a problematic case though, which is incompatible signatures: class A:
def foo(self, *, key: str) -> T: ... # takes 1 mandatory keyword argument "key"
class B:
def foo(self) -> S: ... The issue here is that by the LSP, one is not allowed to have a subclass of I think one has to amend the rules as follows: When
Also, I wonder if "the operation is an error" can generally just be replaced by returning |
@erictraut I deleted the earlier comment, the argument was flawed. In the example class A:
def foo(self, x: int) -> int: ...
class B:
def foo(self, x: str) -> str: ...
class C(A, B):
@overload
def foo(self, x: int) -> int: ...
@overload
def foo(self, x: str) -> str: ...
Actually, I am not the only one who fell for this, in the current specification draft for |
I think most of this is ruled out by the original assignability check. I don't think it should be picking one of A or B as typescript does. If the two are incompatible, the two are incompatible. If they aren't, compatible use should be acceptable, but the assignability concern says it needs to be compatible with both. We aren't stating that there is a direct subclass with a specific MRO with intersections, and even if we were, replacement says such a subclass would have to be compatible this way too. @DiscordLiz linked an accepted (rust) RFC in #14 that has a section detailing detecting overlapping implementations that feels relevant here |
There's also my comment here quick relevant part:
Other than this not checking for compatibility between operands at the time of use (consistent subtyping, we should assume it from assignability), and only needing to check that use is compatible with each operand individually, this should align with how rust does this, and align with a general expectation of "I specified being compatible with each of these" |
Yeah, but there's still a problem with that here: class A:
def foo(self) -> None:
...
class B:
def foo(self, wait: bool = False) -> None:
...
def f(x: A & B):
x.foo() # fine
x.foo(wait=True) # not fine, not consistent with A.foo? But something consistent with A.foo and B.foo should allow this. I think this shows that we have to check that overlapping attributes and methods have compatible overlap and determine what that compatible overlap is. We can't split assignment from use without first calculating a compatible overlap. This means that #5 actually does need to be a type checking concern and mandated. This behavior needs to be part of the spec. We also shouldn't arbitrarily pick a class, or try to determine what the mro would need to be, this is an intersection, not a direct subclass. someone could inherit from both and reconcile in a way that would be impossible without further additions than just these as base classes class A:
def foo(self) -> None:
...
def bar(self, wait: bool = False) -> None:
...
class B:
def foo(self, wait: bool = False) -> None:
...
def bar(self) -> None:
... This example shows that anything there are cases that would need additional reconciliation, even as just a subclass, let alone an intersection. |
Going from that minimal overlap calculation, here would be some of my expectations
But in the above, we could modify it only slightly and also have a solvable case:
we also have to consider names as part of the api here when discussing something being compatible with both
|
@DiscordLiz When we take the literal definition of meet (=Intersection) and join (=Union) from partially ordered sets, then the meet/intersection is by definition the greatest lower bound Definition:
Lemma:
In the example you have given, therefore, class C(A,B):
def foo(self, wait: bool = False) -> None: ...
def bar(self, wait: bool = False) -> None: ... which is a valid subclass of both |
@randolf-scholz yes, that's exactly what I was getting at with that example, but also pointing out that Typescript's approach of just picking one side would never work for that case. I didn't feel I needed to spell that out how it was possible to resolve, especially in the presence of prior conversation and further examples. |
Regarding overlap violation, I think this is really complex since it depends on function signature subtyping, which needs to take into account the 5 different argument kinds possible in python: |
I don't think this makes it more complex, at least not much. We can say that
* There is a way to make a signature that does this and is compatible as a method of a subtype. I think we should just say that for the purposes of this, we handle each group individually, then check on handling points 4 & 5. While point 2 is stylistic in choice, rather than having a direct functional reason, I'd also rather not change library author's intent by intersecting their type with someone else's. Additionally, if the same name shows up in different groups across callabled, it might be a stronger indication that they aren't used the same way and shouldn't be treated as compatible. Not allowing movement between groups (1-3) allows a simple solution that does not need to consider these groups, but instead operate on each of them independently and check that the total signature is valid at the end. |
I don't think it's a good idea to have an exception to the rule. I think we should have a principle that changing any annotation from Any & Callable[[T1, T2, ..., Tn], R] = Callable[[T1, T2, ..., Tn], R] then it could create errors even though substituting a type for It's the same for the middle ground option. I think it must be that: Any & Callable[[T1, T2, ..., Tn], R] = Callable[..., R] I don't think it's a good idea to get into the weeds about "signature compatibility". The rule for calling The key idea is that just because Therefore, let the result type of calling
Now, examine the various cases based on these rules:
class A:
def f(self) -> RA:
return 1
class B:
def f(self, *, x: int = 1) -> RB:
return 1
# (A & B).f() = RA & RB
# (A & B).f(x=1) = RA & RB |
Can you explain this a bit? Why is it not |
This is part of the type. We have to have rules to resolve this. Ignoring the parameter specification does not work, examples of this above. We only know a minimum bound |
@DiscordLiz In your example the issue of "compatible overlap" can actually be decoupled from the issue of working with paramspecs. We can restate the problem as follows: class EmptyCall:
def __call__(self): ...
class WaitCall(EmptyCall):
def __call__(self, wait: bool = ...): ...
class A:
foo: EmptyCall
bar: WaitCall
class B:
foo: WaitCall
bar: EmptyCall Here we used our domain knowledge of paramspecs to claim that all functions with a signature def foo(x: A & B):
x.foo.__call__(wait=True)
# we know x must be a B hence x.foo is known to be a WaitCall hence we can use its "method"
x.bar.__call__(wait=True)
# we know x must be an A hence x.bar is known to be a WaitCall hence we can use its "method" |
@mniip If |
@randolf-scholz if |
@randolf-scholz your overloads there are incorrect, but it will still be complex and there is no way around this @erictraut brought concerns up with this in #5, and unfortunately we can now show this is necessary. We can't fully express the true type here without a |
So, we need a The problem here comes from the following: (A) -> A & (B) -> B There is something which is consistent with both, that being (T) -> T, for T: A XOR B The equivalent overload set would be (overload) (T) -> T, T: A & Not(B) If A&B is passed in place of T, there is no return value consistent with the intersection of callables. While the function might be a passthrough of type and result in A&B, we can't know this to be the case. This matters for typechecking usage in functions receiving an intersection. XOR cannot be expressed without negation of some form, the easiest way would be Current type theory would suggest that Not is only valid for Static Types. I would thus recommend the following behavior: If a gradual type with disjoint paramters is encountered in an intersection of callables, we have to widen it to the widest callable and lose type information. We could reject it, but this goes against gradual typing. For all disjoint static type paramter lists, we can create what is a restricted overload set that explicitly disallows anything which would create a problem with resolving a return type as ambiguous use.
|
My point is that I think it should be possible to assess both the validity of the call and its return value (which is all you need) without synthesizing the entire interface.
I'm not convinced of that. I think it's: I think you can check this by assuming that the intersections |
Unfortunately, this doesn't work. Rust's overlapping trait implementation resolution ran into a similar, yet different thing too, and they showed there were some cases where it was impossible to determine which implementation should be used correctly. There are some parameters that we can't determine the correct return type for without more information than what the intersection provides, we can exclude those using the method @DiscordLiz explained above, either with bound type variables, or with overload sets. Personally, I like the succinctness of the type variable method of consolidating them, but it may be less clear than the overload set for some people, and they are equivalent.
Where does this assumption come from? This is only possible to assume if there are class conflicts between intersection operands, and that these are concrete classes and not protocols. |
I was typing something more than that, but instead, just a slight clarification to what @mikeshardmind just said above
it isn't just this. (A&B) -> A is inconsistent with (A) -> A. class ParamA:
...
class ParamB:
...
class ParamAB(ParamA, ParamB):
...
class A:
def foo(self, x: ParamA) -> ParamA:
...
class B:
def foo(self, x: ParamB) -> ParamB:
...
class AB(A, B):
@overload
def foo(self, x: ParamA) -> ParamA:
...
@overload
def foo(self, x: ParamB) -> ParamB:
...
def foo(self, x):
if isinstance(x, ParamA):
return ParamA()
else:
return ParamB()
def fn(x: A & B):
x.foo(ParamAB())
# if x is AB, this results in ParamA which is inconsistent with B.foo
# even though AB.foo is consistent with A.foo and consistent with B.foo |
I'm not convinced it's worth giving up type consistency to pick up always exceptions, or that it's plausible in many cases. That said, in this case, it could relatively early be picked up when you implement a subclass of A and B. If the type checker is working correctly, it'll require you to have your information that includes consistency with |
Sorry, I meant to say the order of overloaded intersections. Within each part of the intersection which has overloads, the order is of course important. I thought the order of the intersection was what you were taking about from the context, but correct me if I may have misunderstood. |
Normally I would agree, but I think this is a case where the two possible handlings are mutually exclusive, so we should have a way to express which one we intend.
There are, but I'm getting sick of this discussion if you attempt to summarize it, I'll revisit for any needed corrections later. |
If we can't remove the order dependency, then we can't have consistent handling for an intersection between two things that both have overloads. How does the intersection determine which operand's overloads are "first"? Do we require intersections to be ordered? Restricting what is "knowable", and implicitly handling the disjointedness removes the ordering concern and allows normal algebraic operations to function, something I would consider a non-negotiable feature. This doesn't need to be exposed to users as a type they can use, but I think I agree with @DiscordLiz that users should be able to express with This lack of well-ordering and resolving what is safe with multiple definitions has prior art and requires that we can show that interfaces are either disjoint or specializations of each other. |
There are precisely
What is not covered is how you would synthesize a compatible subclass of |
This does not work, If you still do not understand why from my earlier comment about "well ordered overloads" necessitating an ordering on intersections, then please wait until more details explaining this are added to #17. A lot of work went into proving the necessity of this, and there is prior art also showing the necessity of this in a static typed environment. This is going to take some time to explain in proper detail with formal proof. |
Note that the linked rfc is about dispatch for multiple implementations, not about type compatibility. Dispatch needs to be unambiguously ordered because only a single implementation should get called. That doesn't apply for Type compatibility. Wrt to your other points I'll wait for #17 to be fleshed out as requested. |
Rust's method of dispatch on implementation is about unambiguously selecting an implementation based on type compatibility and specificity of the implementation. There's a subtle relation, and I acknowledge it is not 1:1, but it is a useful framework for correctly determining the most accurate/specific overload or intersected implementation for a given parameter list* We then have the return type (This is "to what end") of that overload or intersected implementation as our most specific known knowledge. (rather than dispatching to that, it still only goes to whatever is on the mro of the type) |
I don't believe that is necessary or useful. More precisely it may be useful as part of a type checking implementation, but it isn't necessary as part of the specification. |
If we don't specify this, it can diverge between type checkers, which is not an acceptable outcome with library use. |
Something I found when implementing my simulator - I've been thinking that Callable & Callable would become an overload of class A:
def __call__(self, x: int) -> int:
...
class B:
def __call__(self, x: str) -> str:
...
(A & B).__call__ But I've now realised the call method isn't quite analogous to: Callable[[int], int] & Callable[[str], str] Because in the above the argument isn't named. It's kind of like My conclusion from this is maybe it's a different beast, that behaves similarly - so it still clashes like overloads would etc, but it's not in itself an overload. |
@mark-todd You probably use Callback-Protocols in your simulator, instead of class Call_A(Protocol):
def __call__(self, x: int) -> int:
...
class Call_B(Protocol):
def __call__(self, x: str) -> str:
...
(A & B).__call__ # Call_A & Call_B Simplifying Example@overload
def f(arg: A) -> U: ...
@overload
def f(arg: B) -> V: ...
@overload
def g(arg: S) -> X: ...
@overload
def g(arg: T) -> Y: ... Then
Which can be translated into the following equivalent set of 8 overloads (without using (A & S) -> (U & X)
(A & T) -> (U & Y)
(B & S) -> (V & Y)
A -> U
S -> X
(B & T) -> (V & Y)
B -> V
T -> Y You can verify this by drawing a 4-component Venn diagram: It should be possible to give a tight upper bound for the number of needed overloads, I'll think about this over the holidays. EDIT: It's actually quite straight forward. If |
Since def __call__(self, x: int, /)... |
For now I've implemented something separate in the simulator for the Callable type, but it follows the same logic as class A:
def __call__(self, x: int, /) -> int:
pass
a = Intersection[A, Callable[[str], str]] I suppose if the forward slash makes it positional only that's comparable, but if I'm to make one overloaded method, what's the arg name? I suppose it could take the name from the side that does have a name to produce: Overload[(self, x: int, /) -> int, (self, x: str, /) -> str] |
Where does that notation come from? Are you just making something up? I don't think it was in the callable signature PEP 677, though during its development we considered something like this. I'm also confused by this, since in the example neither side has a name:
|
I could be wrong, but I believe this is how pyright shows method types when you inspect them - if the method is overloaded it uses the notation I used here.
When I say name I mean |
Okay, that's hardly canonical. :-)
But the name |
Yeah that makes sense - I'm not sure if Self should be there really, as like you say in method form it's not really an input arg. So let's say we switch to: Is there a canonical type for overloads? I've seen pyright use Radical thought perhaps but if there isn't such a notation do we need to introduce one? It could be: Edit: Follow up thought - do methods have a different type from Callable's generally? It's presented differently in pyright but I'm not sure this changes anything about the type as such. |
On the below I get a type error: from typing import Callable, overload
class A:
@overload
def foo(self, x: int) -> int:
...
@overload
def foo(self, x: str) -> str:
...
def foo(self, x: int | str) -> int | str:
return 1
x: Callable[[int | str], int | str] = A.foo
Edit: Perhaps stranger still, this also fails: from typing import Callable, overload
@overload
def foo(x: int) -> int:
...
@overload
def foo(x: str) -> str:
...
def foo(x: int | str) -> int | str:
return 1
x: Callable[[int | str], int | str] = foo With error:
|
On closer inspection, I think I've worked out what's going on here (at least in pyright). Interestingly enough, I have a feeling that the type of foo is already basically an intersection in it's current implementation: from typing import Callable, overload
@overload
def foo(x: int) -> int:
...
@overload
def foo(x: str) -> str:
...
@overload
def foo(x: int | str) -> int | str:
return 1
def foo(x: int | str) -> int | str:
return 1
x: Callable[[str], str] = foo The above returns no errors - and interestingly, if I make the final line: x: Callable[[int], int] = foo or x: Callable[[int | str], int| str] = foo These also return no errors. Since all of these are acceptable, I propose that the type of foo is effectively already: |
@mark-todd overloads are order-dependent and thus generally not equivalent to intersections. In your example, this is somewhat masked by the fact that one cannot define a nominal subtype of the built-ins @overload
def foo1(x: X) -> X: ...
@overload
def foo1(x: Y) -> Y: ...
@overload
def foo2(x: Y) -> Y: ...
@overload
def foo2(x: X) -> X: ...
foo3: Callable[[X],X] & Callable[[Y], Y] All describe different behaviors. |
@randolf-scholz Ah yep apologies I remember previous discussions about ordering in Overloads now - in that case I think we're back to the Overload[Callable[[int], int], Callable[[str], str], Callable[[int | str], int| str]]] |
I have to admit I don't know what you're trying to accomplish here (didn't look at the simulator PR) and I don't know your constraints, but that's not an accurate representation of that intersection type, right? In |
I mentioned this in discord earlier, but when trying to represent an intersection of callables with the simplest equivalent overloads, the ordered list for the simplest case
is
The intersection form should be prefered rather than expanding it to this. |
I'm tentatively closing this one. I believe the consistency based rule we are aiming for ends up solving this sufficiently, can be reopened if there are new relevant issues to this topic that would benefit from being continued here. |
In this issue, we shall discuss intersections with
Callable
. There is an unresolved issue with respect toAny & Callable
, that stems from the following 2 axioms:Callable
are resolved by intersecting with an equivalent Callback-Protocol (see current draft)Any
within an Intersection #1 (comment))Both of these together can lead to infinite regress.
Therefore, we cannot use ① when intersecting function-types with function-types. One can distinguish 3 cases:
Any
EDIT: The suggestions below are outdated. The intersection with
Any
is irreducible. What needs to be discussed is what happens when the type is attempted to be evaluated with argumentsargs
.As I see it, there are 2 options of how to resolve ③:
Ⓐ For a strict interpretation of
Any
as an unknown type,Any
could feasibly beCallable[..., R]
, which is a "consistent" subtype ofCallable[[T1, T2, ..., Tn], R]
. It follows that:The consequence is that
(Any & T).foo(*args, **kwargs)
, is valid for any methodfoo
ofT
, which as expressed in the Any intersection thread causes some pains, as it makesAny & T
behave very similar toAny
itself (only attribute types and function return types are preserved)Ⓑ An alternative approach would hinge on a slight re-interpretation of
Any
in the context of intersections. One could demand thatAny
shall be interpreted as a disjoint type from whatever it is intersected with (= maximum compatibility). That is, inAny & T
, we interpretAny
as an unknown type that presumably shares no overlapping methods withT
. This leads toI.e. we come back full circle to question if
Any
can be simplified away from intersections. Under this premise, we would have 3 simple rules, as I mentioned in #1 (comment)Any & T
is an irreducible form(Any & T).foo
≅T.foo
ifT
implementsfoo
(Any & T).bar
≅Any
ifT
does not implementbar
So, does it make sense to have a general exemption to the rules #1 (comment) when intersecting
Any
with function-types?The text was updated successfully, but these errors were encountered: