Interpretation of type Any & T
#31
Comments
|
Assume this simple but verbose example. Module a_untypedclass A:
common: str
a: int
a_str: str
def fn_a(self, a: int) -> int:
return a
def fn_mix(self, mix: int) -> int:
ab_mix: "A"Module b_typedclass B:
common: str
b: str
def fn_b(self, b: str) -> str:
return b
def fn_mix(self, mix: str) -> str:
return mix
ab_mix: "B"
|
|
Hmm looking at the example it seems that we have to decided between allowing As for the most This is in contract to the example given by @ippeiukai here. Copied and modified below for easier reference: By the way, in terms of gradual typing, I feel Intersection[T, Any] = T is awful. Module 1some_fn(some_obj)Module 2def wrap_obj(val: T) -> T & SomeAddedTrait:
…
a = wrap_obj(some_obj)
some_fn(a)Here, let’s assume TODO: formulate example more concrete, I don't get it atm,@ippeiukai could you formulate it with proper files and imports like I did above |
I'll type up some examples when I have more time, hopefully later today, but both of the following are true here:
I think @DiscordLiz had a good point in the prior thread about Any & T never being an intentional construct. When is this going to come up? Do people intending on having Any have a use case for intersections, or is this sufficiently advanced that people should be expected to have typed their bases better and we should err on the side of safety for users on this? I think we need to start from where we expect this to occur before we can evaluate the impact of any choice. It's clear it can only happen at the boundary between typed and either untyped or gradually typed things, but can we get more specific than that and determine if there's ever an intentional use for T & Any which isn't better served by other existing things? |
|
@CarliJoy Thanks for this example! It's very thorough - I've reduced it down a bit to consider a particular subcase, not because the others aren't relevant, but just because I think it might be easier to discuss in pieces: import typing
from intersection_examples import Intersection
class A:
common: str
# A effectively gets cast to Any, so nobody knows the type common even exists
class B:
common: int
def needs_int(x: int) -> None:
"""Example function that needs to be called with integer to work"""
def needs_str(x: str) -> None:
"""Example function that needs to be called with string to work"""
def use_ab_intersected(x: Intersection[A, B]) -> None:
# Note: A&B is an LSP violation, but we don't know that it is, because
# we don't know the type of A
needs_int(x.common) # should be fine - this is a property of B
needs_str(x.common) # This should also be fine - if A is used at runtime
# It could be string? Or could it?
# Follow up idea - do we have to assume the intersection created with Any
# has not created any LSP violations?My conclusion from this is that similarly to other types we intersect, perhaps we have to assume LSP has not been violated by the intersection with the Any type - although we have no way to be sure |
|
I am still groping my way around this subject. I am unsure of the technical meaning of "gradual typing" that seems to be used by some participants. In the meantime, I have an example, which has actually convinced me that this proposal is fine: def f(a: Any & int):
x = a + 1
reveal_type(x)Given that |
Which makes it intersections all the way down and no different than being Any, cause we have to assume LSP wasn't violated. If that were intentional, someone could skip the intersection and just write Any, and that works today.
I don't think it's intentional, but I do think it can happen. The middle ground (that was option 5? and we're only considering options 4 and 5 now? Sorry, I seem to have missed the reason for splitting this to a new thread.) seems to avoid the accidental issues possible in 4, but I'd like more examples of it from @mikeshardmind
That would be the behavior in option 5. Option 4, the return type can only be int & Any, it's recursive with that option, and more pervasive than I think is beneficial. |
Just something for you to consider. Let's just look at an example that doesn't involve class C:
def f(self) -> None: pass
class D:
def g(self) -> None: pass
class E(C, D): pass
def f(x: C):
if isinstance(x, D):
reveal_type(x) # C & D
x.f() # should be okay since x inherits from C
x.g() # should be okay since x inherits from D
f(E())This is why the interface of Now, consider:
It's really worth reading Eric's elucidating comment. For reference, there are two proposals being considered here. I'll call them 4 and 5 (relating to names from #1). |
|
Even though I'm not yet in favor of proposal 5, I have a way to illustrate the problem it may be trying to solve: Consider what x: Any
assert isinstance(x, U)
y: T
assert isinstance(y, U)The general case illustrated by Essentially, there are two I think the people in camp 5 are worried that this pernicious behavior that we avoid using the type replacement will creep in when we enable intersections generally. I considered a 6th proposal: encourage to choose replacement if they want to protect against the spread of def f[T](x: T):
assert isinstance(x, U)
# Normally, this would have type T & U, but you can force replacement by casting.
x_as_u = cast(x, U)
# The over-broad interface of T & U is avoided.This would allow us to leave the ordinary meaning of I think we need to see some concrete examples to test if this could work. |
|
If I need a cast everywhere I use an intersection to avoid issues with Any, then I don't need an intersection, I can cast to a protocol that matches my use. You're just replacing one wart with another worse one that disables other checks here, and requires runtime checkable protocols and a runtime cast use.
That's exactly the issue with option 4. It cripples type checking for the person with fully typed info on their side of the intersection and is no better for the person with Any on their yet untyped object than not using an intersection and using Any. |
So we're on the same page, and I think I understand your point of view. I see how the deference proposal prevents false negatives, but it does so at the cost of false positives. Historically, the Python typing community has preferred solutions that avoid false positives even if they cause false negatives. For example, the adoption of the sequence protocol into the typeshed causes false negatives in order to avoid false positives. I think we just need to see at least a few common examples to get a better handle of what the tradeoffs are.
I don't think it would be "everywhere you use an intersection", but as I stated in the previous comment, it would only be in the cases of intersections with unbound type variables, and similar. Like I said, this was just something I thought of. We need to see some examples to know what it would look like. |
@gvanrossum I think your example makes sense, but the controversial part comes from the other side of the intersection - as you describe the result must have all the properties of My conclusion from this is that perhaps it has to be some subset of every available option, e.g. Any type that fulfils this LSP condition. Or perhaps no methods that "clash" with those from the other half of the intersection.
Perhaps we should restrict our examples to those that fulfil this condition? Even in the case we're untyped, it seems we have to assume that this method clash hasn't occurred. @NeilGirdhar @mikeshardmind Specifics aside, I think whatever solution we come up with, it shouldn't require cast or
I guess this is maybe another way of phrasing @NeilGirdhar 's previous point about false positives vs false negatives. |
|
The False positives case is preferable because we still give the user a way to handle it without a type ignore and without additional runtime costs. The False negative case cannot be remedied except by removing Any, and the whole reason we can't ban Any from intersections is that type checkers have stated this could happen in a way users don't have a way to remedy or even a clear way to inform them. Consider this: from untyped_library import SomeParserAugmentor # user may not realize this is untyped at first
from typed_library import SomeParser # generic over T, provides .parse(self, arg: str) -> T
def my_func(input_: str, parser: SomeParser[int] & SomeParserAugmenter ) -> None:
""" Typed permissively so that other people can use the function """
# This errors, we restrict the interface of Any when it clashes with what is typed
# This also means the person writing the intersection is the one who gets the error
x = parser.parse(input_, fix_mojibake=True)
class _Parser(SomeParser, SomeParserAugmentor):
""" Internal fallback where we create only the baseline functionality """
pass
...
# this is fine, subclassing from Any means the attributes needed are assumed there.
# This is the case currently with subclassing Any, not even just with this proposal
my_func(some_user_content, _Parser(int)) In this case, the user actually has the tools to fix this without a type ignore in multiple ways.
from untyped_library import SomeParserAugmentor # user may not realize this is untyped at first
from typed_library import SomeParser # generic over T, provides .parse(self, arg: str) -> T
from typing import Protocol
class FixesMojiBake[T](Protocol[T]):
def parse(self, input_: str, fix_mojibake: bool=False) -> T:
...
def my_func(input_: str, parser: SomeParser[int] & SomeParserAugmenter & FixesMojiBake) -> None:
x = parser.parse(input_, fix_mojibake=True) # This no longer errors
class _Parser(SomeParser, SomeParserAugmentor):
""" Internal fallback where we create only the baseline functionality """
pass
# this is still fine
my_func(some_user_content, _Parser(int)) With this, they've now explicitly stated they expect this compatible method to exist. This gives users the information they need to type things without compromising on safety for the portions of code that are already typed, and while being easy to accommodate situations outside of their control with untyped libraries. Note that this is safer thana type ignore, it would rely on the nature of Any for the thing Assigned to it, but it requires explicitly escaping out for things that could otherwise be accidentally hidden in terms of misuse by restricting the interface on usage to what is explicitly stated. This also automatically continues working should the untyped library become typed in the future without something lurking around for compatibility that could be silencing errors. I think if we pair this approach with a note that type checkers should inform users when Any is present in an intersection that is causing an error and point them to a reference of how to handle this, we can make this easy to learn and ergonomic as well. |
|
A few observations after having read Eric's comment and trying to reason various things out in my head.
I'l write more later. |
|
[me]
Great, it should be possible to reason this out by considering types as sets of objects.
But why introduce a new term, "interface"? Python's type system never uses this word -- we talk about types. I feel it's misleading to introduce this term -- probably because of my point (2). We should only consider questions of the form "if x has type T1 and y has type T2, is
I feel this is not helping clear reasoning, given that in
Should be rephrase in terms of what happens to
That's a valid question. I think it should be answered by considering separately what the type of an expression is when Interestingly, since the answer might well be "an error occurs" for one of the branches of the But now we get to think about when an error should be reported to the user -- surely not as soon as it occurs, in the case of Also, it seems that whatever rules we come up with for
I don't know what the type of |
Exactly what I was getting at :)
This is a great idea that actually works with both proposals. We could leave the "correct" semantics of proposal 4 coupled, and encourage type checkers to implement an optional warning when someone accesses an attribute on something with type
I agree that we should explore other ways in which
Right, I see where you're coming from. If that's the language you like, then I think you'd find Jelle's comment the most clarifying. I was using language closer to Eric's comment. As per Jelle's comment, two things constitute the "type" (as returned by
These correspond to what Eric called subtyping and attribute type evaluation. And the latter is what you're calling
Yes, you're right of course. I made a mistake in my evaluation.
I think I just made an error when evaluating the values 😄 Regarding the ideas surrounding |
Please review the important distinction with false negatives. There is no way for a user to know they need to resolve a false negative arising from types outside of their control because the user will not get information. This would be particularly insidious if the user thought they had something typed that wasn't. Additionally, the entire reason we are having to consider this is that we cannot ban Any from intersections entirely, they can arise deeper in the type checker, per Eric's comment taking that off the table. This means in those cases, there's nowhere to give the user the error for Any existing in the intersection, and there would only be a resulting false negative. This cannot be used to resolve this in the case of proposal 4 if we continue to accept previously accepted arguments. |
We need to be particularly careful that anything we say is a dual and should have symmetry actually is or we may create worse situations by mis-considering something. It would be one thing to intentionally decide something isn't useful as symmetrical, it would be another to inadvertently state things that arent symetrical must be treated as if they are. This issue here elaborates on Eric's comment and shows that only some of what was said was true by nature of universal properties. Importantly: from it:
|
|
Duly noted that duality is tricky. I have my thoughts about false positives vs. false negatives but they are colored by my experience spinning up mypy as it was being written in a production code base with millions of lines of existing (untyped) code. False positives would cost the tiny mypy team days of explaining to random senior engineers why they had to make changes to working code to satisfy the upstart type checker, while false negatives were what everybody got all the time (since most code was still untyped). I am despairing at ever coming to terms with this topic. I wrote the original text in PEP 483 and I admit it was vague to the point of being unhelpful. (Since it is not a standards track PEP, I'd be happy to entertain PRs that fix specific issues with it, though not with proposed full rewrites.) I am still hopeful that we can define intersections in a way that's the dual of unions (using the correct definition of dual). |
Why can't the type checker produce a warning when a user accesses an attribute of something that has type
In the cases that the attribute access happens deep in some library, the user hasn't been "robbed of a potential error". If there is an error, it's the library author that needs to see it. |
That was Eric's statement that took banning Any in intersections off the table, and was taken at face value given the work he has put into pyright. I don't know why it can't, I see no reason why it shouldn't be possible to bubble it up to where it was sourced from, but I'm not actively maintaining a type checker right now either. Considering this was used to take an option off the table and nobody contested that, we can't simultaneously accept it to take one option off the table and reject it to say something else isn't an issue. If you'd like to contest that, I'd happily bring back the argument to ban Any in an intersection because I can't see a single case where intentionally using it in one is beneficial. It would be better to omit the intersection entirely and just type Any instead of Something & Any with some of the proposed behaviors. (If the presence of Any in the intersection effectively allows everything as compatible, and silences all errors, it's no different than Any even if we have theory that says we shouldn't remove it, the practical use is no different.)
This isn't necessarily true though. It's not an error in the library, it's a lack of information that would be silently hiding any issues in an intersection resulting between my code (typed) and library code (untyped). This would become yet another social pressure to add typing, to libraries that may have various reasons not to, such as still using things the type system does not yet have a way to express. From a pragmatic standpoint, if someone says "I need to be able to use something as this type and this other type", if one of those types isn't typed, do we really want to discard information on the type that is typed? |
I can appreciate that perspective. Largely, I would agree on minimizing false positives. When I was coming up with the middle ground, the considerations I took with it were the following:
|
I don't want to contest that because I agree with Eric that I'm saying that in your own code when the you access an attribute of something having type If you feel strongly about this, maybe you should reopen #1 and try to swing the consensus to the proposals you were supporting (1 and 2). This thread was supposed to be about 4 versus 5.
Can you give an example of library code that accesses an attribute of something having type
Yes,
I don't see how that helps since if something is annotated |
No. Categorically, no, because at that point I'd rather make it an error to include Any in the intersection than an optional warning. Many of the cases we have motivating this are decorators with intersections as the return type. The behavior of (Op(Any & T) being equivalent to Op(Any) means the intersection there is pointless for those specifying their needs, and may lead to surprising outcomes for users. My view on this is not only from the point of safety and correctness, but also on making the type system less surprising to users. If Any & T is no more specific about what is allowed than Any, then specifying Any & T shows that the user clearly thinks something more is happening or they wouldn't bother with a more complex type that is the same thing. This also relates to:
You say it's an obvious analog, but I challenge you to find a case where you would intentionally include Any in an intersection as a parameter and it be more useful than simply stating Any. If there is no case where it is, the behavior is not useful, and the statement of that intersection would indicate that a user has the expectation that something else would happen here.
Since we clearly aren't all on the same page about the reasons why other proposals were not an option, I think that is necessary. I only agreed that we could stop that discussion because I thought people were going to be consistent in applying the reasoning for other options being taken off the table.
I'm not rehashing examples that were already given and interacted with. That you have ignored prior examples I have given on this matter does not make me inclined to take the time on this, those interested can read the prior discussion.
Removal of untyped code does not need to be by removal of the code. I thought you had been aware of the other related discussions on this, and the part of that statement you left out was the social effect. Socially pressuring other libraries to add types is not a positive effect and is more divisive than a lot of people deep in typed python realize. I value a pragmatic boundary between what is typed and what is not that makes it clear when typed code is interacting with untyped code without needing to compromise on the portions that are typed, as it reduces that pressure to a minimum. |
Since neither of you have said it, We can also forbid unbound type vars in intersections or say that the behavior of an unbound typevar in an in intersection is to default to a bound of object rather than of Any, which remains as permissive to what can be passed in, but doesn't create that issue. This isn't a strong argument against forbidding Any in an intersection, but It also doesn't fix everything. The problem here isn't just typevars. def real_class_decorator_example[T: object](user_type: type[T]) -> type[T & MyProtocol]:
...If a user calls a function like this today, inside the body of foo, it is only safe to access what is on type[object]. However, what they get back is safe to use based on whatever the input to this function was. It is clear that this decorator adds support for a protocol, but if T going in is Any, then that protocol is never going to be checked properly under option 4. I'm concerned that if we just allow Any here to remain in and have the behavior from option 4, that a lot of situations involving intersections become useless in the presence of any untyped code at all, because it's just too risky that somewhere deep in the type checker, something became as useless as Any unexpectedly. what @mikeshardmind came up with for option 5 avoids this. If we're reopening up the other options, I think T & Any being treated as T for safe access also avoids this, even if we know it isn't theoretically fully accurate. Both of those options retain what he expressed about a pragmatic boundary between typed and untyped as well, and I agree with him that that it's necessary to have that boundary. He spoke from social pressure, but there are other issues as well. Not everything in python can be expressed by the type system. That's okay with me. But I'd like to be able to use those things when needed and still keep what assurances can be provided by typing in the process. |
|
For what it's worth, keeping in mind that the difference between intersections and unions is more about the subtyping relationship, and that Any behaves differently on opposite sides of <: T | U Allows anything that is a subtype of T or a subtype of U to be assigned to it. In the case of U being Any, this allows anything. I think we all agree on that part right? T & U allows only that which is a subtype of both T and of U to be assigned to it. If U is Any, the requirement of it being a subtype of T has not gone away. A concrete object known as Any, but then known as a subtype of T is no longer Any It's a subtype of T. The fact that in python we do not distinguish between an unknown that should be treated as anything until it is known and literally allowing anything is making this dual harder for people to reason about. From all of that, a consistent behavior here is that Any & T no longer has the compatibility behavior of Any as it's no longer Any. |
|
And if you extend that to "It also needs to be a subtype of Any though", well what does that look like? class Intersected(T, Any): I know he called it a compormise, but it's sure looking less like a compromise and more just like the correct consistent behavior with other typing decisions to me |
|
sigh it's consistent with other typing decisions, and consistent with the subtyping relations involved, but I don't know that the prior decision involved was well considered. I happen to like that outcome, but the ability to subclass Any at runtime to indicate that behavior was accepted with a brief bit on the mailing list that received minimal attention and was done without a pep discussing the impact on how we treat Any in the type system, and I won't hinge it on "We have this behavior, so this must be the right interpretation". It being a consistent interpretation that continues following the subtyping rules is nice, but that was by design. I won't go as far as to say it's the only possible interpretation given the only minimal prior consideration. I think it has precluded something important that could have been done that you actually got at, splitting "Unknown, could be anything, but use what you know about it and permissively allow use until you know something more specific about it" and the theoretical "Any" |
|
I did some more thinking about this, I think option 4 actually is a non-starter unless we also make changing the behavior of runtime subclassing of Any part of the PEP. I'm not in favor of this as I think option 5 is better for users, but I do think it needs to be said so that if option 4 is decided on, that isn't lost. Not doing so would make Any special in that it is the only case where an instance of a valid subclass: class UnimportantName(T, U):
passDid not have the same safe operation on it as valid emphasized, because some intersections would require additional reconciliation in the body. The first form is valid today with Any as a base, and matches the behavior of option 5 |
Maybe it's clear to you, but it's not clear to me what safe operation you are referring to here? |
I would say there have been examples that have shown negative value for option 4 too (e.g. the table example @randolf-scholz put forward earlier in the discussion), it's just that for me in option 5 the pros outweigh the cons.
I should have made this clearer, I guess ultimately I was thinking that options 5 and 6, are most similar so we could figure out which is best as part of developing the "option 5" PEP, I didn't mean to suggest I'd excluded it. I think option 4 presents a case that is much more different, and reconciliation between this and the other two is harder.
It seems to me that there are some cases that work better for option 4 and some that work better for option 5/6. I'm not sure how this could be resolved by somebody hypothetical in the future, unless there exists an option we haven't yet thought of. |
|
@mikeshardmind I think Option 6 would look the same as Option 5 in this table (hence what I meant about similarity) - if this isn't the case though I'd be interested to see what it's column would look like. |
I don't think the arguments for option 4 over option 5 preclude option 6.
The table may differ* between 5 and 6. Specifically, if 2 operands have conflicting definitions for * Edit: actually, it doesn't differ, the table doesn't present the case where the difference exists! but described anyhow |
I don't think there are any cases which work better for 4 which are actually good canidates for intersection. None of the motivating cases we collected benefit from it, but toy examples did. Those toy examples also benefited from the mused about The toy examples which benefited from 4 over 5 assumed complex diamond patterns were common, the actual class which resolves them wouldn't be provided, and that one side of the intersection would be untyped. I view this as a stretch, but I think that case can still be supported separately with the |
Yeah I suppose what I meant was it seems to be "new and improved" option 5, which is great, but then if anything that makes it the successor to option 5. Option 6 takes care of a different (but still very useful!) case. Then the discussion becomes option 6 vs option 4, and we're back to the same old debate. To truly resolve we'd need something to behave like this:
...but I think this is impossible. So that means a trade off has to be made, but which trade off is the better of the two seems quite subjective, it might be based on which use case feels like the most common or most useful. |
This is interesting. I know we floated the idea at some point of If all the motivating cases can be covered by option 6 and this term perhaps this is worth pursuing as the two PEPs. |
|
I think I'd prefer
Kindof why I think it's too early to go to "lets just put a couple peps forward". I don't think we've explored enough options. It didn't take me long to look at where I thought the current options were lacking and the objections raised so far to iterate on option 5 to arrive at option 6. We seem to, myself included, have come into this discussion with preconceived notions of what should happen, but really as long as our rules make sense, serve the purpose we set out to accomplish, and are consistent, we have no obligation to stick with the preconceived notions we have around this. I think it's largely our job here to explore the potentials where there are downsides to see what we can do, if there are things we can't solve with a single construct, and if the path we pick still allows those things to be solved by something else or if it cuts those off. I'd want to see if other people can iterate on what they feel is missing (if anything) as well. Maybe we reach something that can be presented as a single pep with a unified voice, as well as have a path to supporting the things we can't with just this. |
Yeah we should perhaps move this to a different thread, but at least we're in agreement about what behaviour this would have.
I think migrating to a more example based look at things is perhaps a good way to go. I'm not sure we can discount examples for being too "toy" - often reduced examples like this are just difficult to express in practical cases, but that doesn't mean the practical cases won't occur. I've been working some more on the intersect simulator, my hope is if we can get it to a point that we can run all the examples for each option we can see the pros and cons of each.
Yeah this is true - I suppose it was my impression that the notions of expected behaviour had reached an impasse, that would be impossible to reconcile because each person prefers a different use case, or perhaps because one solution is more practically satisfying while the other is more theoretically satisfying. |
|
I don't know if the two PEPs idea is still in the running, and I am just speaking for myself here, but I would advise against this. Making the SC debate this and expecting them to come up with the right answer is unreasonable, given that the group here hasn't been able to get to an agreement -- you might as well flip a coin. Worse, the SC might reject both PEPs. Substitute Typing Council for Steering Council (the SC would likely ask the TC for its opinion anyways) and the same possibilities exist. I strongly advise everyone here to consider what they would rather have -- no intersection or the option that they dislike. And take it from there. |
@gvanrossum For me the option I dislike is definitely my preference over no intersection, but I'm not sure everyone feels the same way. Maybe you're right that the two or three PEPs idea just leads to the Typing Council or Steering Council endlessly debating, I suppose my hope was that in forming the PEP both ideas would gain clarity. I've been thinking a bit about an alternate approach. As @mikeshardmind has pointed out, it's possible that neither options 4 or 5 present that best interpretation of Stage 1: Identify intersection variationsPerhaps it's worth taking a step back, and instead of thinking about how we can narrow down our available options, go for the opposite. We try and identify as many ways that Any & T could be interpreted as possible. In this stage it doesn't matter if there are pro cases or counter cases to these variations, the point is simply to say "this is another way to interpret the intersection". Stage 2: Produce pro and counter cases for our favourite combinations of intersection properties.At this point we try and develop distinct for and against examples in the simulator for each set of properties. These examples can be toy or real - the point of this stage is simply to show that this combination of properties, in this example produces either a useful or not useful result. We can agree on what the result would be because the simulator should produce this result. If the simulator doesn't produce the expected result for the combination of properties, that's a bug in the simulator. Stage 3: Elimination roundMy hope is that by this point there may emerge an option that has few or no counter cases, but if not, I guess we could go tournament style. The point of this stage is to end up with only one option remaining that everyone is satisfied with.
Going back to what @mikeshardmind said, I agree with this, but I think it would be useful to try and structure our process a bit more (hence the above). I'm trying to avoid falling into circular debate, and concentrate more on developing clear options with clear examples. |
You may be absolutely right, however at least two people from the typing council have been commenting on all of these issues. If we were to write a PEP, I'm pretty sure we would copy and paste their own arguments. Also, from what I've seen, both the steering council and the typing council have made excellent and well-reasoned decisions. I have a tremendous amount of respect and faith in their decision-making process.
While I would love to find consensus, it just seems unlikely at this point. First of all, in the last few comments Mike is saying that " If [proposal 4] were accepted, I'd probably give up on trying to improve typing in python". I think it's fair to say he's not willing to compromise. Compromises I'd like to consider include:
Second, if you go back to the very start of #1, there remain fundamental misapprehensions that motivate options 1, 3, 5, and 6. Namely,
The first idea seems correct at first, but the issue is that a "type" as far as a type checker is concerned has to encode both the valid subtypes and the valid interface ( The "any-substitution principle" is that a type expression involving a specified type While I recognize that there is room for making things practical rather than pure, I think breaking these kind of basic rules is going to lead to more problems as typing evolves. For example, if higher-kinded types are added, there may be many more synthetic types. And with synthetic types, we may see synthetic intersections deep in synthesized core where there may not be an opportunity to even stifle type errors (or they may produce very convoluted errors). Finally, there have been some absolutely disrespectful comments, and I don't think that it makes sense to work with people that insist on that kind of behavior. So, my preference is to simply write a PEP, and if the others want to write one or two more PEPs, I think they should do so and I'm happy to wait a few months so that we can submit them together. If anything, maybe this exercise will produce the clarity that's been missing. |
I think I see what you're getting at with these two points, but I'm not entirely convinced the first one is applicable to Any (I'll invert them for discussion)
I see how if T is Any, this becomes Any & U is wider than Any, which doesn't make sense. It's been discussed that Any is the top and bottom type, which I think would mean Any & U is both wider and narrower than Any. I'm not sure I'm convinced this tells us much in the Any case.
This one I buy much more. If you replace a more specified type with Any, it shouldn't create errors - that would be very strange indeed! But I'm not convinced that option 5 is in violation of this. If T & U -> Any & U, all the properties of T just become Any, while the properties of U remain - I don't see any issues here. |
Sorry, I was just speaking loosely to give a feeling for the general principle. For the exact rules, please see Eric's comment (you'll have to search for it). If I remember correctly,
The problem is that if
then, the substitution causes type errors. If I end up writing up a PEP, I'll add this principle as a general principle so that future typing proposals can make use of it. |
I think I found it again: #1 (comment)
Point taken on the substitution part as well. If we want to adhere to these principles option 5 would not work. Let's assume for a moment that we go with |
|
To delve into the more practical, I'll put this thought into an example: class T:
x : int
inst: T & Any = T()
z = inst.x # So this is now type int & Any
z += 1 # Definately valid
z = z + 'test' # Now here we get the controversial bit. My hunch is that (by some means) the final line should be invalid, but here's the problem. If we say it's valid, how is this any different from z just being |
|
Yes, that's the comment I had in mind.
Yes, I think so.
class T:
x : int
class C(int):
def __add__(self, other: Any) -> C: ...
class U(T):
x: C
inst: T & Any = U()
z = inst.x # So this is now type int & Any
z += 1 # Definately valid
z = z + 'test' # No error.
If I understand correctly, you can't do anything with
I think it follows the rules that Eric gave recursively. |
If it must return an
I've had a follow up thought - EDIT: Tested and |
Eric's rules here are very compelling. For cases outside of I'm also drawn back to my previous post: #31 (comment) In the case where T has another type for foo, this becomes a problem. But it has been noted this would create an LSP violation. If we assume that A and B must have the same type for property (A & B).x: Are all the cases where option 5 fails the any-substitution principle LSP violations? |
|
Ok slightly radical idea: Intersections between two classes where the types are different on two of their attributes & methods are banned on access (as in option 6, but expanded to methods). I appreciate this might go further than LSP but it has some advantages:
The only real disadvantage I see is we lose the utility of combining methods of the same name into being overloads, but in comparison to all of the advantages this feels like a small loss. Thoughts? PS: I may have mentioned this before, but if so I wasn't aware of all it's advantages. EDIT: I also vaguely remember when we discussed something similar before, it was concluded that would take too much runtime cost to evaluate both classes and determine if they're compatible. Now it's on access however, that means we just have to compare the relevant attribute. |
That's an interesting idea. That restriction makes many of the problems fall away. Question to others on the thread: Does that restriction eliminate any important use cases that you've identified for intersections? It would preclude my @DiscordLiz said "I would not want to use an intersection with non-disjoint types. It generally doesn't make sense to.". This proposal effectively takes advantage of this observation and codifies it into the rules.
I see this as more of an advantage than a disadvantage. Combining methods of the same name into overloads is problematic because overloads are ordered and intersections are not. Overloads also have a bunch of other complicated rules associated with them that don't apply to intersections. This proposal eliminates this problem entirely. One issue that would need to be tightened up is the specification of what it means for two types to be "different". We've talked in the past about "bidirectionally compatible types" (type Another issue to consider is related to method access and binding. If classes |
Some of those compromises are things I've already said I'm fine with (Well, not entirely as stated, but close), but re-raised a question about something where someone else said it would be a problem or other issues with those compromises. See here I'm very much still wanting to work towards something that can work for everyone, but in unequivocal terms, if option 4 is accepted as-is, I'm personally done with python typing. There are enough issues with it for my real world use that this would kill typing usability for me long term as this started to be used in that fashion, and I've already explained how those would manifest. The fact that I am opposed to one option, but still working towards finding others that meet multiple groups needs is not an unwillingness to find compromise at all, but an unwillingness to accept a solution which has major flaws for my own use when there is more to explore. |
I was viewing option 6 as also banning methods, properties, and functions with diferring types on access as well when I wrote it. The primary reason for allowing overlap at all is the unavoidable overlaps of things inherited from object, but the rule "just working" without special casing those things was good.
bidierectionally compatible is almost fine for what I was considering when proposing that (See below, because I think we do need to be careful in wording this), I can come up with more formal definitions as needed if this approach is viable for others here.
methods should be fine here with how I was considering the option when I proposed it, the type of (A & B).method would bind to (A & B), We can use type[T] / Self here to improve reasoning about this when considering unbound methods prior to binding. This may sneak a small bit of special casing into implementations that don't understand method binding or descriptors though, and is definitely worth making sure we spell out to avoid diverging implementations. |
They only go away partially. Please do not ban callables from intersections entirely, we have a stated use case in this repo that still works with this option.
|
You just accused another collaborator of not being willing to compromise in the same post when they are here still working on a compromise. You are continuing to not read or otherwise ignore other people's contributions to this thread, and even so, I'd rather you keep providing your input here if you have something valuable to say. I don't think competing PEPs are the answer. We can make the PEP stronger by finding what issues people have with it, and that includes any issues you have with it. |
Sort of? I said an intersection would only make sense to me when I care about disjoint types, and that's true, but there are cases for extending base functionality beyond what this would support. However, the thing that @mark-todd and @mikeshardmind went back and forth on in discord and here with |
That's a good point - I hadn't considered it, but you're right it saves us from that issue.
One property of the above description is I was trying to make A.x and B.x effectively interchangeable. If we consider Literal[True, False] to be identical to bool, it might matter which from A and B gets chosen.
Interesting edge case! I think these would be compatible, returning the new type (A & B) as Self, like you describe. If we found down the road though that this has to be banned I don't think that's the end of the world.
Oh ok, great! Apologies, I didn't realise this
Yeah I was thinking about the case of combining two Callables - I see that so long as the other item in the intersection doesn't have a call method that should be find.
Yeah I think separating that behaviour is a good plan - there's certainly a use case for it but I think it can go into a different PEP. |
|
The Issue got too long again. Please continue discussing in #37. Please open new Issues if you start discussing on new sub aspects. |
Following on from the lengthy discussion here #1, it was concluded that
Any & Tis the best resultant type for intersecting Any. This is symmetric with the way union worksAny | T -> Any | T. Conversation on this new thread will investigate the types of the attributes and methods of this intersection type. Just a note, inspired by @CarliJoy we can number and summarise different interpretations. We should also seek to again create a real world example that explores the new types, and compares different interpretations.Also if a summary of each new interpretation could be succinctly provided alongside a usage example that would be grand :)
The text was updated successfully, but these errors were encountered: