Typing conformance results

No changes detected ✅

Memory usage report

Summary

Significant changes

ecosystem-analyzer results

No diagnostic changes detected ✅

Full report with detailed diff (timing results)

What Divergent should actually be is a delicate issue. My comment is not intended to block this PR, but I would like to discuss Divergent and give a proper definition. As I will explain below, I believe that Divergent cannot be fully contained within the specifications of Python's type system and should be defined as an extension.

When I first introduced Divergent (#20312), I thought it would suffice to treat it simply as a type of dynamic type, like Any. This would be the simplest definition of Divergent. However, as already shown, the fact that Divergent is replaced by a fully-static type by materialization causes problems. So it seems that Divergent cannot be considered a simple dynamic type.

However, in this PR, Divergent becomes a type with an unclear origin. It is not a dynamic type, but it is neither Never nor object. In terms of operational rules, it is a type that "allows many operations and propagates itself to the results". Such a type clearly deviates from the specifications of Python's type system.

Theoretically, it would make the most sense to reinterpret Divergent as a recursive variable of a recursive type. In other words, it's equivalent to $X$ in $\mu X. tuple[X | int]$, for example. However, recursive types do not exist in Python's type system. Also, this direction would require quite a major change.

@mtshiba I think it has never been the case (even from the first PR) that Divergent could really be considered a "simple dynamic type". It has always had this "disappears in unions" behavior, which is more like the behavior of Never. In fact Never is the type-theoretically correct place to start a fixpoint iteration, and Divergent originally replaced Never in this role, so in some ways it could be considered that it should be more "like Never" than "a simple dynamic type".

Perhaps ideally Divergent would just be an "is recursively defined as part of query X" marker that could be set on any type, orthogonal to the type itself, and would propagate through uses of that type. That is, it would be outside the type system entirely, but would allow us to avoid infinitely expanding types.

Theoretically, it would make the most sense to reinterpret Divergent as a recursive variable of a recursive type. In other words, it's equivalent to $X$ in $μX. tuple[X | int]$ , for example. However, recursive types do not exist in Python's type system.

I would say that recursive types do exist in Python's type system, given that the type spec and conformance suite require support for recursive type aliases. The question of how to represent them is not specified, however. We've discussed using a de Bruijn index representation to allow transformations of recursive types to not fall back to Any (as they currently do). I'm not sure if such a representation can work for fixpoint iteration of Salsa queries in general, though.

@mtshiba I think it has never been the case (even from the first PR) that Divergent could really be considered a "simple dynamic type". It has always had this "disappears in unions" behavior, which is more like the behavior of Never. In fact Never is the type-theoretically correct place to start a fixpoint iteration, and Divergent originally replaced Never in this role, so in some ways it could be considered that it should be more "like Never" than "a simple dynamic type".

@carljm What makes Divergent special is that it has its own normalization rules in cycle recovery. This does not characterize subtyping/assignability behavior. (Divergent | T).cycle_normalized() = T does not mean Divergent | T = T. Therefore, more precisely, Divergent behaves like Never in cycle recovery and like Any in normal type inference.
(However, IntersectionBuilder mistakenly sets a special rule for the Divergent type, Divergent & T = Divergent, which should not be reduced in normal type inference)

You might then wonder why the behavior of Divergent in normal type inference wasn't aligned with Never. There's an important difference between Divergent and Never. Types containing Divergent are not necessarily empty types. However, since we had no way to accurately represent the instances, I substituted it with dynamic types.

Perhaps ideally Divergent would just be an "is recursively defined as part of query X" marker that could be set on any type, orthogonal to the type itself, and would propagate through uses of that type. That is, it would be outside the type system entirely, but would allow us to avoid infinitely expanding types.

I now find it more appealing to reinterpret Divergent as part of a recursive type ($\mu$-types) than to interpret it as something like Any/Never, because $\mu$-types can literally represent infinite cycles.

Currently, we only have the Divergent type, which is the marker representing the recursive part, but formally, a recursive type should consist of a marker and a binder that encloses the entire type. Something like Type::Recursive(id, tuple[Divergent(id), int]). If we try to get the type of the 0th element of the tuple, this will also be Type::Recursive(id, tuple[Divergent(id), int]), but if we try to get the type of the 1st element, it will be int.

Is this the same as what you have in mind?

I would say that recursive types do exist in Python's type system, given that the type spec and conformance suite require support for recursive type aliases. The question of how to represent them is not specified, however. We've discussed using a de Bruijn index representation to allow transformations of recursive types to not fall back to Any (as they currently do). I'm not sure if such a representation can work for fixpoint iteration of Salsa queries in general, though.

Whether the recursive types mentioned here can be interpreted as recursive type aliases is debatable, as they are synthesized during type inference and are not "aliases" of anything. However, this kind of internal extension is present in ty, with examples like SynthesizedProtocol types, so perhaps there's no need to hesitate.

I would like to create a PoC to replace Divergent with the recursive type system.