[red knot] add `Type::is_disjoint_from` and intersection simplifications by sharkdp · Pull Request #13775 · astral-sh/ruff

sharkdp · 2024-10-16T12:12:30Z

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 astral-sh/ty#245

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()

crates/red_knot_python_semantic/src/types.rs

github-actions · 2024-10-16T12:26:34Z

`ruff-ecosystem` results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/src/types/builder.rs

carljm · 2024-10-17T22:28:41Z

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.

FWIW, I'm quite open to the idea that we discard the positive/negative approach in favor of a Type::Not, if it makes intersection simplification easier.

The downside is we then have to add handling for Type::Not throughout the type system, but I suspect that may actually not be too difficult, since in many places we can just treat it as object, which is less precise but never unsound.

carljm

This is great! I suspect that this approach will carry us a long way; I'm not feeling any particular need to explore more radical approaches. (I'm not 100% sure, but I suspect that the lazy-BDD approach I linked you to may just not be workable anyway for the complexity of Python's type system; particularly inheritance and multiple inheritance.)

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/src/types/builder.rs

…in common way

carljm

Looks like this is still in-process, so didn't do a full re-review of the code, just a few responses to inline comments.

carljm · 2024-10-18T16:04:42Z

crates/red_knot_python_semantic/src/types.rs

+            (ty @ (Type::Function(..) | Type::Module(..) | Type::Class(..)), other)
+            | (other, ty @ (Type::Function(..) | Type::Module(..) | Type::Class(..))) => {
+                ty != other
+            }


It just occurred to me now on second read-through that this case is incorrect if it comes before the union case, because the union of two Type::Function is not disjoint from one of those same Type::Function.

I think this case is really the same as the None and Literal types case below, and could probably just be merged with it?

Would be good to add a test case that would have caught this (to create a union of function or class types, define them in if/else branches.)

It just occurred to me now on second read-through that this case is incorrect if it comes before the union case, because the union of two Type::Function is not disjoint from one of those same Type::Function.

Ah, you're right.

I think this case is really the same as the None and Literal types case below, and could probably just be merged with it?

👍

Would be good to add a test case that would have caught this (to create a union of function or class types, define them in if/else branches.)

Yes. I added a test that failed with the previous version.

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/src/types/builder.rs

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/src/types/builder.rs

carljm · 2024-10-18T20:59:45Z

crates/red_knot_python_semantic/src/types.rs

+            (Type::BooleanLiteral(..), Type::Instance(class_type))
+            | (Type::Instance(class_type), Type::BooleanLiteral(..)) => !matches!(
+                class_type.known(db),
+                Some(KnownClass::Bool | KnownClass::Object)


Because bool is a subtype of int in Python (sadly), we must also include KnownClass::Int here.

There was already a test for this case, but it asserted wrongly that int and a BooleanLiteral were disjoint; I switched it to assert the opposite.

There was also an IntersectionBuilder test relying on this assumption of bool/int disjointness; I fixed it by using a StringLiteral instead of a BooleanLiteral.

carljm

This is excellent work, thank you!!

sharkdp added the ty Multi-file analysis & type inference label Oct 16, 2024

sharkdp commented Oct 16, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Show resolved Hide resolved

sharkdp force-pushed the david/dnf-type-simplifications branch from cd903c3 to e94ba83 Compare October 16, 2024 14:43

sharkdp added 15 commits October 17, 2024 11:06

[red-knot] intersection type simplifications

81157e0

clean up

14dee2e

Handle more cases in disjoint_from

e06687c

Handle tuples, intersections

5770be6

Remove commented-out code

ccb9b1f

Fix tuples

d0063ed

Fix TODO

0f9ba92

Minor improvements

68eae7f

Add new simplification

68ab56e

Add simplification for bools

4b95c65

Add rule for S & T = S

1917618

Remove/reduce simplify

8d78019

Additional rules

1737dd8

Mirror version of the bool rule

98df522

Handle more cases in disjoint_from

2bd1789

sharkdp force-pushed the david/dnf-type-simplifications branch from e94ba83 to 2bd1789 Compare October 17, 2024 11:24

sharkdp commented Oct 17, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

Remove TODO

8ff474f

sharkdp commented Oct 17, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

sharkdp commented Oct 17, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

sharkdp commented Oct 17, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types/builder.rs Show resolved Hide resolved

sharkdp commented Oct 17, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types/builder.rs Show resolved Hide resolved

sharkdp added 3 commits October 17, 2024 14:00

Improve test coverage

6370969

Change test name

efe64d8

Fix instance checks

bf4af40

sharkdp force-pushed the david/dnf-type-simplifications branch from 215ef0c to bf4af40 Compare October 17, 2024 12:40

carljm requested changes Oct 18, 2024

View reviewed changes

sharkdp added 9 commits October 18, 2024 11:26

Use Iterator::find

76787c8

Fix is_disjoint_from(tuple, other)

e242909

Handle None, BooleanLiteral, IntLiteral, StringLiteral, BytesLiteral …

28f7b46

…in common way

Handle None in a more general way

06ecd88

Same for (Boolean|Int|String|Bytes)Literal

57b6949

Add test for BytesLiteral vs StringLiteral

599c9d6

Add TODO comment

7992f1d

Use test_cases instead of loop

ebd4b6e

Fix TODO regarding Any/Unknown/Todo

8d0ff15

carljm reviewed Oct 18, 2024

View reviewed changes

sharkdp added 5 commits October 18, 2024 20:02

Fix comment regarding tuples

3282c0c

Add support for removing multiple elements in one go

1b66358

Add 'object' as a third type to the boolean simplification tests

9eddcbe

Add 'third' type to simplification unit tests

e0cfef4

Fix is_disjoint for function/class/module

34b0383

sharkdp force-pushed the david/dnf-type-simplifications branch from c2930da to 34b0383 Compare October 18, 2024 20:15

sharkdp added 2 commits October 18, 2024 22:24

Add test for union of class types

eaa3d48

Add TODO comment regarding KnownClass::Type

3d4bd52

sharkdp commented Oct 18, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types/builder.rs Show resolved Hide resolved

carljm reviewed Oct 18, 2024

View reviewed changes

bool and int are not disjoint

b3b0ffb

carljm force-pushed the david/dnf-type-simplifications branch from e5af7c9 to b3b0ffb Compare October 18, 2024 21:29

carljm approved these changes Oct 18, 2024

View reviewed changes

carljm enabled auto-merge (squash) October 18, 2024 21:31

carljm merged commit 6964eef into main Oct 18, 2024

carljm deleted the david/dnf-type-simplifications branch October 18, 2024 21:34

sharkdp mentioned this pull request Oct 21, 2024

[red-knot] Support for not equal narrowing #13749

Merged

AlexWaygood mentioned this pull request Oct 1, 2025

[ty] Fix simplification of T & ~T for non-fully-static types #20651

Draft

Comments

Conversation

sharkdp commented Oct 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Open questions:

Test Plan

Uh oh!

Uh oh!

github-actions bot commented Oct 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

ruff-ecosystem results

Linter (stable)

Linter (preview)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carljm commented Oct 17, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

carljm left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carljm left a comment

Choose a reason for hiding this comment

Uh oh!

carljm Oct 18, 2024

Choose a reason for hiding this comment

Uh oh!

sharkdp Oct 18, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carljm Oct 18, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

carljm left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sharkdp commented Oct 16, 2024 •

edited

Loading

github-actions bot commented Oct 16, 2024 •

edited

Loading

`ruff-ecosystem` results

carljm commented Oct 17, 2024 •

edited

Loading

carljm Oct 18, 2024 •

edited

Loading