[red-knot] Ensure differently ordered unions and intersections are considered equivalent #15516

AlexWaygood · 2025-01-15T22:21:05Z

Summary

Currently, we don't understand that str | int and int | str are equivalent types; nor do we understand that P & T ≡ T & P. This PR fixes that, by ensuring that we never construct a str | int union -- str | int is simplified to int | str during constructions via a sorting algorithm introduced by this PR. (For instance types from the same module, specifically, the algorithm puts the instance types in alphabetical order.) This ensures that the trivial case of int | str ≡ str | int can be handled, well, trivially, with our existing logic in Type::is_equivalent_to(). An added benefit of this approach should be reduced memory usage, since we'll only ever store int | str in the Salsa db, never str | int.

Fixing #15380 means that we can now promote the subtype_of_is_antisymmetric property test from flaky to stable 🎉

Why not just implement `Ord` on `Type`?

It would be fairly easy to slap #[derive(PartialOrd, Ord)] on Type. However, this would order types according to their Salsa ID. While this would mean that types would always be consistently ordered in any single run of red-knot, the order in which they would appear might vary between different runs of red-knot. Unless we implemented an entirely different order for display purposes, this would make it difficult to write mdtests, and would also be quite confusing for users.

Moreover, it doesn't really "make sense" for Type to implement Ord in terms of the semantics. There are many different ways in which you could plausibly sort a list of types; the algorithm implemented in this PR is only one (somewhat arbitrary, at times) possible ordering.

Costs of this approach

This approach does have several costs! Firstly, it makes the construction of unions and intersections more expensive. I think this tradeoff is worth it considering the reduced memory usage, and considering that Type::is_equivalent_to() does not need to be O(n^2) for unions and intersections with this change (at least for now). It's also possible that we could mitigate the performance penalty by maintaining the union/intersection elements in sorted order at all times while the union/intersection is being constructed. I haven't looked too hard at this yet, partly because I wanted to keep the diff clean and easy to understand. I also wasn't sure how high a performance cost this might be -- I'm interested to see what codspeed says here!

Another cost to this approach is that it might be confusing for users to see unions displayed in a different order to the order the user gave them in annotations. I don't see this as a significant cost, however, as we already perform many simplifications and rearrangements of unions and intersections.

Lastly, this doesn't solve all problems with Type::is_equivalent_to() that we'll ever encounter. When we implement protocols, for example, we'll need to understand P and Q in the following example as being equivalent types, and we'll need to understand P | None as being equivalent to Q | None, etc.

from typing import Protocol

class P(Protocol):
    x: int

class Q(Protocol):
    x: int

But I think even when we get to these more advanced and trickier problems, having union and intersection elements guaranteed to always be in a predictable order should make answering the question of equivalence easier to do with a complexity less than O(n^2).

Implementation details

The algorithm for sorting union/intersection elements is placed in a new submodule, crates/red_knot_python_semantic/src/types/type_ordering.rs. Other than this algorithm, the only significant changes made are to add a few .sort_by() calls to UnionBuilder::build() and InnerIntersectionBuilder::build().

Test Plan

Many existing mdtests updated
New mdtests added
One property test promoted to stable
Two new property tests added. Both need to be marked as flaky for now, due at least in part to:
- [red-knot] AlwaysTruthy | bool is equivalent to AlwaysTruthy | Literal[False] #15513
- [red-knot] type & ~Literal[True] & bool should simplify to Never #15508
Ran QUICKCHECK_TESTS=1000000 cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::stable to verify that the stable property tests all pass. I also ran QUICKCHECK_TESTS=1000000 cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::flaky and examined the failures for the two added flaky property tests to check whether they looked related to the sorting algorithm; I couldn't find any that were.

github-actions · 2025-01-15T22:29:11Z

`ruff-ecosystem` results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

AlexWaygood · 2025-01-15T22:41:58Z

1% regression on codspeed. I'll wait for review comments before trying to optimise this

MichaReiser · 2025-01-16T06:43:18Z

crates/red_knot_python_semantic/resources/mdtest/annotations/string.md

@@ -105,7 +105,7 @@ def f1(
 from typing import Literal

 def f(v: Literal["a", r"b", b"c", "d" "e", "\N{LATIN SMALL LETTER F}", "\x67", """h"""]):
-    reveal_type(v)  # revealed: Literal["a", "b", b"c", "de", "f", "g", "h"]
+    reveal_type(v)  # revealed: Literal["a", "b", "de", "f", "g", "h", b"c"]


I still think there's value in preserving the source order. E.g I would find this confusing as a user. The same in the example above. It's not the end of the world, but it is irritating.

I agree. I wouldn't want something like int | str | None to be reordered to int | None | str in the output of the type checker (just an example with case-ignoring alphabetical order, not sure if that's the actual order we would choose here).

The idea in this comment was that we could potentially keep a second list inside Union and Intersection structs that would keep track of this order — if sensible to do so. As in: we could always opt-out if we need to perform complex operations on unions/intersections, but we would try to preserve it on a best-effort basis.

I'm imagining something like this: When a user specifies the type int | str | None in an annotation, we would create an internal union type that conceptually looks like this:

Union { elements: [int, None, str], user_order: Some([0, 2, 1]) }

The idea would be that we could usually ignore this user_order field, but then try to reconstruct the original order in the rare case that we need to display a type to the user.

It might be fine as a first solution to switch to user_order: None as soon as we perform any sort of operation on the union type. But I think we could even try to do better by creating new user_orders in a limited set of operations. For example, when joining two unions (A | B) | (C | D), which would both have user_order: Some([0, 1]), we could probably join these by adding max(lhs.user_order) + 1 to all elements on the right hand side:

Union { elements: [A, B, C, D], user_order: Some([0, 1, 2, 3])

The idea in this comment was that we could potentially keep a second list inside Union and Intersection structs that would keep track of this order — if sensible to do so. As in: we could always opt-out if we need to perform complex operations on unions/intersections, but we would try to preserve it on a best-effort basis.

One issue I see with this approach -- that also exists in our current approach on main -- is that it means that our incremental type-checking is very sensitive to the exact source order of union elements. E.g. if somebody made this change in their source code

- x: None | int + x: int | None

then that might trigger a lot of otherwise-unnecessary recomputation. The type before the change would not compare equal with the type after the change, even though it represents the exact same set of union elements, because the type inferred for x would contain a record of the source-order of elements. It will also result in higher memory usage for us.

One idea I've had in the past is that types could have an Option<(File, TextRange)> field -- Type::display could just go back to the original source code and get the exact original representation of the type. This would be elegant in some ways because it also solves tricky problems such as this:

type T = int | str | memoryview | Literal["foo", "bar", "baz", "spam"] def f(x: T): reveal_type(x) # ideally we'd say "Revealed type is `T`" # rather than saying "Revealed type is `int | str | memoryview | Literal["foo", "bar", "baz", "spam"]`"

But carrying a TextRange attribute around would make our incremental type-checking even more sensitive to trivia such as the exact amount of whitespace prior to the type definition, etc.

then that might trigger a lot of otherwise-unnecessary recomputation. The type before the change would not compare equal with the type after the change, even though it represents the exact same set of union elements, because the type inferred for x would contain a record of the source-order of elements.

I'm not too concerned about this. We need to do well at dealing with this because it's no different from when the user makes an actual meaning full change.

But carrying a TextRange attribute around would make our incremental type-checking even more sensitive to trivia such as the exact amount of whitespace prior to the type definition, etc.

I consider this a problem because it means any change will invalidate any public type in that module, unless we hide it behind a salsa interned but that has other costs. It also has the downside that types with a range are displayed differently from types without a range (e.g. it doesn't join Literal values etc).

Have we looked into how other type checkers (TypeScript, flow, Pyright, mypy) handle and represent union types?

It seems TypeScript carries the origin type along

https://github.com/microsoft/TypeScript/blob/4a18b5cf8d41975c86cde25a0b2229f81e3b08d2/src/compiler/types.ts#L6682-L6695

It also seems that preserving the original notation has advantages other than just to display a union

https://github.com/microsoft/TypeScript/blob/4a18b5cf8d41975c86cde25a0b2229f81e3b08d2/src/compiler/checker.ts#L22445-L22458

then that might trigger a lot of otherwise-unnecessary recomputation. The type before the change would not compare equal with the type after the change, even though it represents the exact same set of union elements, because the type inferred for x would contain a record of the source-order of elements.

I'm not too concerned about this. We need to do well at dealing with this because it's no different from when the user makes an actual meaning full change.

But carrying a TextRange attribute around would make our incremental type-checking even more sensitive to trivia such as the exact amount of whitespace prior to the type definition, etc.

I consider this a problem because it means any change will invalidate any public type in that module, unless we hide it behind a salsa interned but that has other costs. It also has the downside that types with a range are displayed differently from types without a range (e.g. it doesn't join Literal values etc).

Fair enough. It sounds like maintaining a separate boxed array recording the source order would be the way to go here, then, like @sharkdp suggests.

It also has the downside that types with a range are displayed differently from types without a range (e.g. it doesn't join Literal values etc).

Hmm, but I thought that this was what you were arguing we wanted -- I thought you were arguing that we should display the type as the user presented it, without any simplifications, if the type comes directly from a user annotation.

Have we looked into how other type checkers (TypeScript, flow, Pyright, mypy) handle and represent union types?

Mypy does not eagerly simplify unions at all; it only lazily simplifies them. This means that it has to do a lot of recomputation that for us is unnecessary. Pyright does some simplification (it deduplicates elements) but not nearly as much as we do (it doesn't remove a subtype from a union if the supertype is present). Even when it removes duplicate elements, it maintains order among the other elements (which we don't do because we use swap_remove()): https://pyright-play.net/?code=GYJw9gtgBALgngBwJYDsDmUkQWEMogCmAboQIYA2A%2BvAoQFCMAmhwUwAFAB4BcmK%2BAD5QAzjBBRhqIVABGYMBUlQIhCLjjEkhAO7LgFMGRnTlFJGIDaYkAF1lTJAGMY18QBp%2BMe8JgBXBApCSw4ASltQnnooGIIScmpaQm5QoA.

It also seems that preserving the original notation has advantages other than just to display a union

microsoft/TypeScript@4a18b5c/src/compiler/checker.ts#L22445-L22458

How did you obtain that link?? When I click on it, GitHub just shows me this 😆

I open it in VS code / Rust Rover and then do Ctrl+P Copy link

Yeah, I think we probably should continue to make an effort to not reorder user-authored types that we haven't simplified (and that it's ok to reorder in simplifying.)

As far as how we do this, I spent some time thinking about whether there could be solution overlap with the more general case of showing users a nice short type alias name instead of the complex type it aliases, which I think we will also want to do, as in Alex's example above. The proposal of carrying around a TextRange doesn't work, as discussed, because it is too sensitive to unrelated source-code changes. I'm not really coming up with any good unified solution here, though; I don't think we want every union/intersection type carrying around a string, for example. So it may be best to go with separate solutions here; a user_order field for unions and intersections, and something else (maybe something like a lookup table mapping types to their known aliases in a file?) for the type alias case.

MichaReiser

This is a great write up with a lot of context. Thank you.

this would make it difficult to write mdtests,

I don't think this is true. The order is predictable for as long as no multi-threading is involved.

astly, this doesn't solve all problems with Type::is_equivalent_to() that we'll ever encounter.

I'd like to understand this more. What makes Protocols different from what we have today? How would sorting the types help?

I do remain concerned about reordering types, especially if that ordering is non-obvious and, therefore, appears to be arbitrary for users. I often write my TypeScript types with a specific order in mind, e.g. group semantically relevant types first and I'd find it rather annoying if the extension removes that ordering when hovering over the type.

I think this is different from making other simplifications because it sort of teaches me how I could have written my type instead, although I have slight reservations there as well.

crates/red_knot_python_semantic/src/types/type_ordering.rs

AlexWaygood · 2025-01-16T11:24:39Z

this would make it difficult to write mdtests,

I don't think this is true. The order is predictable for as long as no multi-threading is involved.

Oh, interesting; I didn't think that through. And we don't use multi-threading in red-knot as invoked by red_knot_test?

I still think it's useful generally for the display of types to be stable between red-knot runs. Among plausible benefits to this, I can think of:

Less user confusion
Should help with persistent caching?
Probably makes it easier to write integration CLI tests that assert the output of red-knot on the command line?

Lastly, this doesn't solve all problems with Type::is_equivalent_to() that we'll ever encounter.

I'd like to understand this more. What makes Protocols different from what we have today? How would sorting the types help?

Well, it didn't help that I forgot to actually write up the example in my initial PR description 🙃 I've edited it in now.

The difference with Protocols is that they use structural subtyping rather than nominal subtyping. I.e. in the following example, Unrelated is not a subtype of Nominal, because it does not explicitly inherit from Nominal, and the type Nominal represents "all possible instances of the Nominal class at runtime". Unrelated is a subtype of Structural, however, because one class does not have to explicitly inherit from a structural type in order for there to be a subtyping relationship between the corresponding types. The type Structural represents "all possible objects that have a mutable instance attribute x with a type that is assignable to int".

from typing import Protocol

class Nominal:
    x: int

class Structural(Protocol):
    x: int

class Unrelated:
    x: int

Going back to the example I've edited into my PR description: the types P and Q are equivalent, because they both represent "all possible objects that have a mutable instance attribute x with a type that is assignable to int". But we can't "simplify" one type into the other type, which has been our approach for many of these equivalence issues, because otherwise you'd get things like this, which would be a truly terrible user experience -- especially if Q is defined in user code but P comes from a third-party library:

def _(obj: Q):
    reveal_type(obj)  # revealed: P

So when we get to protocols (and TypedDicts, which are similar), it will absolutely be necessary to implement some more complex equivalence logic that is more complex and costly than just "eagerly simplify one type into its equivalent type at type construction time, and then check for equivalence using a simple equality comparison". Nonetheless, the reason why I say that this PR might help make even equivalence between protocol types easier to implement is because with this approach we only need to do the complicated equivalence check between two protcol types or between two typeddict types -- and with this PR, we know exactly "where" in the list of union elements protocol types and typedict types will lie, relative to all other types that might be included in the union.

I think this is different from making other simplifications because it sort of teaches me how I could have written my type instead, although I have slight reservations there as well.

I know what you mean, but our existing simplifications already frequently perturb the order of unions and intersections because of our use of swap_remove and swap_remove_indexinUnionBuilderandInnerIntersectionBuilder`

sharkdp · 2025-01-16T11:45:46Z

I think this is different from making other simplifications because it sort of teaches me how I could have written my type instead, although I have slight reservations there as well.

I know what you mean, but our existing simplifications already frequently perturb the order of unions and intersections because of our use of swap_remove and swap_remove_indexinUnionBuilderandInnerIntersectionBuilder`

I think Micha was trying to say that reorderings are fine if any simplifications are performed. But the default case will be that users write union-type annotations that can not be simplified, and maybe we should try a bit harder to make the UX in this case better. It's great that we can simplify Literal[False] | str | Literal[True] to bool | str, or int | object | str to object. But nobody will write that in reasonable user code (and if they do, they will probably be okay with being presented with the simplified version of their type).

(don't get me wrong, I am very much excited about this PR 👍)

AlexWaygood · 2025-01-16T11:48:33Z

But nobody will write that in reasonable user code

I don't know about that. I've seen a lot of object | None and int | bool annotations in my time. And those aren't always a "mistake" -- int | bool is often done quite deliberately, even though folks know it will be simplified by the type checker, because people don't think of bool as being an int subtype even though they know that it is at runtime.

AlexWaygood · 2025-01-16T11:54:19Z

(don't get me wrong, I am very much excited about this PR 👍)

Thank you! And don't get me wrong -- I'm not wedded to the approach here! There are some really tricky tradeoffs to think through.

Even if we don't go with this approach, I don't consider this PR to be time wasted, because of the number of bugs I discoverered along the way:

[red-knot] tuple & AlwaysFalsy should simplify to tuple[()] #15528
[red-knot] AlwaysTruthy | bool is equivalent to AlwaysTruthy | Literal[False] #15513
[red-knot] type & ~Literal[True] & bool should simplify to Never #15508
[red-knot] Simplify object out of intersections #15511
[red-knot] Fix more edge cases for intersection simplification with LiteralString and AlwaysTruthy/AlwaysFalsy #15496
[red-knot] Corrections and improvements to intersection simplification #15475

carljm · 2025-01-16T15:33:23Z

Thanks for this!

I do think it's likely that even with more complex equivalence cases, this can make equivalence a lot cheaper to implement, as long as our equivalent-types reliably end up sorted near each other.

(As a side note, I'm not sure it will ever be necessary, or even an improvement in practice, that we consider two different Protocol types such as P and Q to be equivalent, although technically they are. We will need to consider either one assignable to the other, but for example I don't know that we should simplify the union P | Q to either P or Q.)

carljm · 2025-01-16T15:37:08Z

I guess in terms of next steps, if we are in agreement on the above discussion of user order preservation, the question would be whether we land this as-is and introduce user-order preservation as a follow-up, or add user-order preservation to this PR. I think probably the latter is better, as otherwise it'll be a lot more churn and re-churn to the mdtest output?

AlexWaygood · 2025-01-16T17:42:13Z

(As a side note, I'm not sure it will ever be necessary, or even an improvement in practice, that we consider two different Protocol types such as P and Q to be equivalent, although technically they are. We will need to consider either one assignable to the other, but for example I don't know that we should simplify the union P | Q to either P or Q.)

Right, though that would mean we'd have to abandon this property test if we decided not to recognise the equivalence there -- we'd have two types which would be mutual subtypes but would not be equivalent:

ruff/crates/red_knot_python_semantic/src/types/property_tests.rs

Lines 360 to 365 in e2da33a

    
           // `S <: T` and `T <: S` implies that `S` is equivalent to `T`. 
        
           // This very often passes now, but occasionally flakes due to https://github.com/astral-sh/ruff/issues/15380 
        
           type_property_test!( 
        
               subtype_of_is_antisymmetric, db, 
        
               forall types s, t. s.is_subtype_of(db, t) && t.is_subtype_of(db, s) => s.is_equivalent_to(db, t) 
        
           );

(This PR promotes that property test to stable)

carljm · 2025-01-16T17:49:51Z

Yeah, after more discussion in Discord I think we would want to simplify P | Q to a non-union structural type.

carljm · 2025-01-16T19:28:09Z

@AlexWaygood and I discussed today in 1:1 that deterministically sorting union/intersection elements and also tracking a user_order (which already loses us the property that str | int and int | str result in the same interned Salsa UnionType) is semantically indistinguishable from keeping the user-provided order just as we do today, and lazily producing the deterministic sorting of elements only when we actually need to compare two unions or intersections for equivalence (and possibly Salsa-memoizing that sorting, if that's a win in practice). The choice between the two approaches is a matter of performance, not correctness. I have half a suspicion that lazy sorting may turn out better, given that it means we won't have to do it for all unions. And I think it's probably simpler to implement as well. So I'd be inclined to try that first.

sharkdp · 2025-01-16T19:48:27Z

and lazily producing the deterministic sorting of elements only when we actually need to compare two unions or intersections for equivalence

Just one additional thought: The other scenario where the always-ordered canonical representation (proposed in this PR) would help would be during construction of unions and intersections, i.e. in the {Union,Intersection}Builders. The construction of unions and intersections — the way it's currently implemented — is also $\mathcal{O}(n^2)$, because we have simplification procedures for every insertion that are themselves $\mathcal{O}(n)$. Constructing these aggregate types in ordered fashion could potentially make those simplification steps more efficient. For example: a search whether a particular other type is already part of a union/intersection could be reduced to $\mathcal{O}(\text{log}(n))$, making the whole construction potentially $\mathcal{O}(n\ \text{log}(n))$. I really don't know how much of a problem large unions/intersections are, so this might be misguided.

AlexWaygood · 2025-01-16T19:50:38Z

I really don't know how much of a problem large unions/intersections are, so this might be misguided.

Often quite a large problem! See #13549 for a summary of some of the many problems mypy and pyright have had with large unions of the years

carljm · 2025-01-16T19:52:03Z

No, that's a good point. I suspect that we should probably aim for "simplest implementation that gets the semantics right and isn't obviously inefficient" initially, and tackle deeper optimization as its own project, once we are faced with real-world projects with large-union problems (or at least some projects we can use as benchmarks that make heavier use of unions than tomllib.)

MichaReiser · 2025-01-16T20:18:25Z

We could also do the sorting lazily and cache the result in a separate field that's not part of eq using internal mutability

AlexWaygood · 2025-01-17T11:28:43Z

crates/red_knot_python_semantic/src/types.rs

-            (Type::Instance(instance), Type::SubclassOf(subclass))
-            | (Type::SubclassOf(subclass), Type::Instance(instance)) => {
-                let Some(base_class) = subclass.subclass_of().into_class() else {
-                    return false;
-                };
-
-                instance.class.is_known(db, KnownClass::Type)
-                    && base_class.is_known(db, KnownClass::Object)
-            }
-


I noticed that this branch was redundant, since we now eagerly normalize type[object] to type. But I could separate this out into another PR, if we prefer that

AlexWaygood · 2025-01-17T11:36:24Z

crates/red_knot_python_semantic/src/types/type_ordering.rs

+        (Type::StringLiteral(left), Type::StringLiteral(right)) => {
+            left.value(db).cmp(right.value(db))
+        }


now that the ordering is no longer user-facing, I'm not sure that Salsa db lookups like this in the ordering algorithm make sense anymore. I think it's still useful to make sure that all the StringLiteral elements are next to each other in the elements list, but I don't think it matters anymore whether Literal["bar"] comes before Literal["foo"]. So maybe I should just sort by the Salsa IDs here, which would be cheaper?

That makes sense to me

I implemented this in 64351be

AlexWaygood · 2025-01-17T12:14:54Z

crates/red_knot_python_semantic/src/types/type_ordering.rs

This now is basically equivalent to what we'd get if we just slapped #[derive(PartialOrd, Ord)] on Type, KnownInstanceType, SubclassOfType, ClassLiteralType, etc. So maybe we should just do that at this point -- it would certainly be less code. But it still doesn't make sense semantically (to me) for them to implement Ord. There are many different ways you could plausibly order types; this is only one possible (arbitrary) ordering

You could also define your own trait UnionElementOrd and implement your own derive macro. But that seems painful too :D

I'd probably with what you have now and you can create a (help wanted?) issue that adds a ArbitraryOrd (or similar) trait with a derive macro. Seems like a fun exercise for someone interested in Rust.

MichaReiser · 2025-01-17T12:14:13Z

crates/red_knot_python_semantic/src/types.rs

@@ -4204,6 +4211,18 @@ impl<'db> UnionType<'db> {
    ) -> Type<'db> {
        Self::from_elements(db, self.elements(db).iter().map(transform_fn))
    }
+
+    #[salsa::tracked]


Did you measure the performance impact of caching the sorted unions?

I'm asking because it's unclear to me if caching it always is worth it. E.g. sorting a union with only a few elements is super cheap. So maybe it's only worth calling into the cached variant after a certain threshold?

It might also be worth to test first if the union elements aren't sorted already

I pushed a commit shortly before your review to see what happens to the benchmarks if we don't cache them. Though I'm still worried about what will happen if we encounter very large unions, which do occur regularly in popular Python libraries such as pydantic (see #13549), even if they don't happen much in tomllib.

The benchmarks do seem to be much improved without the caching (codspeed is now neutral). So I guess it makes sense to keep these uncached for now until we benchmark how red-knot performs on projects with catastrophically huge unions.

It might also be worth to test first if the union elements aren't sorted already

it would be easier if we upgraded our MSRV to 1.82 :P

It shouldn't be too hard to implement ;)

done in 1e47693 :-)

The version where we first check to see whether it is already sorted before attempting to sort it does (I think) seem to be doing slightly worse on the benchmarks? But it's all within the noise range; I might be looking for signal here in something that's actually random variation.

crates/red_knot_python_semantic/src/types/type_ordering.rs

MichaReiser · 2025-01-17T12:24:29Z

crates/red_knot_python_semantic/src/types/type_ordering.rs

+        (_, Type::AlwaysFalsy) => Ordering::Greater,
+
+        (Type::KnownInstance(left_instance), Type::KnownInstance(right_instance)) => {
+            match (left_instance, right_instance) {


I think implementing PartialOrd for KnownInstance should be fine. I agree that Type itself should not implement Ord. It would drastically reduce the code needed here (and I'd probably to the same for other types, e.g. `ClassBase)

I think implementing PartialOrd for KnownInstance should be fine.

Hmm, why do you think it's okay for KnownInstanceType but not for Type? The two enums seem pretty similar to me in terms of whether it makes sense for them to implement Ord

I consider Type as the main public interface. I agree that probably the same argument applies as for Type.

I kinda feel inclined to either add it to Type and all its wrapped enums/structs or none of them. Writing it all out like this is a lot of boilerplate code, but it's not too hard to review it for correctness (it's all quite simple). But maybe it would be better to just write a macro here...

crates/red_knot_python_semantic/src/types/type_ordering.rs

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md

sharkdp · 2025-01-17T12:53:32Z

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md

+static_assert(is_equivalent_to(Intersection[Q, R, Not[P]], Intersection[Not[P], R, Q]))
+static_assert(is_equivalent_to(Intersection[Q | R, Not[P | S]], Intersection[Not[S | P], R | Q]))
+static_assert(is_equivalent_to(str | None, None | str))
+```


If I recall correctly, one of the original concerns with the ordering approach was that we would not recognize if two equivalent-but-not-Eq types like type and type[object] would be part of the union.

Can we add a test for this? Like

static_assert(is_equivalent_to(type[object] | P | type, type | P | type[object]))

Or do we already simplify unions with type and type[object]?

No wait, that's not the right test. More like:

static_assert(is_equivalent_to(type[object] | P, P | type))

If we don't recognize that yet, that's also okay. Might still be worth adding the test.

I imagined that we would design the ordering in such a way that those equivalence classes (w.r.t. is_equivalent_to) would be grouped together. Which would then make it easier to implement the Union(…) branch in is_equivalent_to.

Yeah. So far we've managed to get by here by ensuring that equivalent types are recognised as such by ensuring that only one of the two can ever appear in our internal model. So type[object] is eagerly simplified to type (meaning no special logic is necessary to implement the equivalence between the two), bool & AlwaysTruthy is eagerly simplified to Literal[True], etc.. There are some known places where we don't currently do this, but where I'm hopeful that we can, e.g. #15528 and #15513

But there will be types we encounter in the future where we cannot do the eager simplification from one type to the other: Protocols, TypedDicts, type aliases, there may be others.

So this is a good reason to keep the manual ordering rather than deriving #[PartialOrd, Ord] (links to the conversation I was having with @MichaReiser at #15516 (comment)), because we can see and control exactly how the types are ordered. But it makes it hard to test right now, because we haven't got that far yet in our implementation of the type system!

I don't think one necessarily precludes the other. We can automatically derive ordering for some types but manually implement ord where necessary (or our custom ordering trait)

AlexWaygood · 2025-01-17T19:15:20Z

I think this should be ready for another round of review now!

carljm

This looks good to me! I'm really not too concerned about custom trait vs macro vs explicit match; these are surface code organization issues that are easy to change later if we decide we don't like what we have.

carljm · 2025-01-17T21:55:04Z

crates/red_knot_python_semantic/src/types/property_tests.rs

+    );
+
+    // Equal element sets of intersections implies equivalence
+    // flaky at least in part because of https://github.com/astral-sh/ruff/issues/15508


The linked issue is closed. Was it closed prematurely, or is it not in fact the cause of this property test being flaky, or is this property test not in fact flaky?

Or did you mean #15528 here?

I think #15508 used to cause this property test to be flaky, and now #15513 causes this property test to be flaky. We need at least #15508 and #15513 and this PR (and possibly more fixes on top) for this property test to pass.

I realised that with the latest version of the PR, however, we can promote gradual_equivalent_to_is_symmetric to stable! I ran it for 2,000,000 iterations without any failures.

and now #15513 causes this property test to be flaky

e.g. it's given me this as a failing example, which looks pretty clearly #15513-related

---- types::property_tests::flaky::intersection_equivalence_not_order_dependent stdout ---- thread 'types::property_tests::flaky::intersection_equivalence_not_order_dependent' panicked at /Users/alexw/.cargo/registry/src/index.crates.io-6f17d22bba15001f/quickcheck-1.0.3/src/tester.rs:165:28: [quickcheck] TEST FAILED. Arguments: (KnownClassInstance(Bool), AlwaysFalsy, Intersection { pos: [], neg: [BooleanLiteral(false)] })

…tests (#15563) ## Summary Part of #15397 and #15516. ## Test Plan Markdown tests.

…is already sorted

AlexWaygood added the red-knot Multi-file analysis & type inference label Jan 15, 2025

AlexWaygood marked this pull request as ready for review January 15, 2025 22:42

AlexWaygood requested review from carljm, MichaReiser and sharkdp as code owners January 15, 2025 22:42

MichaReiser reviewed Jan 16, 2025

View reviewed changes

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

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

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

AlexWaygood force-pushed the alex/union-equivalence branch from c37f8d5 to 0034a03 Compare January 17, 2025 11:21

AlexWaygood commented Jan 17, 2025

View reviewed changes

AlexWaygood force-pushed the alex/union-equivalence branch from b022cf7 to 64351be Compare January 17, 2025 12:11

AlexWaygood commented Jan 17, 2025

View reviewed changes

MichaReiser reviewed Jan 17, 2025

View reviewed changes

sharkdp added the great writeup A wonderful example of a quality contribution label Jan 17, 2025

AlexWaygood changed the title ~~[red-knot] Ensure union elements and intersection elements always appear in sorted order~~ [red-knot] Ensure differently ordered unions and intersections are considered equivalent Jan 17, 2025

sharkdp reviewed Jan 17, 2025

View reviewed changes

crates/red_knot_python_semantic/resources/mdtest/type_properties/is_equivalent_to.md Outdated Show resolved Hide resolved

sharkdp reviewed Jan 17, 2025

View reviewed changes

carljm approved these changes Jan 17, 2025

View reviewed changes

InSyncWithFoo mentioned this pull request Jan 18, 2025

[red-knot] Migrate is_gradual_equivalent_to unit tests to Markdown tests #15563

Merged

carljm pushed a commit that referenced this pull request Jan 18, 2025

[red-knot] Migrate is_gradual_equivalent_to unit tests to Markdown …

9d845ec

…tests (#15563) ## Summary Part of #15397 and #15516. ## Test Plan Markdown tests.

AlexWaygood added 13 commits January 18, 2025 11:43

Ensure union and intersection elements always appear in sorted order

fbb5f10

remove redundant branches and rename functions

804474b

Move length-checking logic into order_sequences function

638037c

Discard most changes to mdtests

0d2a3b2

Discard changes to builder.rs

5b0da6c

sort unions and intersections lazily

5e033f8

update comments

53bba9c

reduce Salsa lookups in sorting algorithm

56b5167

what happens to the benchmarks if they're not salsa-tracked methods

5e5190f

update comments and rename functions

6978a48

better tests

88f7dbe

do not create new Unions/Intersections if the union/intersection …

4bd70b0

…is already sorted

fix pre-commit & micro-optimise

14cd669

AlexWaygood force-pushed the alex/union-equivalence branch from 9bf4a77 to 72277ef Compare January 18, 2025 11:58

final fixes

6496d9a

AlexWaygood force-pushed the alex/union-equivalence branch from 72277ef to 6496d9a Compare January 18, 2025 12:05

[red-knot] Ensure differently ordered unions and intersections are considered equivalent #15516

Are you sure you want to change the base?

[red-knot] Ensure differently ordered unions and intersections are considered equivalent #15516

Conversation

AlexWaygood commented Jan 15, 2025 • edited Loading

Summary

Why not just implement Ord on Type?

Costs of this approach

Implementation details

Test Plan

github-actions bot commented Jan 15, 2025 • edited Loading

ruff-ecosystem results

Linter (stable)

Linter (preview)

AlexWaygood commented Jan 15, 2025 • edited Loading

MichaReiser Jan 16, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood Jan 16, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MichaReiser left a comment • edited Loading

Choose a reason for hiding this comment

AlexWaygood commented Jan 16, 2025 • edited Loading

sharkdp commented Jan 16, 2025 • edited Loading

AlexWaygood commented Jan 16, 2025 • edited Loading

AlexWaygood commented Jan 16, 2025

carljm commented Jan 16, 2025

carljm commented Jan 16, 2025

AlexWaygood commented Jan 16, 2025

carljm commented Jan 16, 2025

carljm commented Jan 16, 2025 • edited Loading

sharkdp commented Jan 16, 2025

AlexWaygood commented Jan 16, 2025

carljm commented Jan 16, 2025

MichaReiser commented Jan 16, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood Jan 17, 2025 • edited Loading

Choose a reason for hiding this comment

AlexWaygood Jan 17, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood Jan 17, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood Jan 17, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood commented Jan 17, 2025

carljm left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexWaygood commented Jan 15, 2025 •

edited

Loading

Why not just implement `Ord` on `Type`?

github-actions bot commented Jan 15, 2025 •

edited

Loading

`ruff-ecosystem` results

AlexWaygood commented Jan 15, 2025 •

edited

Loading

MichaReiser Jan 16, 2025 •

edited

Loading

AlexWaygood Jan 16, 2025 •

edited

Loading

MichaReiser left a comment •

edited

Loading

AlexWaygood commented Jan 16, 2025 •

edited

Loading

sharkdp commented Jan 16, 2025 •

edited

Loading

AlexWaygood commented Jan 16, 2025 •

edited

Loading

carljm commented Jan 16, 2025 •

edited

Loading

AlexWaygood Jan 17, 2025 •

edited

Loading

AlexWaygood Jan 17, 2025 •

edited

Loading

AlexWaygood Jan 17, 2025 •

edited

Loading

AlexWaygood Jan 17, 2025 •

edited

Loading