Skip to content
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

General Organisation / How to continue / Consensus Finding #8

Open
CarliJoy opened this issue Jul 25, 2023 · 2 comments
Open

General Organisation / How to continue / Consensus Finding #8

CarliJoy opened this issue Jul 25, 2023 · 2 comments

Comments

@CarliJoy
Copy link
Owner

CarliJoy commented Jul 25, 2023

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 & Any Problem

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

@mikeshardmind
Copy link
Collaborator

mikeshardmind commented Jul 26, 2023

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
Copy link

The logic of keeping Any & T dual to Any | T rather than banning it or asymmetrically reducing it makes sense.

Is this what's going into the PEP?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants