Skip to content

[RFC] Latest status of draft #53

Open

Description

@mikeshardmind

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.

2025-4-18-draft2.pdf

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

  1. emmatyping commented on Apr 20, 2025

    @emmatyping

    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 if Any uses 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 Annotated could use some context. Right now it's not clear what annotated values have to do with intersections.

  2. mikeshardmind commented on Apr 20, 2025

    @mikeshardmind
    CollaboratorAuthor

    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.

    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.

    Second, I don't see a discussion of the rules with intersections with Any

    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.

    Third, I think the proposal needs to discuss changes to the language implementation, especially giving a name for the intersection type.

    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.

    Finally, I think the section about value types and Annotated could use some context. Right now it's not clear what annotated values have to do with intersections.

    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

  3. CarliJoy commented on Apr 20, 2025

    @CarliJoy
    Owner

    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 :-)

  4. DiscordLiz commented on Apr 20, 2025

    @DiscordLiz
    Collaborator

    I'm looking for comments on which examples

    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.

    any of the language remains unclear.

    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.

  5. superbobry commented on Apr 22, 2025

    @superbobry
    Collaborator

    @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?

  6. mikeshardmind commented on Apr 22, 2025

    @mikeshardmind
    CollaboratorAuthor

    @DiscordLiz The example for total ordering I intend to include is something like this:

    class LT(Protocol):
        def __lt__(self, other: object) -> bool:  ...
    
    class LE(Protocol):
        def __le__(self, other: object) -> bool:  ...
    
    class GT(Protocol):
        def __gt__(self, other: object) -> bool:  ...
    
    class GE(Protocol):
        def __ge__(self, other: object) -> bool:  ...
    
    class EQ(Protocol):
        def __eq__(self, other: object) -> bool:  ...
    
    class NE(Protocol):
        def __ne__(self, other: object) -> bool:  ...
    
    
    type MinimumComparable = EQ & (LT | LE | GT | GE)
    type TotalComparable = EQ & LT & LE & GT & GE & NE
    
    def total_ordering[T: MinimumComparable](typ: type[T]) -> type[T &TotalComparable]:  ...

    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 Any in the motivation section, but I'll be sure this is included in one of the examples for examining types of attributes.

  7. mikeshardmind commented on Apr 22, 2025

    @mikeshardmind
    CollaboratorAuthor

    @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.

  8. mikeshardmind commented on Apr 22, 2025

    @mikeshardmind
    CollaboratorAuthor

    @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.

  9. mark-todd commented on Apr 23, 2025

    @mark-todd
    Collaborator

    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 type section 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 & Any is 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:

    class A:
        foo: str
    
    class B:
        foo: int
        bar: str

    What is ~A? It seems to me this is effectively Any, but with the added restrictions that it cannot inherit from A. B & ~A must have attribute bar, but what about foo - perhaps int & ~str? And if ~A has all other attributes as Any, does that mean (B & ~A).new has type Any too?

  10. carljm commented on Apr 23, 2025

    @carljm

    What is ~A? It seems to me this is effectively Any, but with the added restrictions that it cannot inherit from A

    It is object, but excluding all instances of A and any subclasses of A. There is no Any involved. This is a pretty important distinction: Any is not object, and ~A is a fully static type.

    B & ~A must have attribute bar, but what about foo - perhaps int & ~str

    B & ~A has attribute foo with type int. It would be incorrect to add & ~str to the type of foo. The fact that we cannot have a subtype of A does not prevent an instance of B (independently, without being an instance of A) from having foo of type int & str. (Well, Python's runtime multiple inheritance semantics do prevent that in the specific case of int and str, but this is something type checkers don't currently understand.) In general, negated nominal types tell us nothing about the types of members.

    And if ~A has all other attributes as Any

    No, it has only the attributes of object.

  11. mark-todd commented on Apr 23, 2025

    @mark-todd
    Collaborator

    It is object, but excluding all instances of A and any subclasses of A. There is no Any involved. This is a pretty important distinction: Any is not object, and ~A is a fully static type.

    Ah ok this makes sense - thanks!

    I hadn't thought about using object instead of Any as the set of all other classes, but I think under this formulation the rest of it now works. Although....

    By this logic:

    class A:
        foo: str
    
    class B:
        pass

    B could be considered a subtype of ~A (it doesn't inherit from A, and inherits from object). Does this not imply that A & B is a subtype of A & ~A (or Never), and we end up with a fallacy?

  12. mikeshardmind commented on Apr 23, 2025

    @mikeshardmind
    CollaboratorAuthor

    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.

  13. carljm commented on Apr 23, 2025

    @carljm

    B could be considered a subtype of ~A

    B is not a subtype of ~A. The type B includes all instances of B or any subclass of it. The type ~A includes all objects which are not an instance of A or any subclass of it. It is possible for a class C(A, B) to exist (that is, a class that inherits from both B and A.) Instances of C inhabit the type B, but do not inhabit the type ~A. Therefore, B cannot be a subtype of ~A.

    Another way to put this is that for any types T and S, T is a subtype of ~S only if T and S are disjoint types: no object can possibly inhabit both of them. For two normal Python classes A and B, this is not true due to the possibility of multiple inheritance.

    If either A or B were final, then B and A would be disjoint types, and B would be a subtype of ~A (and vice versa: A would be a subtype of ~B). In this scenario, A & B is Never (for any two disjoint types T and S, T & S is Never), so in fact it is true that A & B is a subtype of A & ~A -- both are Never.

    It's not possible to be a subtype of a negated type

    I don't think that's true.

  14. mikeshardmind commented on Apr 23, 2025

    @mikeshardmind
    CollaboratorAuthor

    It's not possible to be a subtype of a negated type

    I don't think that's true.

    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

  15. carljm commented on Apr 23, 2025

    @carljm

    requires strictly adopting the set-theoretic subtyping definitions, something which hasn't been fully done in python.

    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.

  16. 17 remaining items

  17. mikeshardmind commented on Sep 26, 2025

    @mikeshardmind
    CollaboratorAuthor

    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.

    • Allows for diverging behavior across typecheckers in public interfaces.
    • Breaks the gradual guarantee to leave unresolved.
    • Creates impossible-to-satisfy interfaces due to a missing tool for expression.

    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 pick for structural types.

  18. mikeshardmind commented on Dec 4, 2025

    @mikeshardmind
    CollaboratorAuthor

    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) of str. 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#14980

    For 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.

  19. mikeshardmind commented on Dec 4, 2025

    @mikeshardmind
    CollaboratorAuthor

    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.

  20. JelleZijlstra commented on Dec 4, 2025

    @JelleZijlstra

    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.

  21. davidhalter commented on Dec 6, 2025

    @davidhalter

    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).

  22. mikeshardmind commented on Dec 6, 2025

    @mikeshardmind
    CollaboratorAuthor

    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

  23. CarliJoy commented on Dec 16, 2025

    @CarliJoy
    Owner

    Just wanted to note that ty implemented user facing Intersections already:
    https://docs.astral.sh/ty/features/type-system/#intersection-types

    I remember a ty developer 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.

  24. carljm commented on Dec 16, 2025

    @carljm

    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 with if TYPE_CHECKING for now), you can also import ty_extensions.Not and use it like Not[SomeType]: https://play.ty.dev/66afb356-11aa-43d6-84b5-bbcfe597635f

  25. mikeshardmind commented on Dec 17, 2025

    @mikeshardmind
    CollaboratorAuthor

    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!

    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.

  26. mikeshardmind commented on Dec 17, 2025

    @mikeshardmind
    CollaboratorAuthor

    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.

  27. CarliJoy commented on Feb 25, 2026

    @CarliJoy
    Owner

    @mikeshardmind Can we somehow support you writing the Negation part?

  28. mikeshardmind commented on Feb 26, 2026

    @mikeshardmind
    CollaboratorAuthor

    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:

    1. Is it reasonable to have user-negation with intentionally incorrect or intentionally imprecise information in the typeshed?
    2. Is it reasonable for typecheckers to error just because of implicit Any with negation and intersections?
    3. What's the negation of a protocol, absent the knowledge of the data model not used by typecheckers today as a bound on allowable types?
    4. Do we need to require that typecheckers must not silently ignore user-provided types?
    5. Do we need to fix existing issues with variance?

    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"

  29. drkspace commented on Feb 27, 2026

    @drkspace

    Is it reasonable to have user-negation with intentionally incorrect or intentionally imprecise information in the typeshed

    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 be str|bytes|None instead of just str|None
    • Depending on your POV, Container being generic but all subclasses taking object as the "other" argument
    • TypedDict.items/keys/values having the values typed as object

    It 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 the collections.abcs) working "nicely".

    I think it being mostly correct now is acceptable and understandable.

    Do we need to require that typecheckers must not silently ignore user-provided types?

    (atleast) pyright is already ignoring user-provided types sometimes. For example:

    from typing import Sequence
    vals: Sequence[int] = (1,2,3)
    
    # mypy: Sequence[int]
    # pyright: tuple[Literal[1], Literal[2], Literal[3]]
    reveal_type(vals)

    mypy-play link pyright-play link

    Edit: Fixed return type of Io.name

  30. mikeshardmind commented on Mar 2, 2026

    @mikeshardmind
    CollaboratorAuthor

    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.

    Is it reasonable to have user-negation with intentionally incorrect or intentionally imprecise information in the typeshed?

    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.

    Is it reasonable for typecheckers to error just because of implicit Any with negation and intersections?

    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.

    What's the negation of a protocol, absent the knowledge of the data model not used by typecheckers today as a bound on allowable types?

    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)

    Do we need to require that typecheckers must not silently ignore user-provided types?

    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)

    Do we need to fix existing issues with variance?

    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)

  31. mikeshardmind commented on Mar 17, 2026

    @mikeshardmind
    CollaboratorAuthor

    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:

    1. Introduce sub-proposal based upon https://discuss.python.org/t/hash-eq-and-lsp/68138
    2. Create specification language covering the difference between subtyping and assignability as it relates to safe applicable function domains.
    3. Cover the rationale and the foundational type theory behind point 2 (done on pen and paper, needs to be typed up)
    4. Include a section on how current types in the typeshed are incorrect and could be made correct with intersections + how current issues with the typeshed being incorrect rather than using gradual typing with Any or partial structural typing causes problems, and how intersections can help.
    5. Introduce a policy subproposal based on point 4 to ensure long-term interoperability is based on standards and correctness, not on lint-like behaviors that typecheckers differ on or to accomodate specific typecheckers not implementing specified features.
    6. (maybe): Include an appendix discussing the interactions with future/tangential work, such as that of pep 827 that have already come up in discussion of that pep

    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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions