-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
[red-knot] handle sealed types #12694
Labels
red-knot
Multi-file analysis & type inference
Comments
Other examples of sealed types are the various singletons available in
|
carljm
added a commit
that referenced
this issue
Sep 1, 2024
The `UnionBuilder` builds `builtins.bool` when handed `Literal[True]` and `Literal[False]`. Caveat: If the builtins module is unfindable somehow, the builder falls back to the union type of these two literals. First task from #12694 --------- Co-authored-by: Carl Meyer <[email protected]>
carljm
added a commit
that referenced
this issue
Oct 18, 2024
…ons (#13775) ## Summary - Add `Type::is_disjoint_from` as a way to test whether two types overlap - Add a first set of simplification rules for intersection types - `S & T = S` for `S <: T` - `S & ~T = Never` for `S <: T` - `~S & ~T = ~T` for `S <: T` - `A & ~B = A` for `A` disjoint from `B` - `A & B = Never` for `A` disjoint from `B` - `bool & ~Literal[bool] = Literal[!bool]` resolves one item in #12694 ## Open questions: - Can we somehow leverage the (anti) symmetry between `positive` and `negative` contributions? I could imagine that there would be a way if we had `Type::Not(type)`/`Type::Negative(type)`, but with the `positive`/`negative` architecture, I'm not sure. Note that there is a certain duplication in the `add_positive`/`add_negative` functions (e.g. `S & ~T = Never` is implemented twice), but other rules are actually not perfectly symmetric: `S & T = S` vs `~S & ~T = ~T`. - I'm not particularly proud of the way `add_positive`/`add_negative` turned out. They are long imperative-style functions with some mutability mixed in (`to_remove`). I'm happy to look into ways to improve this code *if we decide to go with this approach* of implementing a set of ad-hoc rules for simplification. - ~~Is it useful to perform simplifications eagerly in `add_positive`/`add_negative`? (@carljm)~~ This is what I did for now. ## Test Plan - Unit tests for `Type::is_disjoint_from` - Observe changes in Markdown-based tests - Unit tests for `IntersectionBuilder::build()` --------- Co-authored-by: Carl Meyer <[email protected]>
Singleton types are a degenerate case of sealed types. They are sealed, but they don't require the handling discussed in this issue, since there is no equivalence to a union (except in the sense that all types are equivalent to a union of just that type, but we don't allow building size-one unions.) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Some types have a finite number of possible inhabitants. Examples include
builtins.bool
(the inhabitants areLiteral[True]
andLiteral[False]
) and enum types. For such types, we should consider the union of all possible inhabitants as equivalent to the type itself (so for exampleLiteral[True, False]
) is equivalent tobuiltins.bool
). We should also take this equivalence into account when resolving negated intersections (so for examplebuiltins.bool & ~Literal[True]
is equivalent toLiteral[False]
; practically this will come up in type narrowing.)Tasks here, in the order we'll likely get to them:
Literal[True] | Literal[False]
tobuiltins.bool
builtins.bool
back toLiteral[True] | Literal[False]
when intersection eliminates a type inhabitantThe text was updated successfully, but these errors were encountered: