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] fix equivalence (and gradual equivalence) for differently-ordered unions and intersections #15380

Open
carljm opened this issue Jan 9, 2025 · 1 comment
Labels
red-knot Multi-file analysis & type inference

Comments

@carljm
Copy link
Contributor

carljm commented Jan 9, 2025

This issue relates to the TODO comment here:

/// Return true if this type is [equivalent to] type `other`.
///
/// This method returns `false` if either `self` or `other` is not fully static.
///
/// [equivalent to]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent
pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool {
if !(self.is_fully_static(db) && other.is_fully_static(db)) {
return false;
}
// TODO equivalent but not identical structural types, differently-ordered unions and
// intersections, other cases?
// For all other cases, types are equivalent iff they have the same internal
// representation.
self == other
}

Some ~raw comments from discussion about this issue:


it's not simple, but it also shouldn't be worse than the existing is_subtype_of support for intersections and unions, I think; it just feels wrong that it's O(n^2)
i mean the simplest (but maybe not most efficient) implementation of it would be "is A a subtype of B and B a subtype of A"
if so, they are equivalent

Alex Waygood — Today at 10:01 AM

except that is_subtype_of() calls is_equivalent_to() 😆
so you'll get infinite recursion with our current structure

carljm — Today at 10:01 AM

true, we may need to split atomic equivalence
because we do maintain a simplified two-layer structure for unions and intersections
we don't have arbitrary recursive structures
so we should know when handling union/intersection subtyping when we won't be dealing with more unions/intersections

Alex Waygood — Today at 10:02 AM

I do also think that we can implement optimisations by making sure that equivalent types have the same internal representation wherever possible, like the thing I implemented the other day so that type[object] is eagerly simplified to type

@carljm carljm added the red-knot Multi-file analysis & type inference label Jan 9, 2025
@carljm carljm added this to the Red Knot Q1 2025 milestone Jan 9, 2025
@carljm
Copy link
Contributor Author

carljm commented Jan 9, 2025

In our 1:1 just now @sharkdp raised the possibility that we could do a more efficient version of this based on consistently ordering unions and intersections according to "equivalence classes" of types (so that for example Any and Unknown would always be ordered adjacent to each other).

This would require that we track "user-facing" order (i.e. to preserve the user-provided order) separately, or just decide that we're doing enough type simplification that tracking this user-facing order actually doesn't matter.

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

No branches or pull requests

1 participant