Rekindling Intersection

[mark-todd]

I'm adding this here as well as on the Discord, in case this has more visibility. I've been trying to make sense of all the discussions that happened in August, and where that might leave the PEP. The number of outstanding issues (as far as I can tell) seems now limited to essentially just the Any discussion, as well as some edge cases with dataclass transforms. In some way this is good news, as it limits the number of things that need to be still discussed.

As a general path to completion:

1. Agree a set of example tests that are coherent and reflect the same implementation.

2. (optional) Ideally we would have a working mypy implementation of Intersection that passes the tests using the new system.

3. Ensure the examples are consistent with the pep.

I would suggest a kind of fresh start for development - anyone who's still interested in development of this, please thumbs up this message and we can organise a call with everyone.

[gvanrossum]

Yeah, Intersection has been called out as a solution to many things people have asked for; I think it's time to start developing a PEP for real. Good luck!

[NeilGirdhar]

the Any discussion

Although heated, the Any discussion ended fairly unanimously as far as I can tell.

I think the most important thing that we're missing are motivating examples. Intersections may end up being a lot of work for type checkers to implement and we need to convince them that that work is worth doing for the PEP to be accepted in the first place. It may be worth reading Eric's comments in the various issues in this project to get a feel for the kind of resistance. Although he did recently say on some issue "if and when intersections are added", which suggests that he might be warming up to the idea 😄.

If you're looking for motivating examples, you might search through the issue trackers of various type checkers, the python discussion forum, the typeshed and the python-typing issue tracker. It might help to search for "intersection", or make educated guesses about where intersections would have been useful and search for that.

Since no one else has responded to your pull request, I volunteer to look it over when it's done. Just ping me 😄

[gvanrossum]

At the same time, as a member of the Typing Council who will ultimately have to review the PEP, may I ask for brevity in the actual specification? The way I like to learn stuff is through examples, so examples showing the common syntax and semantics (and some edge cases) would also be super helpful. I'm personally already convinced that there are enough motivating use cases, so I'll probably skip that section, but it's good to have for other readers -- the Typing Council is unlikely to accept a proposal if there is widespread resistance.

[mark-todd]

@NeilGirdhar Thanks that'd be great! The Any discussion as far as I know has now concluded, we'll be summarising it's findings tomorrow and hopefully adding this to the specification.

@gvanrossum re brevity sounds good to me! The plan is to try and keep the PEP as minimal as possible, while also keeping in the features that will be useful. I think having lots of examples is definitely a good idea, I also prefer to learn new syntax this way. We'll include justification for why different choices have been made in the PEP, but perhaps we'll put this in a specific section or appendix to separate it from the specification of Intersection itself. We're meeting to discuss the PEP tomorrow, and hopefully resolve any remaining discrepancies on definitions.

[mikeshardmind]

@gvanrossum we need to circle back briefly to discuss how we want the boundary between gradual typing and static typing to work in the case of SomeConcreteType & Any

We have 3 options based on where and how we draw that fence, one of them was ruled out

• disallowing Any as nonsensical in an intersection(ruled out, could happen due to untyped libraries, and would arise deep in the type checker internals)
• Any & T irreducible (prior front runner), and essentially makes every attribute infinitely compatible, similar to as if it became Any
• Any & T is T for things T provides, but any allows other attributes (safer hard fence between the two, came up in discussion in discord today, explanation on issue here)

I'm in the process of updating a lot of the language we have for where we have consensus (on everything else) and other changes type checkers have made regarding LSP and enforcing it in subclasses has rendered the other controversies moot or deferrable.

Namely:

• we no longer need to care if an intersection is impossible to satisfy at the point of an intersection, lazily checking compatibility with each intersection operand at assignment is sufficient.

• These same LSP guarantees also change type negation from necessary to have, to a nice addition that can be considered separately in a future pep

[gvanrossum]

Why can’t Any&T be just T? And what does irreducible mean?

[randolf-scholz]

@gvanrossum Irreducible means precisely that it cannot be simplified to T. A type substituted for Any could provide methods that are not present on T, and therefore it cannot be removed from the intersection.

For example, I might import class Book from library. Without library-stubs, Book is considered Any. But Book & Hashable should not simplify to Hashable.

[mikeshardmind]

Any & T = T Would be treating Any as having a different definition than it does. While I'm in favor of such a definition, it's not the one we have and might be better suited for a hypothetical typing.Unknown that defers to all other static information available and is not the top type, bottom type, and an infinitely compatible placeholder all in one.

In the other direction, we have irreducibility and Any & T = Any

The problem with it being irreducible is that gradual typing then flows in the opposite direction as intended (gradually typing more things) by acting to infinitely broaden most interfaces essentially being Any

class X:
    def foo(self) -> int

z: X & Any = SomeUntypedFunction()
z.foo(1)  # This is allowed if irreducible, there's a hypothetical possible
# class that implements a compatible foo with a default value for this parameter.
# This hypothetical class that Any could be would prevent checking the intended use.

[CarliJoy]

Why can’t Any&T be just T

Next to the case of introducing problems using 3rd Party libraries that aren't typed yet as explained by @randolf-scholz above and by @ippeiukai here, it also breaks symmetry between Union and Intersections as described by @erictraut here.

[NeilGirdhar]

Why can’t Any&T be just T? And what does irreducible mean?

If you look at this issue, you can see the explanation for irreducibility and the arguments for and against it. Since you like examples, I'll just illustrate with examples.

Yes, you are right that Any & T is T in some cases. For example,

class A: pass
class B: pass
def f(x: A&Any): ...
f(A())  # Okay, of course.  A is both a subtype of A and Any.
f(B())  # Error, of course.  

But, given an element of A & B, you can do anything with that you can do with a A or with an B:

class A:
    def a(self): pass
class B:
    def b(self): pass

def f(x: A):
    assert isinstance(x, B)
    reveal_type(x)  # subclass of A and B; i.e., A & B
    x.a()  # Okay!
    x.b()  # Okay!

And thus when B is Any, you can do anything with such an object.

There are some much nicer explanations in the linked thread by Eric and Jelle.

[gvanrossum]

Okay, no more explanations needed. I was simply mistaken. I presume standard type would turn it into just Any?