[RFC] Latest status of draft

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

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

[mikeshardmind]

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

[CarliJoy]

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]

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.

[superbobry]

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

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

[mikeshardmind]

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

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

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?

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

[mark-todd]

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?

[mikeshardmind]

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]

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.

[mikeshardmind]

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