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

[red-knot] Simplify unions of T and ~T #15400

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

sharkdp
Copy link
Contributor

@sharkdp sharkdp commented Jan 10, 2025

Summary

Simplify unions of T and ~T to object.

Test Plan

Adapted existing tests.

@sharkdp sharkdp added the red-knot Multi-file analysis & type inference label Jan 10, 2025
@@ -21,22 +21,22 @@ else:
if x and not x:
reveal_type(x) # revealed: Never
else:
reveal_type(x) # revealed: Literal[0, "", b"", -1, "foo", b"bar"] | bool | None | tuple[()]
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In these first four, only the order changed slightly.

@@ -87,10 +87,10 @@ def f(x: A | B):
if x and not x:
reveal_type(x) # revealed: A & ~AlwaysFalsy & ~AlwaysTruthy | B & ~AlwaysFalsy & ~AlwaysTruthy
else:
reveal_type(x) # revealed: A & ~AlwaysTruthy | B & ~AlwaysTruthy | A & ~AlwaysFalsy | B & ~AlwaysFalsy
reveal_type(x) # revealed: A | B
Copy link
Contributor Author

@sharkdp sharkdp Jan 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

According to the descriptions in #14687, we have

~AlwaysTruthy = Falsy
~AlwaysFalsy = Truthy

and

Truthy | Falsy = U = object (U is the Universal Set in set theory)

So we can rewrite what we had before to prove that this is correct:

  A & ~AlwaysTruthy | B & ~AlwaysTruthy | A & ~AlwaysFalsy | B & ~AlwaysFalsy
= A & Falsy | B & Falsy | A & Truthy | B & Truthy
= A & Falsy | B & Falsy | A & Truthy | B & Truthy
= A & Falsy | A & Truthy | B & Falsy | B & Truthy
= A & (Falsy | Truthy) | B & (Falsy | Truthy)
= A & object | B & object
= A | B

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To show that no narrowing happens (i.e. that we still have A | B) also seems to be the intention of this test.


if x or not x:
reveal_type(x) # revealed: A & ~AlwaysFalsy | B & ~AlwaysFalsy | A & ~AlwaysTruthy | B & ~AlwaysTruthy
reveal_type(x) # revealed: A | B
Copy link
Contributor Author

@sharkdp sharkdp Jan 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same proof as above, just starts with a reordered union.

@@ -214,10 +214,10 @@ if x and not x:
reveal_type(y) # revealed: A & ~AlwaysFalsy & ~AlwaysTruthy
else:
y = x
reveal_type(y) # revealed: A & ~AlwaysTruthy | A & ~AlwaysFalsy
reveal_type(y) # revealed: A
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Similar to above:

  A & ~AlwaysTruthy | A & ~AlwaysFalsy
= A & Falsy | A & Truthy
= A & (Falsy | Truthy)
= A & object
= A

Copy link
Contributor

github-actions bot commented Jan 10, 2025

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

@sharkdp sharkdp force-pushed the david/union-of-type-and-its-complement branch from 29f0bf5 to fcb9795 Compare January 10, 2025 13:50

# TODO: It should be A. We should improve UnionBuilder or IntersectionBuilder. (issue #15023)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR does not resolve #15023, but we can remove the TODO comment nevertheless.

Copy link
Contributor

@carljm carljm left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

@@ -80,6 +82,17 @@ impl<'db> UnionBuilder<'db> {
return self;
} else if element.is_subtype_of(self.db, ty) {
to_remove.push(index);
} else if ty_negated.is_subtype_of(self.db, *element) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there an argument for inlining the negation to ensure we avoid doing it if one of the above cases matches? We only use ty_negated once.

Suggested change
} else if ty_negated.is_subtype_of(self.db, *element) {
} else if ty.negate(self.db).is_subtype_of(self.db, *element) {

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
red-knot Multi-file analysis & type inference
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants