You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I don't really think this needs its own issue. We can detect some cases where an intersection is impossible to satisfy, and that should result in Never, I'm not sure why this would be something requiring any amount of bikeshedding.
Reacted by Ruan Comelli, diabolo-dan and Randolf Scholz
I'm not in a position to do anything formal at the moment, but that said I already posted a partial list of "trivial" reductions in the discord server, I'll post them here as well.
Note, removal of Any was included prior to some people finding that controversial, don't read into it as a mandate that this approach is the resolution
Trivial Removal of Any
Any & P -> P
Any & P & Q -> P & Q
Subtype relationship example
(copied directly from draft, already included)
(Note: examples for Any above also follow this rule of more specific types taking precedence)
Intersection[str, Employee, Manager] is Intersection[str, Manager]
concrete types which fully satisfy protocols
SupportsIndex & int -> int
Reductions involving None
None & ConcreteType -> Never
None & ProtocolNoneDoesntSatisfy -> Never
None & ProtocolNoneSatisfies -> None (ie. bool)
Interaction with other Final types
(Note: None follows all of these rules, no special casing of None)
FT is a final type
NBFT is another type that isn't in FT's bases
BFT is a type that is in FT's bases
SFTP is a protocol (heh) that FT satisfies
NSFTP is a protocol that FT does not satisfy
FT & NBFT -> Never
FT & BFT -> FT
FT & NSFTP -> Never
FT & SFTP -> FT
In addition to this post, there's also if you have two types with incompatible interfaces -> Never as it would be impossible to satisfy both requirements requested by use of the intersection. I don't think artificially creating overloads works, for reasons above, complexity, and so on. It also behaves more like a Union at that point, so if you want a Union, just use a Union.
In addition to this post, there's also if you have two types with incompatible interfaces -> Never as it would be impossible to satisfy both requirements requested by use of the intersection. I don't think artificially creating overloads works, for reasons above, complexity, and so on. It also behaves more like a Union at that point, so if you want a Union, just use a Union.
That's where we disagree.
Creating overloads is actually one use case for intersections. I.e. think of Callable[[int], str] & Callable[[float], [str].
People already said that would expect an overload there.
Of course the special cases about staticmethods and classmethods are non trivial and need some evaluation.
The specification is also stricter on allowable type combinations than what is required by python. It is possible to have multiple inheritance from multiple builtin types without it being in error. This is why my post was specific to mention type compatibility as well as if a class was marked as being final
The specification is also stricter on allowable type combinations than what is required by python. It is possible to have multiple inheritance from multiple builtin types without it being in error. This is why my post was specific to mention type compatibility as well as if a class was marked as being final
I should have been so much more specific. There is no rule in the interpreter or at runtime that multiple inheritance from builtin classes is impossible. The specification implies this off it being true for the current types there, but one can imagine that it may not remain true. It should be sufficient, more succinct, and more permanently correct to say that A & B is not valid for concrete types if class(A, B) is not valid.
Anyhow, if you are resolving this by adding overloads, I'm no longer interested in intersections. I consider this to be antithetical to why I want an intersection in python. Everything else there's been disagreement about I could see multiple paths out of, but this would result in me just not using the feature ever. It would be more correct to just hand out protocols that specify exactly my intent at that point.
If I specify A & B where A is mine, and B is a library's, I expect that A & B are out-of-the-box not incompatible interfaces. Hiding the incompatibility with artificially inserted overloads that then have to be checked for an outcome when used breaks expectations and some of the reasons for Intersections. I want to be able to use this as if it is A and as if it is B. If I wanted to check which interface I had, I wouldn't need an intersection.
Well the correct definition would be A & B is never if class (A, B) or class(B, A) raises TypeError.
There are two Problems with this definition:
Performance: You need to check all permutations of all arguments
It requires running the code what a type checker never should do (strongest arguemt)
How should type checker not implemented in python know this? And there are even multiple implementations of python next to CPython. So maybe in one of this implementation class (int, float) maybe even works. So typing will now depend on the interpreter?
The type error here is predictable and arises from a base class layout conflict. This can be statically determined and does not require running the code.
All permutations of arguments should be checked, it shouldn't be possible to create an impossible requirement.
Realistically, though, this goes back to what was brought up in discord by @DiscordLiz that even maintainers of type checkers thought intersections on anything other than protocols would be too complex.
pragmatically speaking, it's worth just disallowing multiple inheritance of builtin types. The manner in which they are implemented would need to change for this to no longer be true, and other implementations could allow it.
you do need to verify that a combination of types is possible, which would be checking that there exists at least 1 valid permutation of bases.
Really should just have intersections be for fully compatible protocols only. It's simple, and and solves a real problem. All of these edge cases come in from things nobody should ever need to care about in practice, but for it to be defined robustly and allow more than protocols, do.
I read through the current specification, and I need to state more than just simple agreement that the overloads are a mistake. This creates a situation where intersections do something that could never be valid on real classes for protocols, and only for protocols. Protocols are already only a definition structurally, I would expect any incompatibility to be a mistake on the part of whoever requested that something works with both.
You can't hack this together for real classes, because it would become an LSP violation. This breaks symmetry between structural and nominal typing.
Reacted by James Hilton-Balfe, Tomas R. and Michael H
Regarding overloads, these are not the same as intersections. The two should not be conflated. Overloads have complex signature matching rules and are order dependent. Intersections have simple rules based on set theory, and are order independent. I would be surprised if the word "overload" appeared anywhere within this PEP.
The subtyping rules for intersections should build upon existing subtyping rules within the type system. Type checkers already have rules in place for evaluating subtyping relationships for functions and overloads. The same is true for protocols, nominal classes, generics, etc. This PEP should not attempt to define these existing rules. It should simply explain how intersections work with respect to these existing subtyping rules. This will simplify the PEP and help ensure that it composes well with existing type features. If the PEP attempts to define all of the behaviors in terms of specific cases ("if an overload is involved..." or "if a protocol is intersected with a nominal class..." or "if a nominal class is intersected with Any"), the complexity of the spec will explode and inconsistencies and omissions will result. I therefore encourage the authors to stick to defining intersection rules that leverage existing generalized rules within the type system.
Regarding "impossible" intersections, my recommendation is to leave it up to each type checker to decide whether to detect such impossible conditions and where such conditions should be flagged as an error (e.g. at the point where the type is "spelled" as an annotation, where it's evaluated, or where it's used to evaluate type compatibility). I don't think the PEP should mandate such errors — or even express an opinion as to whether such errors should be reported. There are many reasons in Python why an intersection type may not be realizable without generating type checking or runtime errors. Some of these conditions are quite expensive to check for. Here's a partial list off the top of my head:
Classes that are explicitly marked @final
Certain builtin classes that are implicitly @final
Classes that generate MRO conflicts when combined
Classes that generate metaclass conflicts when combined
Conflicts involving __slots__
Certain builtins that cannot be combined
Generic classes whose specialized type arguments conflict
Classes that define the same attribute with conflicting types — those that result in a Never when intersected
Type checkers today detect a subset of these conditions when evaluating a class declaration with multiple base classes, but many of these conditions are not flagged as errors. Here are some examples:
classA(int, str): ... # Runtime error, but not currently flagged as error by mypy or pyrightclassB(list[str], Sequence[int]): ... # Flagged as error by pyright in strict mode, no error in mypyclassP1(Protocol):
a: strclassP2(Protocol):
a: intclassC(P1, P2): # Both mypy and pyright generate an error here
...
In practice, I think that we'll find that most of these "impossible intersection" cases occur very rarely (if ever) in real code. If some of these cases do come up more often, users will report these cases, and type checker authors can decide if it makes sense (based on tradeoffs like implementation complexity and runtime costs) to check for that specific condition. So my preference is for the PEP not to say anything about "impossible intersections" or simply state that "type checkers may (but are not obligated to) check for certain conditions where an intersection type cannot be realized at runtime".
Reacted by Neil Girdhar, Sebastian Law, diabolo-dan, Randolf Scholz and Omar Valdez
@CarliJoy I think @DiscordLiz has provided a much clearer explanation of why even though A.foo & B.foo = Never, that doesn't mean C.foo can be defined to depend on Never over here I also think you are correct when you said that discussion may need to wrap up before this one.
Some code to go with the prose she wrote:
int# singular static typeclassA: ... # singular static typeclassB: ... # also a singular static typeABAlias=A&B# *also* a singular static typeAny# This is the top type, and could be anything. This is not a singular type.Never# This is the bottom type, and can't be anything. classSomeClass:
foo: ABAlias# This is a type specification, spelled with a singular type, but this is not a singular type!# As an annotation, this allows the set of all potential types which are also A & B# and of which until further inference happens, is only safe to use what is provided by A&B.# Never doesn't provide A&B, so allowing this would violate LSP, even if Never was possible to exist!defx() ->Never: # Never isn't a singular type, it's the absence of a type being returned at all!defy(foo: Never): # Because There are no types which are never, this code isn't callable.
@randolf-scholz I think you hit the nail right on the head for the current issues with Never and LSP. This is a good formulation and good example of the desirable properties of LSP that are broken with the currently accepted definitions. My only qualm with layering on an exception instead of changing the definition, is that it appears to me that they have the same effects on all currently valid code. With this being the case, changing the rules to match those of the definitions which don't have the bottom type participate in subtyping freely gives us what is correct in more things which could be added to python later, as there are other features of type systems which are provably correct with those definitions, including rules for how they compose, that we can freely take in the future as they are proven already if we take the definition for the bottom type from the set-theoretic view.
@CarliJoy It's basically that if a type relies on the existence of Never (needs an instance of Never to exist for it to exist), the type itself can't exist. I think we need to wait on the outcome of the wider typing discussion on Never, because a definitive statement there could remove this from being the concern of this PEP or not depending on how strongly worded the definitive statement is.
And @CarliJoy following up on @mikeshardmind's above example there's also A | B, which is a set of static types. In an annotation, the annotation allows the set of all possible types that can claim to be members of {A, B} by substitutability, which is a possibly wider set of types defined by a subtyping relation to a set of types. I believe you [Michael] were aware of this given your wording in the discussion in python/typing, but it's worth mentioning for completeness.
that forbids to substitute a function with another function that unconditionally raises if the original didn't.
I also don't see what this has to do with LSP-exception since you don't know whether the superclass method raised the exception that the child class method is unconditionally raising. I also don't see why there's anything wrong with subclasses raising unconditionally where their superclasses don't. That already happens in ordinary code.
Is there any progress towards resolving the top level topic, which is "should reduction to never be mandated?"
Yes, if you don't mandate reduction, then assert_never won't do what you want it to. Is there any evidence that many people will use it to test whether two interfaces are entirely compatible? What seems more like is that people will inherit from two interfaces and write tests for the various functions, and in those tests, it will come up that there are type errors. That is tested without mandated reduction.
I think ultimately, if you want to mandate this behaviour, then given that there are significant runtime and implementation costs, those will have to be justified with real world examples of bugs that would be caught by not reducing—in order to be convincing to the people reviewing the PEP.
Yes, if you don't mandate reduction, then assert_never won't do what you want it to. Is there any evidence that many people will use it to test whether two interfaces are entirely compatible? What seems more like is that people will inherit from two interfaces and write tests for the various functions, and in those tests, it will come up that there are type errors. That is tested without mandated reduction.
It doesn't actually matter if we think they will or not. It's been confirmed that if intersections get added, they may end up in inference inside of type checker internals. We can't build this to be knowingly incompatible with other typing features that are supposed to work everywhere, especially with this being the only one of those with actual runtime behavior associated. assert_never is not for writing tests, it's for exhaustive matching against types in runtime code, and getting the type checker to confirm you actually exhausted all possible types in your handling. Getting this wrong has runtime impact as it causes assertion errors. (and worse, silent failures in runtime code using -O)
However
Is there any progress towards resolving the top level topic, which is "should reduction to never be mandated?"
Somewhat, and related to the above, this and #17 are both pending discussion here python/typing#1458
There are 5 outcomes for that that I can forsee, and 3 of them leave us able to restrict mandating when intersections need to be resolved from "a lot of places" to "only when the existence of Never is specifically checked for" (Which is currently only typing.assert_never) and remove the need for Not as a requirement, and instead turn it into a nice addition. 1 of the remaining 2 options also makes the rules for Not immediately obvious, and therefore non-expensive, both in terms of PEP language and type implementation.
@DiscordLiz Also came up with a slightly broader set than this which would be needed in the remaining 1 case here
We're quite close to being able to close much of the controversial issues with intersections and focus on picking how much needs mandating (And presenting good arguments for it) based on clearing up a couple of foundational details where some behaviors aren't well defined in python PEPs
I think ultimately, if you want to mandate this behaviour, then given that there are significant runtime and implementation costs, those will have to be justified with real world examples of bugs that would be caught by not reducing—in order to be convincing to the people reviewing the PEP.
Will do, and I'm making a conscious effort to make sure we mandate the bare minimum actually necessary in light of these costs., as well as opportunity costs where this interacts with potential future features. If it ends up the assert_never case is the only case, type checkers will almost never encounter it and can defer the reduction until reaching an intersection passed to assert_never, rather than needing to reduce it eagerly. This makes the cost directly proportional to the number of places user code specifically is asserting that something is Never and that the type checker should check this is true, and that the intersection survived other type inference removals during the user exhausting types. (otherwise it won't be part of the type passed in)
We're quite close to being able to close much of the controversial issues with intersections and focus on picking how much needs mandating (And presenting good arguments for it) based on clearing up a couple of foundational details where some behaviors aren't well defined in python PEPs
That's good to hear.
If it ends up the assert_never case is the only case, type checkers will almost never encounter it and can defer the reduction until reaching an intersection passed to assert_never, rather than needing to reduce it eagerly.
Sounds good. (And really they don't even need to get assert_never right in my opinion. It would just mean that you can't use assert_never with intersections and expect that type checkers are checking that every method of the interface is compatible.)
Somewhat, and related to the above, this and #17 are both pending discussion here python/typing#1458
I'm not sure exactly what you are looking for to actually resolve that issue, but hopefully it is resolved to your satisfaction soon.
Actually, I'm going to go ahead and preemptively close #17. If it ends up needing to be reopened, I'll reopen it, but it seems the least likely case after we cleared up some other discrepencies.
I'm not sure exactly what you are looking for to actually resolve that issue, but hopefully it is resolved to your satisfaction soon.
@NeilGirdhar We just need a clear answer from type checkers on "Is it intended that this is allowed, and are we sure this is the behavior we want to go with for handling Never and subtyping given a few issues with that"
Right now the answer to the first half of that is yes, the second we don't have an answer to yet. There's been a few things shown where mypy has had user complaints with the current behavior actually not being expected or causing other issues, and there's a statement that we need to investigate the impact of actually changing this, which I'm hoping to have the time to do later today myself.
If the answer is yes to both, then we can start from what Liz had as a very slim set of cases where type checkers would need to.
If there is a willingness to make a slight modification on Never's behavior on the second, (specifically where we can't have attributes be Never (or replace a method with an attribute that is Never) and a class be valid, but we can have parameters be Never and only error if initialized), then we only need to check in typing.assert_never and we don't even need to mandate it in that case anymore, only define the reductions and leave it to type checkers (it can no longer leak out of library code poorly in that case).
There are a few other outcomes on the second question possible, but that's the most likely one if there is going to be a change in my opinion as it is the most minimal in its potential disruption of existing code while addressing the "safe substitution" concern.
In the mean time, I've started summarizing all of what we've discussed so that in any outcome we have a nice record of what was and wasn't considered for the PEP, not sitting idle while waiting on the upstream outcome.
What was shunted over to python/typing has resulted in Eric saying we should formalize the existing type system prior to adding intersections. That said, there's a simpler case to show the problem presented here with Never without never, and a corresponding mypy issue going back to 2017.
In the case of
classA:
foo: int
foo should be invariant. This being resolved in type-checking implementations preempts the issue in this case from interacting with Never as str & int would not be invariantly compatible with str
Demonstrating this as an issue without Never:
classA:
a: intclassB(A):
a: booldeffoo(a: A) ->None:
a.a=2B().a=2# not okfoo(B()) # ok
This clearly isn't safe despite being (currently) allowed.
The above has been patched in pyright, is being patched in mypy, and pyre has also been made aware of it. Given that, and the general consensus that this was something that type checkers weren't checking, but was part of the specification over in the related discussion in python/typing, I believe that leaves us with the following:
Mutable fields must be invariantly compatible all across all operands of an intersection that provide the field or the intersection can't be satisfied.
This vastly simplifies any rules here as we don't need to intersect all the way down, we can simply check for conflict. This increases the arguability to reduce to Never as simple in the case of impossible intersections.
Bit late to the discussion so hopefully this isn't repeating anyone, but I think one consequence of reducing impossible types to Never is that the types C1: TypeAlias = Callable[[t1], None] | Callable[[t2], None] and C2: TypeAlias = Callable[[t1 & t2], None] are not equivalent, but if you treat such impossible types as unique types (even though they all share the property of having no valid values) then they are equivalent.
(Note: whilst I do have a maths background, it's been a while, so do let me know if there's a mistake in my logic 😉)
C1 is obviously a subtype of C2: if you have some function f that's a valid C1 then it's (only) safe to pass something that's both a t1 and a t2, aka t1 & t2. Hence f is also a valid C2*.
*
As long as you allow that `Callable[[Never], None]` is a valid type (it's the type of a callable that takes a single argument and returns None). You can't actually call it since you don't know what types it accepts, but you can do other operations that would be valid such as query its `__name__`, or introspect it to figure out what types it accepts and then call it with a valid type.
For C2 to be a subtype of C1, we could try to show that any g that's not a valid C1 is also not a valid C2. For g not to be a valid C1 there must be some type u1 that's a subtype of t1 that g cannot be called with (if no such type exists then g can be called with any subtype of t1 hence it's a valid Callable[[t1], None]. Similarly there must be some u2 subtype of t2 that g cannot be called with. The next step would be to argue that now u1 & u2 is a type that's a sub-type of t1 & t2 that cannot be passed to g**, and hence g is not a valid C2. This is where the argument diverges - if u1 & u2 can be Never, then this argument doesn't work. If u1 & u2 will always be a valid unique type (even if it might not have any valid values) then it does.
**
I've hand-waved over a step here - it's possible that some sub-types of u1 are valid for g, and same for some sub-types of u2, and the intersection u1 & u2 happens to yield a narrowed type that would actually be wholly valid for g. But this is basically the same argument again - you just narrow to u1_ = u1 & ~(u1 & u2) and u2_ = u2 & ~(u1 & u2) and use u1_ & u2_ instead, which once again only works if that intersection is not Never.
For an example of such a function g (abusing notation and glossing over the exact meanings of some operations):
This cannot be called with all A1 or all A2, so it's not a valid Callable[[A1], None] | Callable[[A2], None], but the "C2 version" would be Callable[[A1 & A2], None] and the u1 & u2 type would be B1 & B2 (which is "impossible" in CPython at least, but not actually invalid at runtime). You could also do this with
In this case Callable[[int & str], None] already contains such an invalid type, and the u1 & u2 type of Literal[0] & Literal[''] looks even more absurd, but... it does exhibit the potential problem with reducing int & str to Never - it's throwing away information. If you reduce Callable[[int & str], None] to Callable[[Never], None], then (as per * above) your type is now the type of all callables that accept a single argument (aka Union[Callable[[T], None] for T in TYPES]) and not just Callable[[int], None] | Callable[[str], None].
So I guess the question is, do you like this nice duality of union/covariance with intersection/contravariance, or do you dislike the potential absurdity of treating types like Literal[0] & Literal[''] as distinct from Never? Personally I think I lean towards the duality.
As for assert_never() - perhaps that indicates that we need two distinct concepts here: one is the bottom type (aka intersection of all other types) and the other is the set of types that have no valid values, which would be used as the type of arguments to assert_never() (and a lot of the discussion on python/typing#1458 seems to revolve around which of these is "correct"). As has been mentioned though, it might not always be obvious to a type checker when a type (eg generated by an intersection) is in this set, which is when the programmer might need to step in to help out.
Sidenote
The name assert_never() (and similarly assert_type()) seems slightly off to me - I would usually use and assertion when I need to tell the type checker something I know (hope?) to be true but that it can't infer/prove, not when I want it to check something. Maybe it should have a check: bool argument to specify which mode you want, though I guess the ship has sailed on the default value for that.
@mikeshardmind Thats because due to the ordered nature of our suggestion there are no conflicts when accessing in attribute, as the highest order is taken, correctly?
And when trying to assign an object to a value, it could simply be that no object ever could satisfy the condition.
Is that more or less correct?
Yeah. At assignment it needs to be compatible with all. The ordered nature for lookup means there's no reason to determine a minimum bound in the type system statically, and it basically gets handled when creating a type (being told the type violates other rules)
Activity
mikeshardmind commentedon Jul 24, 2023
I don't really think this needs its own issue. We can detect some cases where an intersection is impossible to satisfy, and that should result in
Never, I'm not sure why this would be something requiring any amount of bikeshedding.CarliJoy commentedon Jul 24, 2023
@mikeshardmind I already wrote an algorithm for protocols in the current specification under https://github.com/CarliJoy/intersection_examples/blob/main/specification.rst#protocol-reduction
Could you adopt this algorithm to accompany this?
There is already a section with evaluation to never, we could add things there, too.
But in this case I would like to define also, that type checkers should deliver a good error msg. Otherwise finding these issues will be pain.
mikeshardmind commentedon Jul 24, 2023
I'm not in a position to do anything formal at the moment, but that said I already posted a partial list of "trivial" reductions in the discord server, I'll post them here as well.
Note, removal of Any was included prior to some people finding that controversial, don't read into it as a mandate that this approach is the resolution
Trivial Removal of Any
Any & P -> P
Any & P & Q -> P & Q
Subtype relationship example
(copied directly from draft, already included)
(Note: examples for Any above also follow this rule of more specific types taking precedence)
Intersection[str, Employee, Manager] is Intersection[str, Manager]
concrete types which fully satisfy protocols
SupportsIndex & int -> int
Reductions involving None
None & ConcreteType -> Never
None & ProtocolNoneDoesntSatisfy -> Never
None & ProtocolNoneSatisfies -> None (ie. bool)
Interaction with other Final types
(Note: None follows all of these rules, no special casing of None)
FT is a final type
NBFT is another type that isn't in FT's bases
BFT is a type that is in FT's bases
SFTP is a protocol (heh) that FT satisfies
NSFTP is a protocol that FT does not satisfy
FT & NBFT -> Never
FT & BFT -> FT
FT & NSFTP -> Never
FT & SFTP -> FT
In addition to this post, there's also if you have two types with incompatible interfaces -> Never as it would be impossible to satisfy both requirements requested by use of the intersection. I don't think artificially creating overloads works, for reasons above, complexity, and so on. It also behaves more like a Union at that point, so if you want a Union, just use a Union.
CarliJoy commentedon Jul 24, 2023
I already included them in the specification. Did you have look at it?
CarliJoy commentedon Jul 24, 2023
That's where we disagree.
Creating overloads is actually one use case for intersections. I.e. think of
Callable[[int], str] & Callable[[float], [str].People already said that would expect an overload there.
Of course the special cases about
staticmethodsandclassmethodsare non trivial and need some evaluation.mikeshardmind commentedon Jul 24, 2023
I would expect this to be an error. If I wanted that, the correct tool is a Union, not an intersection.
Callable[[int], str] | Callable[[float], str]has the behavior you are putting into the intersection here by creating overloads artifically.mikeshardmind commentedon Jul 24, 2023
The specification is also stricter on allowable type combinations than what is required by python. It is possible to have multiple inheritance from multiple builtin types without it being in error. This is why my post was specific to mention type compatibility as well as if a class was marked as being final
CarliJoy commentedon Jul 24, 2023
That is not correct, see https://github.com/CarliJoy/intersection_examples/blob/main/test_basetypes.py I didn't find any combination that is valid.
mikeshardmind commentedon Jul 24, 2023
I should have been so much more specific. There is no rule in the interpreter or at runtime that multiple inheritance from builtin classes is impossible. The specification implies this off it being true for the current types there, but one can imagine that it may not remain true. It should be sufficient, more succinct, and more permanently correct to say that A & B is not valid for concrete types if class(A, B) is not valid.
mikeshardmind commentedon Jul 24, 2023
Anyhow, if you are resolving this by adding overloads, I'm no longer interested in intersections. I consider this to be antithetical to why I want an intersection in python. Everything else there's been disagreement about I could see multiple paths out of, but this would result in me just not using the feature ever. It would be more correct to just hand out protocols that specify exactly my intent at that point.
If I specify
A & Bwhere A is mine, and B is a library's, I expect that A & B are out-of-the-box not incompatible interfaces. Hiding the incompatibility with artificially inserted overloads that then have to be checked for an outcome when used breaks expectations and some of the reasons for Intersections. I want to be able to use this as if it is A and as if it is B. If I wanted to check which interface I had, I wouldn't need an intersection.CarliJoy commentedon Jul 24, 2023
Well the correct definition would be A & B is never if
class (A, B)orclass(B, A)raises TypeError.There are two Problems with this definition:
class (int, float)maybe even works. So typing will now depend on the interpreter?mikeshardmind commentedon Jul 24, 2023
The type error here is predictable and arises from a base class layout conflict. This can be statically determined and does not require running the code.
All permutations of arguments should be checked, it shouldn't be possible to create an impossible requirement.
Realistically, though, this goes back to what was brought up in discord by @DiscordLiz that even maintainers of type checkers thought intersections on anything other than protocols would be too complex.
DiscordLiz commentedon Jul 24, 2023
pragmatically speaking, it's worth just disallowing multiple inheritance of builtin types. The manner in which they are implemented would need to change for this to no longer be true, and other implementations could allow it.
you do need to verify that a combination of types is possible, which would be checking that there exists at least 1 valid permutation of bases.
Really should just have intersections be for fully compatible protocols only. It's simple, and and solves a real problem. All of these edge cases come in from things nobody should ever need to care about in practice, but for it to be defined robustly and allow more than protocols, do.
DiscordLiz commentedon Jul 24, 2023
I read through the current specification, and I need to state more than just simple agreement that the overloads are a mistake. This creates a situation where intersections do something that could never be valid on real classes for protocols, and only for protocols. Protocols are already only a definition structurally, I would expect any incompatibility to be a mistake on the part of whoever requested that something works with both.
You can't hack this together for real classes, because it would become an LSP violation. This breaks symmetry between structural and nominal typing.
erictraut commentedon Jul 25, 2023
A few thoughts...
Regarding overloads, these are not the same as intersections. The two should not be conflated. Overloads have complex signature matching rules and are order dependent. Intersections have simple rules based on set theory, and are order independent. I would be surprised if the word "overload" appeared anywhere within this PEP.
The subtyping rules for intersections should build upon existing subtyping rules within the type system. Type checkers already have rules in place for evaluating subtyping relationships for functions and overloads. The same is true for protocols, nominal classes, generics, etc. This PEP should not attempt to define these existing rules. It should simply explain how intersections work with respect to these existing subtyping rules. This will simplify the PEP and help ensure that it composes well with existing type features. If the PEP attempts to define all of the behaviors in terms of specific cases ("if an overload is involved..." or "if a protocol is intersected with a nominal class..." or "if a nominal class is intersected with
Any"), the complexity of the spec will explode and inconsistencies and omissions will result. I therefore encourage the authors to stick to defining intersection rules that leverage existing generalized rules within the type system.Regarding "impossible" intersections, my recommendation is to leave it up to each type checker to decide whether to detect such impossible conditions and where such conditions should be flagged as an error (e.g. at the point where the type is "spelled" as an annotation, where it's evaluated, or where it's used to evaluate type compatibility). I don't think the PEP should mandate such errors — or even express an opinion as to whether such errors should be reported. There are many reasons in Python why an intersection type may not be realizable without generating type checking or runtime errors. Some of these conditions are quite expensive to check for. Here's a partial list off the top of my head:
@final@final__slots__Neverwhen intersectedType checkers today detect a subset of these conditions when evaluating a class declaration with multiple base classes, but many of these conditions are not flagged as errors. Here are some examples:
In practice, I think that we'll find that most of these "impossible intersection" cases occur very rarely (if ever) in real code. If some of these cases do come up more often, users will report these cases, and type checker authors can decide if it makes sense (based on tradeoffs like implementation complexity and runtime costs) to check for that specific condition. So my preference is for the PEP not to say anything about "impossible intersections" or simply state that "type checkers may (but are not obligated to) check for certain conditions where an intersection type cannot be realized at runtime".
157 remaining items
mikeshardmind commentedon Aug 31, 2023
@CarliJoy I think @DiscordLiz has provided a much clearer explanation of why even though A.foo & B.foo = Never, that doesn't mean C.foo can be defined to depend on Never over here I also think you are correct when you said that discussion may need to wrap up before this one.
Some code to go with the prose she wrote:
DiscordLiz commentedon Aug 31, 2023
@randolf-scholz I think you hit the nail right on the head for the current issues with Never and LSP. This is a good formulation and good example of the desirable properties of LSP that are broken with the currently accepted definitions. My only qualm with layering on an exception instead of changing the definition, is that it appears to me that they have the same effects on all currently valid code. With this being the case, changing the rules to match those of the definitions which don't have the bottom type participate in subtyping freely gives us what is correct in more things which could be added to python later, as there are other features of type systems which are provably correct with those definitions, including rules for how they compose, that we can freely take in the future as they are proven already if we take the definition for the bottom type from the set-theoretic view.
@CarliJoy It's basically that if a type relies on the existence of Never (needs an instance of Never to exist for it to exist), the type itself can't exist. I think we need to wait on the outcome of the wider typing discussion on Never, because a definitive statement there could remove this from being the concern of this PEP or not depending on how strongly worded the definitive statement is.
And @CarliJoy following up on @mikeshardmind's above example there's also A | B, which is a set of static types. In an annotation, the annotation allows the set of all possible types that can claim to be members of {A, B} by substitutability, which is a possibly wider set of types defined by a subtyping relation to a set of types. I believe you [Michael] were aware of this given your wording in the discussion in python/typing, but it's worth mentioning for completeness.
CarliJoy commentedon Sep 1, 2023
Thank you @DiscordLiz and @mikeshardmind . I understand it now a bit better.
NeilGirdhar commentedon Sep 1, 2023
I also don't see what this has to do with LSP-exception since you don't know whether the superclass method raised the exception that the child class method is unconditionally raising. I also don't see why there's anything wrong with subclasses raising unconditionally where their superclasses don't. That already happens in ordinary code.
Is there any progress towards resolving the top level topic, which is "should reduction to never be mandated?"
Yes, if you don't mandate reduction, then
assert_neverwon't do what you want it to. Is there any evidence that many people will use it to test whether two interfaces are entirely compatible? What seems more like is that people will inherit from two interfaces and write tests for the various functions, and in those tests, it will come up that there are type errors. That is tested without mandated reduction.I think ultimately, if you want to mandate this behaviour, then given that there are significant runtime and implementation costs, those will have to be justified with real world examples of bugs that would be caught by not reducing—in order to be convincing to the people reviewing the PEP.
mikeshardmind commentedon Sep 1, 2023
@NeilGirdhar
It doesn't actually matter if we think they will or not. It's been confirmed that if intersections get added, they may end up in inference inside of type checker internals. We can't build this to be knowingly incompatible with other typing features that are supposed to work everywhere, especially with this being the only one of those with actual runtime behavior associated. assert_never is not for writing tests, it's for exhaustive matching against types in runtime code, and getting the type checker to confirm you actually exhausted all possible types in your handling. Getting this wrong has runtime impact as it causes assertion errors. (and worse, silent failures in runtime code using -O)
However
Somewhat, and related to the above, this and #17 are both pending discussion here python/typing#1458
There are 5 outcomes for that that I can forsee, and 3 of them leave us able to restrict mandating when intersections need to be resolved from "a lot of places" to "only when the existence of Never is specifically checked for" (Which is currently only typing.assert_never) and remove the need for Not as a requirement, and instead turn it into a nice addition. 1 of the remaining 2 options also makes the rules for Not immediately obvious, and therefore non-expensive, both in terms of PEP language and type implementation.
@DiscordLiz Also came up with a slightly broader set than this which would be needed in the remaining 1 case here
We're quite close to being able to close much of the controversial issues with intersections and focus on picking how much needs mandating (And presenting good arguments for it) based on clearing up a couple of foundational details where some behaviors aren't well defined in python PEPs
Will do, and I'm making a conscious effort to make sure we mandate the bare minimum actually necessary in light of these costs., as well as opportunity costs where this interacts with potential future features. If it ends up the assert_never case is the only case, type checkers will almost never encounter it and can defer the reduction until reaching an intersection passed to assert_never, rather than needing to reduce it eagerly. This makes the cost directly proportional to the number of places user code specifically is asserting that something is Never and that the type checker should check this is true, and that the intersection survived other type inference removals during the user exhausting types. (otherwise it won't be part of the type passed in)
NeilGirdhar commentedon Sep 1, 2023
That's good to hear.
Sounds good. (And really they don't even need to get
assert_neverright in my opinion. It would just mean that you can't useassert_neverwith intersections and expect that type checkers are checking that every method of the interface is compatible.)I'm not sure exactly what you are looking for to actually resolve that issue, but hopefully it is resolved to your satisfaction soon.
mikeshardmind commentedon Sep 1, 2023
Actually, I'm going to go ahead and preemptively close #17. If it ends up needing to be reopened, I'll reopen it, but it seems the least likely case after we cleared up some other discrepencies.
@NeilGirdhar We just need a clear answer from type checkers on "Is it intended that this is allowed, and are we sure this is the behavior we want to go with for handling Never and subtyping given a few issues with that"
Right now the answer to the first half of that is yes, the second we don't have an answer to yet. There's been a few things shown where mypy has had user complaints with the current behavior actually not being expected or causing other issues, and there's a statement that we need to investigate the impact of actually changing this, which I'm hoping to have the time to do later today myself.
If the answer is yes to both, then we can start from what Liz had as a very slim set of cases where type checkers would need to.
If there is a willingness to make a slight modification on Never's behavior on the second, (specifically where we can't have attributes be Never (or replace a method with an attribute that is Never) and a class be valid, but we can have parameters be Never and only error if initialized), then we only need to check in typing.assert_never and we don't even need to mandate it in that case anymore, only define the reductions and leave it to type checkers (it can no longer leak out of library code poorly in that case).
There are a few other outcomes on the second question possible, but that's the most likely one if there is going to be a change in my opinion as it is the most minimal in its potential disruption of existing code while addressing the "safe substitution" concern.
In the mean time, I've started summarizing all of what we've discussed so that in any outcome we have a nice record of what was and wasn't considered for the PEP, not sitting idle while waiting on the upstream outcome.
mikeshardmind commentedon Sep 8, 2023
What was shunted over to python/typing has resulted in Eric saying we should formalize the existing type system prior to adding intersections. That said, there's a simpler case to show the problem presented here with Never without never, and a corresponding mypy issue going back to 2017.
In the case of
foo should be invariant. This being resolved in type-checking implementations preempts the issue in this case from interacting with Never as
str & intwould not be invariantly compatible withstrDemonstrating this as an issue without Never:
This clearly isn't safe despite being (currently) allowed.
mikeshardmind commentedon Sep 17, 2023
The above has been patched in pyright, is being patched in mypy, and pyre has also been made aware of it. Given that, and the general consensus that this was something that type checkers weren't checking, but was part of the specification over in the related discussion in python/typing, I believe that leaves us with the following:
This vastly simplifies any rules here as we don't need to intersect all the way down, we can simply check for conflict. This increases the arguability to reduce to Never as simple in the case of impossible intersections.
QuantumTim commentedon Nov 20, 2023
Bit late to the discussion so hopefully this isn't repeating anyone, but I think one consequence of reducing impossible types to
Neveris that the typesC1: TypeAlias = Callable[[t1], None] | Callable[[t2], None]andC2: TypeAlias = Callable[[t1 & t2], None]are not equivalent, but if you treat such impossible types as unique types (even though they all share the property of having no valid values) then they are equivalent.(Note: whilst I do have a maths background, it's been a while, so do let me know if there's a mistake in my logic 😉)
C1is obviously a subtype ofC2: if you have some functionfthat's a validC1then it's (only) safe to pass something that's both at1and at2, akat1 & t2. Hencefis also a validC2*.*
For
C2to be a subtype ofC1, we could try to show that anygthat's not a validC1is also not a validC2. Forgnot to be a validC1there must be some typeu1that's a subtype oft1thatgcannot be called with (if no such type exists thengcan be called with any subtype oft1hence it's a validCallable[[t1], None]. Similarly there must be someu2subtype oft2thatgcannot be called with. The next step would be to argue that nowu1 & u2is a type that's a sub-type oft1 & t2that cannot be passed tog**, and hencegis not a validC2. This is where the argument diverges - ifu1 & u2can beNever, then this argument doesn't work. Ifu1 & u2will always be a valid unique type (even if it might not have any valid values) then it does.**
For an example of such a function
g(abusing notation and glossing over the exact meanings of some operations):This cannot be called with all
A1or allA2, so it's not a validCallable[[A1], None] | Callable[[A2], None], but the "C2 version" would beCallable[[A1 & A2], None]and theu1 & u2type would beB1 & B2(which is "impossible" in CPython at least, but not actually invalid at runtime). You could also do this withIn this case
Callable[[int & str], None]already contains such an invalid type, and theu1 & u2type ofLiteral[0] & Literal['']looks even more absurd, but... it does exhibit the potential problem with reducingint & strtoNever- it's throwing away information. If you reduceCallable[[int & str], None]toCallable[[Never], None], then (as per * above) your type is now the type of all callables that accept a single argument (akaUnion[Callable[[T], None] for T in TYPES]) and not justCallable[[int], None] | Callable[[str], None].So I guess the question is, do you like this nice duality of union/covariance with intersection/contravariance, or do you dislike the potential absurdity of treating types like
Literal[0] & Literal['']as distinct fromNever? Personally I think I lean towards the duality.As for
assert_never()- perhaps that indicates that we need two distinct concepts here: one is the bottom type (aka intersection of all other types) and the other is the set of types that have no valid values, which would be used as the type of arguments toassert_never()(and a lot of the discussion on python/typing#1458 seems to revolve around which of these is "correct"). As has been mentioned though, it might not always be obvious to a type checker when a type (eg generated by an intersection) is in this set, which is when the programmer might need to step in to help out.Sidenote
mikeshardmind commentedon Feb 21, 2024
I believe this is resolved as not to be enforced at the point of the intersection for the options we are considering
CarliJoy commentedon Feb 22, 2024
@mikeshardmind Thats because due to the ordered nature of our suggestion there are no conflicts when accessing in attribute, as the highest order is taken, correctly?
And when trying to assign an object to a value, it could simply be that no object ever could satisfy the condition.
Is that more or less correct?
mikeshardmind commentedon Feb 22, 2024
@CarliJoy
Yeah. At assignment it needs to be compatible with all. The ordered nature for lookup means there's no reason to determine a minimum bound in the type system statically, and it basically gets handled when creating a type (being told the type violates other rules)
CarliJoy commentedon Feb 23, 2024
Sorry I don't understand what this means (in detail).
I think I am confused again with structual/nominal typing etc.
But I think it is more productive to wait for the PEP draft and see I reading it I will get it and if not work together with you to reformulate it :-)