mikeshardmind
commented
1 year ago From my perspective, I think if we take the general rules as erictraut has provided them as a concise and solid baseline, the primary issue remaining has been disagreement about is how Any should be handled, and how we can prevent intersections from creating new ways for current missing features in type expressions to cause problems (#17)
Handling reductions and impossibility does not need to be mandated by the PEP, and can be left to type checkers as what follows naturally from the PEP, but I think it may be worth at least including the 3 or 4 (depending on the decisions made on Any) most trivial reductions that should not change over time, even if only as an example of what type checkers may simplify and not as a mandate*
Any & T -> T (If and only if this is the decision on Any)- T & Never -> Never
- T & object -> T
- T & T -> T
I do think for the sake of consistency in discussions about this, we should recommend disjunctive normal form ** as the canonical form for expressing combinations of unions and intersections, but as long as we either have a canonical form or say that we leave the user's presentation untouched, either is fine. (Note: leaving the user's presentation untouched may not be feasible or come at additional costs if it becomes desirable for a type checker to reduce a combination of unions and intersections internally)
WRT: Any & T, I view it as irreducible at this point in time for reasons that are detailed in how I've gone about generalizing attribute access on Intersections here but I think this generalization should be double checked by others for soundness before it is adopted. However, I view this irreducibility as being functionally equivalent to Any & T reducing to Any for structural use, and am not sure this is a good thing overall. generally speaking, I consider the inclusion of Any in an intersection to be more likely to indicate a misunderstanding than be intentional.
* Actually, we have a case where we need to be sure type checkers don't diverge behaviorally, see #17 ** #22 See here for slightly more detail on where CNF is useful as well.
alexchandel
In the different issues a lot of valid points were given, that the current specification is too complex and unsound.
I recognized that I really lack the fundamentals to keep track with discussion about type theory. Still as user I would like to see this implemented (especially for Mixins). Therefore I would like to help as much as I can i.e. in trying to keep order with issues, help organizing and maybe write things/read through them from an "normal (=not experienced with type theory)" Python user perspective.
@erictraut already did very good job in writing some general rules and applying them to the
T & AnyProblemThis could probably replace the current specification - hopefully I soon find time to put this into the current document.
I also was so free and included the original work of Kevin Millikin (@kmillikin) and Sergei Lebedev (@superbobry) from there PEP inside the specification document in order to create more context. Hote that they also created PEP draft propsal for a python type system spec. This could also help clarify some thing here.
I see still the open point how to handle 'impossible' intersections that needs some discussion before reaching a consensus.
@mikeshardmind @tomasr8 @NeilGirdhar @JelleZijlstra @DiscordLiz -> Maybe you could also summarize in your understanding the current consensus and disagreement we have? This helps finding the pain points of disagreement and finding a consensus.
One note about organisational stuff: I will be on holiday 2023-07-28 t 2023-08-07 and also as I don't want to be a door keeper of any kind feel free to become a contributor and edit the draft yourself :-). I am happy for every help.