-
Notifications
You must be signed in to change notification settings - Fork 257
Introduce an Intersection #213
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Comments
Mypy complains about your code because I'm worried that intersection types would be tricky to implement in mypy, though conceptually it should be feasible. I'd prefer supporting structural subtyping / protocols -- they would support your use case, as
|
It would be really cool to implement protocols. Still, in this case intersection could be added as a "syntactic sugar", since there would be a certain asymmetry: Assume you want a type alias for something that implements either protocol, then you write: class _Intersection:
def __getitem__(self, bases):
full_bases = bases+(Protocol,)
class Inter(*full_bases): ...
return Inter
Intersection = _Intersection() then one could write: |
|
I understand what you mean. That could be indeed tricky in general case. Concerning protocols, I think structural subtyping would be quite natural for Python users, but only practice could show whether it will be useful. I think it will be useful. |
This keeps coming up, in particular when people have code that they want to support both sets and sequences -- there is no good common type, and many people believe Iterable is the solution, but it isn't (it doesn't support |
I think I don't think that one needs to choose between protocols and It is easy to add |
For cross-reference from #2702, this would be useful for type variables, e.g. |
|
If we had an intersection class in
|
As a data point, I first looked for |
Just as a random idea I was thinking about T = TypeVar('T')
CBack = Optional[Callable[[T], None]]
def process(data: bytes, on_error: CBack[bytes]) -> None:
... |
I just opened #483 hoping for exactly the same thing. I literally named it the same. I would be all for |
Requests for |
I think we should note the use cases but not act on it immediately -- there
are other tasks that IMO are more important.
|
OK, I will focus now on PEP 560 plus related changes to Btw, looking at the milestone "PEP 484 finalization", there are two important issues that need to be fixed soon: #208 ( |
I agree that now's not the right time to add intersection types, but it may make sense later. |
(been redirected here from the mailing list) I think the Intersection[Any, Not[None]] Would mean anything but |
How about the expression example:
|
@rnarkk these have already been proposed many times, but have not been accepted. |
The What's the use case for that? It's not something I've ever missed in a medium-sized typed codebase at work and in lots of work on typeshed. |
Switch back to protocols such that we can require multiple protocols (as long as there are no [intersection types](python/typing#213) and `TypeVar`s cannot have multiple bounds).
Switch back to protocols such that we can require multiple protocols (as long as there are no [intersection types](python/typing#213) and `TypeVar`s cannot have multiple bounds).
@mark-todd , ordered sounds far too easy to make mistakes with. What benefits does it bring? |
@tylerlaprade pls follow the discussions in this repo. This issue is not suitable for further discussions. Don't post here unless there is general progress in the intersection. In short the ordered nature was thought about while handling the |
For anyone curious, here's an encoding of general intersection types using continuation-passing style. Turns out type checkers already have the capability of checking for intersections: checking if from collections.abc import Callable
from typing import Protocol, reveal_type
# A ≈ (A -> R) -> R
# A & B -> R ≈ (A -> R) | (B -> R)
# A & B ≈ ((A & B) -> R) -> R ≈ (A -> R) | (B -> R) -> R
class Continuation[T](Protocol):
def __call__[R](self, x: Callable[[T], R], /) -> R: ...
def intro[T](value: T) -> Continuation[T]:
return lambda x: x(value)
class Intersection[A, B](Protocol):
def __call__[R](self, x: Callable[[A], R] | Callable[[B], R], /) -> R: ...
def left[A](intersection: Intersection[A, object]) -> A:
return intersection(lambda x: x)
def right[B](intersection: Intersection[object, B]) -> B:
return intersection(lambda x: x)
class A:
foo: int
class B:
bar: str
class C(A, B):
pass
def f(x: Intersection[A, B]) -> None:
reveal_type(left(x).foo) # int
reveal_type(right(x).bar) # str
f(intro(C())) EDIT: def intro[T](value: T) -> tuple[T, T]:
return value, value
class A:
foo: int
class B:
bar: str
class C(A, B):
pass
def f(x: tuple[A, B]) -> None:
reveal_type(x[0].foo) # int
reveal_type(x[1].bar) # str
f(intro(C())) Both approaches are based on the same idea: you represent |
@LeeeeT I don't think either of those encodings are true intersection types. For the first encoding, it's not the case that The subtype relation holds in the other direction, This makes sense operationally: the implementation of a function of type For the second encoding, you want |
Yes, these are not true intersection types, but they trigger the same kinda check in a type checker that you would expect for true intersection types and therefore can be useful to prevent certain bugs in your program.
So, let's talk about the case where you can pattern match on that union (for example, when implementing a union as an ADT). I'm not sure how to show that You're not limited to calling only one of
Yes, |
@LeeeeT this is the wrong forum to discuss this and I don't want to get into a back and forth argument with you. I just didn't want the misleading encoding of intersections to stand. Here's a semantic (i.e., types are sets of values, subtyping is subsetting, and unions types are set unions) proof that Case 1: Case 2: Therefore, every function in the set of functions
That's not a proof, its an informal argument and it shows the opposite of what you think it does. You're claiming that all the functions in The question for if I'm by no means an expert but that reasoning does seem correct to me. |
@CarliJoy did add a post for this, but just pointing out - anyone feel free to open an issue here for discussion if there are points to be resolved: https://github.com/CarliJoy/intersection_examples/issues There hasn't been much movement on intersection for the past year ish but would be cool to get something specified if interest has increased. |
@kmillikin There are many logics and type systems with different sets of laws. I think in Python specifically, given you can't pattern match on the union type, the equivalence between |
@LeeeeT Those aren't equivalent. This has been gone over in great detail elsewhere. I'm not going to go link to each piece of the discussion nor fully re-explain it, as you're responding to someone who already did explain. If you don't understand the given explanation, the simplest mental model, without touching the nuances around gradual typing that have to be preserved is "Given an intersection A & B, things assignable to the intersection must be usable as if they are both A and B, whereas a union between A and B only asks that they are usable as at least one of A or B" I'm preparing a draft that builds on the years of discussion, for intersections to be added to the type system, By far, the longest section in it is handling method assignability, and why various shortcuts are not equivalent. (many shortcuts were attempted along the way to make this easier to implement, none of them work) |
@LeeeeT is saying that even though This is a property of Python's union and arrow types --- you can't distinguish dynamically if you have a value of type The reason we might do such a thing is so that we can encode intersection types as union types by CPS transforming the types and using this "equivalence" to get a union instead of intersection. Of course, we don't have a complete formal semantics of Python typing so we can't actually prove soundness of Python with intersections and this extra rule, so I'd be a little uncomfortable about it. The trick is cute, and maybe it might answer some questions about intersections (because you can ask the question of unions instead, which might have more intuitive answers). I'm skeptical of that too, because I have a feeling that there are interesting questions exactly in the gap between |
class A:
aaa: int
class B:
bbb: int
def f(x: A & B) -> int:
return x.aaa + x.bbb |
@kmillikin We already have answers to this here: CarliJoy/intersection_examples#22 (comment) These answers are also consistent with the ongoing work to add gradual typing to Elixir: https://elixir-lang.org/blog/2023/09/20/strong-arrows-gradual-typing/ Thinking in terms of the Union in CPS form gives us the safe applicative domain of the function, the return type requires further analysis, and is more precise the more information we have at the time. Thus, a given call has more information than all possible calls of the function. We can examine and negate function domains without tranforming to CPS style. That interacts better with the language, especially if overloads exist in the operands, and gives more precise information. My draft proposal will be ready this week barring catastrophe. While I'd normally encourage further discussion to iron out details, it may be more productive to wait to discuss a specific draft proposal. |
Status update on the above: This is almost ready to propose officially. Details, and a place for anyone who wants to comment on specific things about the latest draft can be found here Currently soliciting feedback on which examples make the most sense to highlight to make the case for inclusion the strongest, but if you have other concerns about the proposal, feel free to comment on them as well there. |
This question has already been discussed in #18 long time ago, but now I stumble on this in a practical question: How to annotate something that subclasses two ABC's. Currently, a workaround is to introduce a "mix" class:
but mypy complains about this
But then I have found this code snippet in #18
Which is exactly what I want, and it is also much cleaner than introducing an auxiliary "mix" class. Maybe then introducing
Intersection
is a good idea, @JukkaL is it easy to implement it in mypy?The text was updated successfully, but these errors were encountered: