[ty] Perform assignability etc checks using new Constraints trait
#19838
Conversation
Diagnostic diff on typing conformance testsNo changes detected when running ty on typing conformance tests ✅ |
|
CodSpeed WallTime Performance ReportMerging #19838 will not alter performanceComparing Summary
|
dcreager
force-pushed
the
dcreager/relation-with-constraints
branch
2 times, most recently
from
53077f3 to
efabd55
Compare
dcreager
force-pushed
the
dcreager/relation-with-constraints
branch
from
efabd55 to
737c8e9
Compare
dcreager
force-pushed
the
dcreager/relation-with-constraints
branch
from
737c8e9 to
1e5c45d
Compare
dcreager
changed the title
Constraints traitConstraints trait
carljm
left a comment
carljm
left a comment
There was a problem hiding this comment.
This is quite cool! Very impressed with how you wrangled the Rust API to make the translation fairly mechanical in many cases, even though you're adding significant capability.
| // not false). Once we're using real constraint sets instead of bool, we should be | ||
| // able to simplify the typevar logic. |
There was a problem hiding this comment.
I'm curious how you think the logic can be simplified "once we're using real constraint sets"? To me it appears kind of the opposite -- this duplication is here precisely because we are trying to be correct in a future with real constraint sets, where we need to return the actual accumulated constraints from the inner has_relation_to_impl checks. In this PR, with just bool, we can pass all tests without this duplication, by just changing the sense of the match arm if clause back to a positive .is_always(db) instead of a negated .is_never(db), and making the body of the match arm be C::always(db).
There was a problem hiding this comment.
Considering this case is actually making me wonder about a more fundamental thing: what about a case where this match arm returns some constraints (neither always nor never), but some later match arm would also have returned some constraints, had we reached it? In an ideal world, wouldn't we OR those constraint sets, if we're trying to express the conditions under which the relation would be true?
I guess in the real world, we just pick one of them and don't find all solutions?
There was a problem hiding this comment.
My thinking is not that the stuff inside the match arm would change all that much. The part that I find too complex in its current state is that so much depends on the order of the match arms. My hunch is that the fall-through here won't be needed, and the ordering will no longer matter as much, because we'll be able to better combine the results of each recursive call with the other surrounding constraints.
| /// Encodes the constraints under which a type property (e.g. assignability) holds. | ||
| pub(crate) trait Constraints<'db>: Clone + Sized { | ||
| /// Returns a constraint set that never holds | ||
| fn never(db: &'db dyn Db) -> Self; |
There was a problem hiding this comment.
There's the obvious name tension with Type::Never here, but I'm not sure I have a better name to offer.
There was a problem hiding this comment.
unsatisfiable or never_satisfiable, but that's longer to type 😄
There was a problem hiding this comment.
unsatisfiableornever_satisfiable, but that's longer to type 😄
I sort-of prefer those, actually! unsatisfiable doesn't seem too verbose to me. Not a big deal though.
There was a problem hiding this comment.
No problem, it's just a couple of sed commands to make the change!
For the predicates, I've gone with is_{always,never}_satisfied. For the constructors, I want them to be consistent, so I went with unsatisfied/always_satisfied.
* main: (29 commits) [ty] add docstrings to completions based on type (#20008) [`pyupgrade`] Avoid reporting `__future__` features as unnecessary when they are used (`UP010`) (#19769) [`flake8-use-pathlib`] Add fixes for `PTH102` and `PTH103` (#19514) [ty] correctly ignore field specifiers when not specified (#20002) `Option::unwrap` is now const (#20007) [ty] Re-arrange "list modules" implementation for Salsa caching [ty] Test "list modules" versus "resolve module" in every mdtest [ty] Wire up "list modules" API to make module completions work [ty] Tweak some completion tests [ty] Add "list modules" implementation [ty] Lightly expose `FileModule` and `NamespacePackage` fields [ty] Add some more helper routines to `ModulePath` [ty] Fix a bug when converting `ModulePath` to `ModuleName` [ty] Split out another constructor for `ModuleName` [ty] Add stub-file tests to existing module resolver [ty] Expose some routines in the module resolver [ty] Add more path helper functions [`flake8-annotations`] Remove unused import in example (`ANN401`) (#20000) [ty] distinguish base conda from child conda (#19990) [ty] Fix server hang (#19991) ...
Co-authored-by: Carl Meyer <[email protected]>
Co-authored-by: Alex Waygood <[email protected]>
Co-authored-by: Alex Waygood <[email protected]>
This PR adds an implementation of constraint sets.
An individual constraint restricts the specialization of a single
typevar to be within a particular lower and upper bound: the typevar can
only specialize to types that are a supertype of the lower bound, and a
subtype of the upper bound. (Note that lower and upper bounds are fully
static; we take the bottom and top materializations of the bounds to
remove any gradual forms if needed.) Either bound can be “closed” (where
the bound is a valid specialization), or “open” (where it is not).
You can then build up more complex constraint sets using union,
intersection, and negation operations. We use a disjunctive normal form
(DNF) representation, just like we do for types: a _constraint set_ is
the union of zero or more _clauses_, each of which is the intersection
of zero or more individual constraints. Note that the constraint set
that contains no clauses is never satisfiable (`⋃ {} = 0`); and the
constraint set that contains a single clause, which contains no
constraints, is always satisfiable (`⋃ {⋂ {}} = 1`).
One thing to note is that this PR does not change the logic of the
actual assignability checks, and in particular, we still aren't ever
trying to create an "individual constraint" that constrains a typevar.
Technically we're still operating only on `bool`s, since we only ever
instantiate `C::always_satisfiable` (i.e., `true`) and
`C::unsatisfiable` (i.e., `false`) in the `has_relation_to` methods. So
if you thought that #19838 introduced an unnecessarily complex stand-in
for `bool`, well here you go, this one is worse! (But still seemingly
not yielding a performance regression!) The next PR in this series,
#20093, is where we will actually create some non-trivial constraint
sets and use them in anger.
That said, the PR does go ahead and update the assignability checks to
use the new `ConstraintSet` type instead of `bool`. That part is fairly
straightforward since we had already updated the assignability checks to
use the `Constraints` trait; we just have to actively choose a different
impl type. (For the `is_whatever` variants, which still return a `bool`,
we have to convert the constraint set, but the explicit
`is_always_satisfiable` calls serve as nice documentation of our
intent.)
---------
Co-authored-by: Alex Waygood <[email protected]>
Co-authored-by: Carl Meyer <[email protected]>
…stral-sh#19838) "Why would you do this? This looks like you just replaced `bool` with an overly complex trait" Yes that's correct! This should be a no-op refactoring. It replaces all of the logic in our assignability, subtyping, equivalence, and disjointness methods to work over an arbitrary `Constraints` trait instead of only working on `bool`. The methods that `Constraints` provides looks very much like what we get from `bool`. But soon we will add a new impl of this trait, and some new methods, that let us express "fuzzy" constraints that aren't always true or false. (In particular, a constraint will express the upper and lower bounds of the allowed specializations of a typevar.) Even once we have that, most of the operations that we perform on constraint sets will be the usual boolean operations, just on sets. (`false` becomes empty/never; `true` becomes universe/always; `or` becomes union; `and` becomes intersection; `not` becomes negation.) So it's helpful to have this separate PR to refactor how we invoke those operations without introducing the new functionality yet. Note that we also have translations of `Option::is_some_and` and `is_none_or`, and of `Iterator::any` and `all`, and that the `and`, `or`, `when_any`, and `when_all` methods are meant to short-circuit, just like the corresponding boolean operations. For constraint sets, that depends on being able to implement the `is_always` and `is_never` trait methods. --------- Co-authored-by: Carl Meyer <[email protected]> Co-authored-by: Alex Waygood <[email protected]>
This PR adds an implementation of constraint sets.
An individual constraint restricts the specialization of a single
typevar to be within a particular lower and upper bound: the typevar can
only specialize to types that are a supertype of the lower bound, and a
subtype of the upper bound. (Note that lower and upper bounds are fully
static; we take the bottom and top materializations of the bounds to
remove any gradual forms if needed.) Either bound can be “closed” (where
the bound is a valid specialization), or “open” (where it is not).
You can then build up more complex constraint sets using union,
intersection, and negation operations. We use a disjunctive normal form
(DNF) representation, just like we do for types: a _constraint set_ is
the union of zero or more _clauses_, each of which is the intersection
of zero or more individual constraints. Note that the constraint set
that contains no clauses is never satisfiable (`⋃ {} = 0`); and the
constraint set that contains a single clause, which contains no
constraints, is always satisfiable (`⋃ {⋂ {}} = 1`).
One thing to note is that this PR does not change the logic of the
actual assignability checks, and in particular, we still aren't ever
trying to create an "individual constraint" that constrains a typevar.
Technically we're still operating only on `bool`s, since we only ever
instantiate `C::always_satisfiable` (i.e., `true`) and
`C::unsatisfiable` (i.e., `false`) in the `has_relation_to` methods. So
if you thought that astral-sh#19838 introduced an unnecessarily complex stand-in
for `bool`, well here you go, this one is worse! (But still seemingly
not yielding a performance regression!) The next PR in this series,
astral-sh#20093, is where we will actually create some non-trivial constraint
sets and use them in anger.
That said, the PR does go ahead and update the assignability checks to
use the new `ConstraintSet` type instead of `bool`. That part is fairly
straightforward since we had already updated the assignability checks to
use the `Constraints` trait; we just have to actively choose a different
impl type. (For the `is_whatever` variants, which still return a `bool`,
we have to convert the constraint set, but the explicit
`is_always_satisfiable` calls serve as nice documentation of our
intent.)
---------
Co-authored-by: Alex Waygood <[email protected]>
Co-authored-by: Carl Meyer <[email protected]>
3 participants
"Why would you do this? This looks like you just replaced
boolwith an overly complex trait"Yes that's correct!
This should be a no-op refactoring. It replaces all of the logic in our assignability, subtyping, equivalence, and disjointness methods to work over an arbitrary
Constraintstrait instead of only working onbool.The methods that
Constraintsprovides looks very much like what we get frombool. But soon we will add a new impl of this trait, and some new methods, that let us express "fuzzy" constraints that aren't always true or false. (In particular, a constraint will express the upper and lower bounds of the allowed specializations of a typevar.)Even once we have that, most of the operations that we perform on constraint sets will be the usual boolean operations, just on sets. (
falsebecomes empty/never;truebecomes universe/always;orbecomes union;andbecomes intersection;notbecomes negation.) So it's helpful to have this separate PR to refactor how we invoke those operations without introducing the new functionality yet.Note that we also have translations of
Option::is_some_andandis_none_or, and ofIterator::anyandall, and that theand,or,when_any, andwhen_allmethods are meant to short-circuit, just like the corresponding boolean operations. For constraint sets, that depends on being able to implement theis_alwaysandis_nevertrait methods.