-
Notifications
You must be signed in to change notification settings - Fork 1.7k
[ty] introduce DivergentType
#20312
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
[ty] introduce DivergentType
#20312
Conversation
Diagnostic diff on typing conformance testsNo changes detected when running ty on typing conformance tests ✅ |
|
carljm
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good, thank you! I put together a proof-of-concept to show how we can use this type to address an infinite-tuple case in implicit instance attribute (given a small change in Salsa) -- that's enough to convince me that this will be generally useful.
## Summary Derived from #17371 Fixes astral-sh/ty#256 Fixes astral-sh/ty#1415 Fixes astral-sh/ty#1433 Fixes astral-sh/ty#1524 Properly handles any kind of recursive inference and prevents panics. --- Let me explain techniques for converging fixed-point iterations during recursive type inference. There are two types of type inference that naively don't converge (causing salsa to panic): divergent type inference and oscillating type inference. ### Divergent type inference Divergent type inference occurs when eagerly expanding a recursive type. A typical example is this: ```python class C: def f(self, other: "C"): self.x = (other.x, 1) reveal_type(C().x) # revealed: Unknown | tuple[Unknown | tuple[Unknown | tuple[..., Literal[1]], Literal[1]], Literal[1]] ``` To solve this problem, we have already introduced `Divergent` types (#20312). `Divergent` types are treated as a kind of dynamic type [^1]. ```python Unknown | tuple[Unknown | tuple[Unknown | tuple[..., Literal[1]], Literal[1]], Literal[1]] => Unknown | tuple[Divergent, Literal[1]] ``` When a query function that returns a type enters a cycle, it sets `Divergent` as the cycle initial value (instead of `Never`). Then, in the cycle recovery function, it reduces the nesting of types containing `Divergent` to converge. ```python 0th: Divergent 1st: Unknown | tuple[Divergent, Literal[1]] 2nd: Unknown | tuple[Unknown | tuple[Divergent, Literal[1]], Literal[1]] => Unknown | tuple[Divergent, Literal[1]] ``` Each cycle recovery function for each query should operate only on the `Divergent` type originating from that query. For this reason, while `Divergent` appears the same as `Any` to the user, it internally carries some information: the location where the cycle occurred. Previously, we roughly identified this by having the scope where the cycle occurred, but with the update to salsa, functions that create cycle initial values can now receive a `salsa::Id` (salsa-rs/salsa#1012). This is an opaque ID that uniquely identifies the cycle head (the query that is the starting point for the fixed-point iteration). `Divergent` now has this `salsa::Id`. ### Oscillating type inference Now, another thing to consider is oscillating type inference. Oscillating type inference arises from the fact that monotonicity is broken. Monotonicity here means that for a query function, if it enters a cycle, the calculation must start from a "bottom value" and progress towards the final result with each cycle. Monotonicity breaks down in type systems that have features like overloading and overriding. ```python class Base: def flip(self) -> "Sub": return Sub() class Sub(Base): def flip(self) -> "Base": return Base() class C: def __init__(self, x: Sub): self.x = x def replace_with(self, other: "C"): self.x = other.x.flip() reveal_type(C(Sub()).x) ``` Naive fixed-point iteration results in `Divergent -> Sub -> Base -> Sub -> ...`, which oscillates forever without diverging or converging. To address this, the salsa API has been modified so that the cycle recovery function receives the value of the previous cycle (salsa-rs/salsa#1012). The cycle recovery function returns the union type of the current cycle and the previous cycle. In the above example, the result type for each cycle is `Divergent -> Sub -> Base (= Sub | Base) -> Base`, which converges. The final result of oscillating type inference does not contain `Divergent` because `Divergent` that appears in a union type can be removed, as is clear from the expansion. This simplification is performed at the same time as nesting reduction. ``` T | Divergent = T | (T | (T | ...)) = T ``` [^1]: In theory, it may be possible to strictly treat types containing `Divergent` types as recursive types, but we probably shouldn't go that deep yet. (AFAIK, there are no PEPs that specify how to handle implicitly recursive types that aren't named by type aliases) ## Performance analysis A happy side effect of this PR is that we've observed widespread performance improvements! This is likely due to the removal of the `ITERATIONS_BEFORE_FALLBACK` and max-specialization depth trick (astral-sh/ty#1433, astral-sh/ty#1415), which means we reach a fixed point much sooner. ## Ecosystem analysis The changes look good overall. You may notice changes in the converged values for recursive types, this is because the way recursive types are normalized has been changed. Previously, types containing `Divergent` types were normalized by replacing them with the `Divergent` type itself, but in this PR, types with a nesting level of 2 or more that contain `Divergent` types are normalized by replacing them with a type with a nesting level of 1. This means that information about the non-divergent parts of recursive types is no longer lost. ```python # previous tuple[tuple[Divergent, int], int] => Divergent # now tuple[tuple[Divergent, int], int] => tuple[Divergent, int] ``` The false positive error introduced in this PR occurs in class definitions with self-referential base classes, such as the one below. ```python from typing_extensions import Generic, TypeVar T = TypeVar("T") U = TypeVar("U") class Base2(Generic[T, U]): ... # TODO: no error # error: [unsupported-base] "Unsupported class base with type `<class 'Base2[Sub2, U@Sub2]'> | <class 'Base2[Sub2[Unknown], U@Sub2]'>`" class Sub2(Base2["Sub2", U]): ... ``` This is due to the lack of support for unions of MROs, or because cyclic legacy generic types are not inferred as generic types early in the query cycle. ## Test Plan All samples listed in astral-sh/ty#256 are tested and passed without any panic! ## Acknowledgments Thanks to @MichaReiser for working on bug fixes and improvements to salsa for this PR. @carljm also contributed early on to the discussion of the query convergence mechanism proposed in this PR. --------- Co-authored-by: Carl Meyer <[email protected]>
Summary
From #17371
In #17371,
DivergentTypewas introduced to prevent type inference for recursive functions from diverging and causing panics. This turned out to be useful for other divergent type inferences (#17371 (comment)), so I extracted the introduction part ofDivergentTypeinto this PR so that we can use it without waiting for the merge of #17371.Note that this PR only introduces
DivergentTypeand does not actually address divergent type inference yet. Please refer to https://github.com/astral-sh/ruff/pull/17371/files#diff-20b910c6e20faa962bb1642e111db1cbad8e66ace089bdd966ac9d7f9fa99ff2R542-R622 etc. when implementing handling of divergence suppression using this type.Test Plan