Repository navigation
Description
This is in pdf form for now because it was easier to work with locally. I'll have to translate this over to rst for the proposal process, and will do so soon.
I consider this almost ready to propose as-is. I'm looking for comments on which examples we should use (we have too many to use all of them) for the motivation section and whether any of the language remains unclear.
The scope has been narrowed down a bit, and sections have been re-ordered, re-worded, and clarified thanks to the first round of feedback received in other channels from @carljm @Jackenmen @DiscordLiz and @Sachaa-Thanasius
This incorporates all of the collected theory that we had agreement for, limits the definition of negation in such a way that user-denotable negation can be deferred to a later proposal, and avoids breaking the gradual guarantee.
Included alongside the theory are a procedural set of steps that are equivalent, yet that do not require set-theoretic type checker internal representations, and minimizes both false positives and false negatives to the minimum possible without breaking the gradual guarantee.
Not yet written:
- The step-by-step examples of attribute resolution/callable type resolution.
- Conformance tests
- appropriate user-facing documentation that does not require a strong theory background. This will be framed around "compatable use" and will contrast that Unions represent "compatible with at least one of", while Intersections represent "compatible with all of"
The first of those is a blocker for the proposal to be made formally; the other two are not, but will still need to be done as part of the process if this is to be accepted.
Activity
emmatyping commentedon Apr 20, 2025
Thank you for writing this up! I'll admit I haven't really been following a lot of the discussion for intersection beyond messages in the typing bug. So I apologize in advance if any of this has been discussed already.
First, I highly recommend that if this to become a PEP (which I expect it would), you should use the format of the PEP template in PEP 12: https://peps.python.org/pep-0012/#suggested-sections, and keep the section ordering. The current layout and ordering makes it hard to understand what is motivation vs specification vs other discussion.
Second, I don't see a discussion of the rules with intersections with
Any, which I think should be called out explicitly somewhere. Even ifAnyuses the non-trivial reductions, I think it is good to be clear about that.Third, I think the proposal needs to discuss changes to the language implementation, especially giving a name for the intersection type. While many (most?) people will probably use
&, some people will want to spell out the type.Finally, I think the section about value types and
Annotatedcould use some context. Right now it's not clear what annotated values have to do with intersections.mikeshardmind commentedon Apr 20, 2025
Most of this would fall under "rationale", with very little under "specification" and "implementation", the specification can be summed up as:
"Intersections are a means of expressing the subtyping relationship: C ⊆ A ∩ B ⟺ (C ⊆ A ∧ C ⊆ B) and all rules for them in the type system follow from existing subtyping rules."
The implementation is to be nearly identical to that of Union, with only differing names for symbols, and a different operator implemented.
Reasoning through the implications and ensuring all type checkers can reach the same conclusions here is the majority of the proposal, as this will require type checkers to reach the same conclusions here for this to be a feature that is useful to library authors no matter which type checker their users use.
While it can be reorganized under those headings, most of the existing headings would end up subheadings of rationale then, and I'm not sure how useful such an organization will be, but I'll see if there's a way to clear up which parts are for which audience. Type checkers need some information here that to users is almost certainly going to seem strictly academic.
The rules for Any apply the same as any other type, no special casing is required to handle Any, the reductions provided are just consequences of the above subtyping relationship. Hopefully the examples make this more clear, but that includes that intersections containing Any retain gradual behavior related to Any.
I believe that's covered under the section heading "Implementation", though I could specifically say typing.Intersection and types.IntersectionType rather than the wording there.
Agreed, this will need an example that highlights it. The type system shouldn't care about Annotated, only the type contained in it, but the recommendations there for those using Annotated to extend the type system beyond specification will ensure users end up with intuitive beahvior, and that current extensions that are essentially acting as refinement types are compatible with the set-theoretic understanding of refinement types, even without them being in the type system officially.
An example of this is the use of Annotated in libraries like msgspec and pydantic to constrain values
CarliJoy commentedon Apr 20, 2025
Thank you writing up the draft.
Could you explain what you mean by (un)inhabited code?
The draft is hard to read for me. So I am happily waiting for the not yet written parts, which make it more understandable for users not so deep in type theory :-)
DiscordLiz commentedon Apr 20, 2025
functools.lru_cache,functools.total_ordering, and an example with typed dicts and protocol composition.You also need an example with
Any, even though there aren't special cases because not everyone will intuitively follow how an why that functions as it does.Language seems fine. Theory section is very dense, but the audience for that section is type checker maintainers, so I think that's fine. the theory section could even just be an appendix of the pep since the audience for it is so narrow.
superbobry commentedon Apr 22, 2025
@mikeshardmind thank you for working on this! Could you upload the draft on Google Docs or make it a PR so that it is easier for people to ask questions/leave comments?
mikeshardmind commentedon Apr 22, 2025
@DiscordLiz The example for total ordering I intend to include is something like this:
I'll grab a real world example of improved typed dict composition from a library that handles typed-json payloads.
lru_cache is trivial (we've discussed that one before)
I'm not sure I want an example with
Anyin the motivation section, but I'll be sure this is included in one of the examples for examining types of attributes.mikeshardmind commentedon Apr 22, 2025
@CarliJoy See the section "Definitions", but it's essentially referring to a case where we can logically deduce that there are no possible runtime values, and that we've either exhausted all possible values (such as with exhaustiveness checking in match statements) or there is an error of some sort.
mikeshardmind commentedon Apr 22, 2025
@superbobry
I'm intending to move this forward to looking for a sponsor rather soon and am not currently looking for detailed line-by-line feedback, this is largely already the result of taking the time to distill down years of theory discussion to what we know to work, and what can be shown as working not just in python, but in other gradual type systems as well.
Ever since the definition of "Any" has been ammended in such a way that it is compatible with set-theoretic intersections (Any was updated not be a catch all, but more accurately a compatible unknown, you can read more about this in the sections on Gradual Types and Materilization in the specification), it has been possible to define intersections building on set-theory without special casing of Any.
I'll let you know when the RST form in standard PEP formatting is available if that's easier for you to comment on.
mark-todd commentedon Apr 23, 2025
This looks really good! A couple of things I noticed:
In the trivial reductions section I think we should add:
T & T = T. This seems to be assumed to be true for other things to check out.Perhaps also in the
callability and return typesection it should be "Start with an empty set", as I think otherwise if a type in the list is the same it doesn't collapse.Re
Any, I agree that the rules you've defined handle the case well, but it might be worth adding a line somewhere of "T & Anyis irreducible" just to spell it out.Also re negation, I think there are still quite a few outstanding questions so personally I would move it into the future work section. E.g. If a user has:
What is
~A? It seems to me this is effectivelyAny, but with the added restrictions that it cannot inherit fromA.B & ~Amust have attributebar, but what aboutfoo- perhapsint & ~str? And if~Ahas all other attributes asAny, does that mean(B & ~A).newhas typeAnytoo?carljm commentedon Apr 23, 2025
It is
object, but excluding all instances ofAand any subclasses ofA. There is noAnyinvolved. This is a pretty important distinction:Anyis notobject, and~Ais a fully static type.B & ~Ahas attributefoowith typeint. It would be incorrect to add& ~strto the type offoo. The fact that we cannot have a subtype ofAdoes not prevent an instance ofB(independently, without being an instance ofA) from havingfooof typeint & str. (Well, Python's runtime multiple inheritance semantics do prevent that in the specific case ofintandstr, but this is something type checkers don't currently understand.) In general, negated nominal types tell us nothing about the types of members.No, it has only the attributes of
object.mark-todd commentedon Apr 23, 2025
Ah ok this makes sense - thanks!
I hadn't thought about using
objectinstead ofAnyas the set of all other classes, but I think under this formulation the rest of it now works. Although....By this logic:
Bcould be considered a subtype of~A(it doesn't inherit from A, and inherits from object). Does this not imply thatA & Bis a subtype ofA & ~A(orNever), and we end up with a fallacy?mikeshardmind commentedon Apr 23, 2025
No, but that's something that needs expanding on for any work on user-denotable negation.
It's not possible to be a subtype of a negated type(B here is a subtype of object, and is not a subtype of A, placing it in the set of types that are not subtypes of A), but a type may be assignable to the resulting set of types. The distinction there is subtle enough that that alone is reason enough to defer user-denotable negation to a separate proposal.carljm commentedon Apr 23, 2025
Bis not a subtype of~A. The typeBincludes all instances ofBor any subclass of it. The type~Aincludes all objects which are not an instance ofAor any subclass of it. It is possible for aclass C(A, B)to exist (that is, a class that inherits from bothBandA.) Instances ofCinhabit the typeB, but do not inhabit the type~A. Therefore,Bcannot be a subtype of~A.Another way to put this is that for any types
TandS,Tis a subtype of~Sonly ifTandSare disjoint types: no object can possibly inhabit both of them. For two normal Python classesAandB, this is not true due to the possibility of multiple inheritance.If either
AorBwere final, thenBandAwould be disjoint types, andBwould be a subtype of~A(and vice versa:Awould be a subtype of~B). In this scenario,A & BisNever(for any two disjoint typesTandS,T & SisNever), so in fact it is true thatA & Bis a subtype ofA & ~A-- both areNever.I don't think that's true.
mikeshardmind commentedon Apr 23, 2025
Sorry, that was poorly phrased. The existing subtyping rules don't work the way imagined here for being a subtype of a negated type, and requires strictly adopting the set-theoretic subtyping definitions, something which hasn't been fully done in python.
What we know with ~A, is that if such a type exists, it must not be a subtype of A, but this alone says nothing about the type's other relationships, and as you pointed out, it's possible there there are types that are A & B, and these types aren't in ~A
carljm commentedon Apr 23, 2025
The typing spec has adopted the set-theoretic subtyping definitions as the intended semantics of Python subtyping. Current type checkers may not fully implement them in all cases, but those are type-checker limitations, not a reflection of the underlying theory of Python typing.
Otherwise, agreed.
17 remaining items
mikeshardmind commentedon Sep 26, 2025
I don't personally feel great about leaving some of the problems as "open issues". I don't feel the need to specify every corner case that could possibly occur, but many parts of this aren't really corner cases, but cases that require minor redefinitions of existing behavior for consistency.
I know people want to see this move forward. I'll try to find more of my personal time to wrap up the parts I think shouldn't remain open so that it can be put forward with only the less consequential parts in an unanswered state.
For the record, I'm categorizing it as "too important to leave as open or underspecified" based on any of the following being true.
Of the parts that are remaining to write up, it's mostly scoping negation appropriately. It's required under the third item on my criteria above, but I know there is existing opposition to having negation be user-expressible at this time, so I am trying to limit the impact of it for existing implementations to only what is strictly necessary, while defining it robustly enough that it can be safely expanded in the future without creating new problems.
Several other things that have come up I have put into a "should be expanded on in the future, but not a blocker to progress" category. Some of these are things that should be simple extensions, but that I don't want to predicate intersections on, and can be proposed separately, like an equivalent to TypeScript's
pickfor structural types.mikeshardmind commentedon Dec 4, 2025
I've come to a conclusion that took me longer than I wanted to reach. I was trying to avoid needing generalized negation, despite that it's been my opinion from the beginning that having it was likely necessary.
It's necessary to have generalized user expressible negation be introduced with user expressible intersections, including consistent rules for the negation of gradual types. The work on intersections itself is finished at this point, but it would be a mistake to propose it as such.
I'm going to explicitly reject not including negation in work going forward. There are necessary cases within our motivating examples already, and there are no viable paths for implicit negation strategies that remain consistent with the rest of the type system while also having uniquely decidable inference.
My next steps are working out consistent rules that work properly with negation of gradual types, and performant implementations of all required behavior, as well as preparing to provide implementations to at least 2 typecheckers.
I'm also going to have to take some time to see if some other parts can be made implicit, namely the implied "acceptable types" for various attributes and methods prescribed by python's data model. I believe this would be better to be handled by the typesystem rules and consistent behavior, rather than requiring users to fix types of things like
__slots__manually for every participating type in an intersection. As an example of this, the type system and type checkers should just understand that__slots__must be an iterable (not a sequence) ofstr. An annotation here should not only not be required, but also not be allowed. This is not a hypothetical issue either, real examples of an issue caused by too strict of an annotation being naively included for__slots__in particular, specifically to accomodate typecheckers not knowing the appropriate type of__slots__without it: python/typeshed#14980For anyone concerned about the performance implications of such, I invite you to consider that typecheckers already have to model negation, formalizing it will just make the behavior consistent across typecheckers.
There's also been work done specifically with making negation and intersections more performant over in Elixir, which I expect typechecker authors to be able to draw from given the amount to which the direction of intersections proposed here parallels how they exist in Elixir's type system, and the amount of collaboration that has already occured between some people working on typing in Python and in Elixir.
My own experimentation with implementing this for my theoretical replacement of python's type system used a different structure with similar properties. I may publish this later, but it's still a toy model I've been using to explore ideas to bring into python, and not a standalone tool ready for use by others.
mikeshardmind commentedon Dec 4, 2025
CC @JelleZijlstra On the above, considering your publicly expressed view that negation should not be included in Python's type system. and @carljm because this re-ignites some of our prior discussions on this.
If either of you are concerned about this direction, I can make time to discuss the direction, the rationale, or anything else about the need for negation going forward, either over text, here in the issue, or if we can find a time, in a call of some sort where it may be easier to go back and forth and clear up any possible communication issues as they happen.
JelleZijlstra commentedon Dec 4, 2025
My assessment was that negation types have limited practical use cases and introduce significant complexity over just intersection types, so it makes sense to prioritize adding intersection types first. That doesn't mean I'd oppose a well-written PEP (along with an implementation in a major type checker) that introduces explicit negation types; I'm happy to be proven wrong here.
davidhalter commentedon Dec 6, 2025
Just in case it matters, I tend to agree with Jelle here. I personally don't think the complexity is worth it. I also don't think we need to solve all of the initial motivating examples for intersections to be useful. All of the existing type checkers have some form of intersection already (for isinstance) and formalizing this in the type system would make sense IMO. (FYI: I'm the author of Zuban).
mikeshardmind commentedon Dec 6, 2025
There are too many cases with the most basic use where users won't be able to express the public interface of library code that uses intersections in a way that will reliably work across typecheckers without negation being user-expressible. The issue of typecheckers diverging on library interface interpretation also remains a year-after-year visible complaint in the typing survey, so even if it means more work for me on specifying and providing initial implementations, it's worth not exacerbating that problem.
It's also not really much in the way of added complexity; typecheckers already have to have some form of negation already too to support TypeIs. It's just formalizing the rules for negation and exposing it to users, rather than keeping it nebulously defined as part of TypeIs
CarliJoy commentedon Dec 16, 2025
Just wanted to note that
tyimplemented user facing Intersections already:https://docs.astral.sh/ty/features/type-system/#intersection-types
I remember a
tydeveloper discussing here as well, so I am quite sure they followed the state of the discussion.As they now released a beta, that they recommend for production use of early adopters, I expect that Intersection usage will gain tracking, even with not explicitly defined not (negation).
As much I would love to use not in my types, maybe this could motivate us to put a PEP intersection-only draft out?
At least the people in Astral think it is useful to endusers, so do I.
If you release a current version of the draft I could give you feedback on how understandable the main part is for non native english speakers without a background in the theory of typing.
carljm commentedon Dec 16, 2025
ty dev here -- we've definitely been tracking this effort and would like to contribute to it more directly, but right now we are pretty focused on ty development. I think our implementation tracks well with the latest thinking here. Having an actual type checker with first-class intersection support seems like it will be useful in the standardization process!
Just a note, we do have first-class negation types as well. It's not shown in our docs example, but just as you can import
ty_extensions.Intersection(not at runtime since we don't have a runtime shim module (yet?), you have to protect withif TYPE_CHECKINGfor now), you can also importty_extensions.Notand use it likeNot[SomeType]: https://play.ty.dev/66afb356-11aa-43d6-84b5-bbcfe597635fmikeshardmind commentedon Dec 17, 2025
I have to double-check a few things about it, but I believe based on how it was last I looked, and some of our discussions on this, it's likely already compatible with what I would propose, or would at most, only involve minor changes.
Negation is more likely to have places that may differ, though again, I suspect not significantly so.
mikeshardmind commentedon Dec 17, 2025
After fielding a few questions about the necessity of negation for this proposal elsewhere, there are at least three lines of logic that reach it being necessary to specify.
I find the potential for divergent behavior across typecheckers to be the strongest reason for it to be fully specified, and that user-expression is just a "free" side effect of it being a fully specified behavior: There should be no need to restrict it if so well defined.
Negation is already exposed to users via TypeIs. Differing interpretations of Negation when combined with intersections results in an intersection of callables exported by a library (including those created by decorators) behaving differently on inputs narrowed by users via TypeIs. Negation via TypeIs is already inconsistent across type checkers, and has also been shown to compose poorly with existing limitations of the type system, namely the absence of universal quantification types and the negation of generics.
In practice, some of this already results in diverging type checker behavior, but it would become worse in the presence of user-expressible intersections.
If C is the intersection of two callables A & B
and the domain of A is X, domain of B is Y
then C applied to some variable has a different resulting type based on whether the variable is known to be:
X, Y, X & ~Y, Y & ~X, X & Y, X | Y, or even any of the cases that include a potential runtime error: ~(X | Y), ~X, and ~Y
Because the user can get an intersection from a library, and perform type negation with TypeIs, the composition of these features makes negation required to be defined by the type system rather than by individual typecheckers.
This isn't a place where allowing divergence is positive or can be described as local inference or typechecker-specific heuristics. This will occur at well-defined boundaries across libraries, places where we need typecheckers to behave identically for the idea that users can bring their own choice of typechecker to their own project to remain true.
Adding intersections means every existing source of negation requires agreement within the ecosystem to have stable type behavior when using libraries which may use different type checkers.
There are other lines of logic that require it, but I don't want to get into arguments about whether or not those should be in scope, when the more pressing issue of potential for diverging behavior here applies to this case.
CarliJoy commentedon Feb 25, 2026
@mikeshardmind Can we somehow support you writing the Negation part?
mikeshardmind commentedon Feb 26, 2026
Sorry, getting this to a proposable state has been more challenging than I'd have hoped for, and it's not entirely just the negation portion.
It really should be as simple as putting forth the logical statements and be done with it, but we don't have a foundation that allows that.
Here's the list of things that I need to pose an answer to:
All of these stem from actual existing problems and interactions with our motivating cases. Some of these have answers I'm willing to say should be the only answer, while others I'm worried have two answer that basically come down to "expand existing behavior that has caused problems to include the interaction with intersections" or "fix longstanding issues people have argued against fixing"
drkspace commentedon Feb 27, 2026
There are already places in typeshed/current type checker behavior that's intentionally wrong/imprecise/could be typed tighter (this is just for the typing module):
Io.name's return type should bestr|bytes|Noneinstead of juststr|NoneContainerbeing generic but all subclasses takingobjectas the "other" argumentobjectIt is also littered with
type: ignores because the current types break LSP, which I would argue means the types were defined intentionally incorrect for the sake of the types (mostly thecollections.abcs) working "nicely".I think it being mostly correct now is acceptable and understandable.
(atleast) pyright is already ignoring user-provided types sometimes. For example:
mypy-play link pyright-play link
Edit: Fixed return type of
Io.namemikeshardmind commentedon Mar 2, 2026
Here's the answers I'm currently mulling over for the questions I posed. I'm not sure if these will end up with pushback, and if anyone has a reason I should reconsider, I'm open to suggestions here.
No to intentionally incorrect, "technically okay, but undesirable impact" for imprecise with the exception of APIs where the point of imprecision doesn't cut across gradual/concrete, but across structural/nominal, (ie. returning a protocol because the function doesn't want to commit to certain api details is fine, Unioning Any when the return type is precisely known and expressible is not)
This directly conflicts with something the typing docs call "the Any trick" in an attempt to specifically allow not checking for None in APIs that can return it.
No. Implicit Any is part of gradual typing. It arises naturally in places that the type system doesn't have complete information and such checks if offered by a type checker should not be presented as if they are type errors.
Yet, I think we're too late on actually mandating that distinction.
However this proposal will require improvements to bounds checking on Any for reasonable user experience, and I intend to propose specifics here, including formulating how to do it efficiently, and where the boundary exists on a provable type error vs an opt-in check for users that want to eliminate every implicit source of Any.
The answer here is that without augmenting with information about possible types, the negation incorrectly includes certain things; This seems mostly inconsequential, except for the impact on overload resolution. This isn't ignorable, but I'll try and come up with options that are less invasive than requiring all typechecker bound all types based on what the data model says must exist. While that's a nice goal in it of itself, if we can offer a lighter weight alternative for typecheckers to use, I'd rather offer both to typecheckers (along with examples of why at least one is required)
I think the answer is no, but it should be explicitly called out as something that will have exacerbated impact if intersections enter the equation, and it may be worth reccomending that in places a typechecker is ignoring a user's annotation in favor of it's own inference, that this is available at a non-error level diagnostic (eg. something like a note-level in terms of language server, or an annotation but not a failure by default in CI)
No, but there's some significant complexity if we don't, and some consequences people are going to find strange. It would be better to fix this, but the best opportunity for fixing this was when the unified specification effort began, and now the problems are even more baked in.
Other current in-progress proposals are also running into issues that relate to the same problems, though they manifest slightly differently due to the interactions at play. see PEP 827's open questions and the section on being able to make the top level operations more strictly typed needing context-aware type bound inference (note that changing variance to either be use site based or to require matching variance in subtypes also solves the missing pieces)
mikeshardmind commentedon Mar 17, 2026
Sorry for the slow work on this. I'm getting close to being ready to see if I can find a sponsor. Much of my work on this has been back to paper and pen because I find it easier to work out some parts. The largest remaining portion is to condense the logical outcomes of a specific interpretation of function/method assignability that best models python's runtime behavior while remaining in sound type theory. It's along the same lines as the prior posted draft, but I'm working on wording it more appropriately for a wider audience.
This is a somewhat informal list of remaining steps on my end:
Sub-proposals mentioned as points 1 and 5 here are not load-bearing to intersections, and will be presented in such a way that they can be split off into separate proposals, deferred to a later date, or rejected without blocking intersections
I would greatly appreciate anyone comfortable with the type theory side of things who hasn't checking the prior draft if they have the time to do so for specifically soundness on the function domain portion in case I missed something about it, but I'll have something that may be easier to follow ready in the future.
I hope to have a draft in standard pep formatting ready to look for a sponsor within 6 weeks, but my free time has been less predictable over the last few months.
I'd like to thank to everyone here who has given feedback on the prior draft, especially on the layout of the proposal and on the accessibility of how certain theory was presented.