Glossary: Improve gradual form and gradual type definitions #1907
Conversation
| @@ -65,19 +65,19 @@ This section defines a few terms that may be used elsewhere in the specification | |||
| primary gradual form is :ref:`Any`. The ellipsis (``...``) is a gradual | |||
| form in some, but not all, contexts. It is a gradual form when used in a | |||
| :ref:`Callable` type, and when used in ``tuple[Any, ...]`` (but not in | |||
| other :ref:`tuple <tuples>` types). | |||
| other :ref:`tuple <tuples>` types). Types that contain gradual forms do not participate | |||
There was a problem hiding this comment.
This doesn't look right to me. Gradual forms must also participate in subtyping, because otherwise we will not be able to decide subtyping whenever we encounter a gradual form. Also, there is a natural way to define subtyping for them:
Any <: Anytuple[S, ...]<:tuple[T, ...]ifS <: TCallable[..., S]<:Callable[T, ...]ifS <: T
There was a problem hiding this comment.
AFAIK, no—gradual forms do not participate in subtyping, and what you've shown is decided by materialization and consistency (or by consistent subtyping, which is not the subtype relation referenced here) that span all types in the Python type system.
There was a problem hiding this comment.
Huh, interesting! So what should type checkers do when they need to use the subtyping relation and one of the types is gradual? E.g. union normalization where the union is Any | Any | T.
There was a problem hiding this comment.
Non-fully-static types participate in assignability, but not in subtyping.
Allowing them to participate in subtyping is a problem because it would make subtyping non-transitive.
A union of Any | T does not simplify, it represents an unknown type with lower bound T (that is, the union of "an unknown set of objects" and "inhabitants of T" is some unknown set of objects at least as large as T, possibly larger.)
Any | Any can simplify to Any, because there is a gradual equivalence relation (defined as "both types have exactly the same possible materializations") under which Any is equivalent to Any, and this equivalence can be used in simplifying unions. (Intuitively: the union of two unknown sets of objects is... an unknown set of objects.)
This is discussed in the spec at https://typing.readthedocs.io/en/latest/spec/concepts.html#union-types, and the gradual equivalence relation is mentioned at https://typing.readthedocs.io/en/latest/spec/concepts.html#summary-of-type-relations
There was a problem hiding this comment.
Thanks, Carl. Can you elaborate why including these forms into subtyping in the way I described above breaks transitivity?
It looks like you get the same behavior via "both types have exactly the same possible materializations", so I assume directly saying that Any <: Any shouldn't break anything?
There was a problem hiding this comment.
@superbobry Oh, sorry, I mis-interpreted your comment as suggesting a broader interpretation of subtyping for non-fully-static types than you were actually suggesting.
No, I don't think there would be any harm (or non-transitivity) in saying Any <: Any. I'm recalling now that I think we had this same discussion on the original PR that added the "core concepts" section of the typing spec, though that PR had so much discussion that I can no longer find the thread!
I think my conclusion in that discussion (and still my feeling today) is that the way the spec defines this is simpler. Assuming we want to also be able to simplify e.g. tuple[Any, Any] | tuple[Any, Any] to just tuple[Any, Any], it would not be sufficient to only say Any <: Any; we would still need a materialization-based definition of gradual type equivalence. At that point it seems clearer to rely solely on gradual type equivalence, and not have a special-case for a few specific non-static types to participate in subtyping.
EDIT: This last paragraph is not right; we could say tuple[Any, Any] <: tuple[Any, Any] solely on the basis of Any <: Any, without having to introduce any subtype relation between e.g. tuple[int, int] and tuple[Any, Any]. So I think you are right that Any <: Any could replace the concept of gradual equivalence, without changing behavior? But I'm still not convinced that would be overall simpler.
There was a problem hiding this comment.
Is the concept of "materialization" necessary if we define subtyping for gradual forms directly? If yes, it might be "simpler" in a sense that we can avoid introducing "materialization".
There was a problem hiding this comment.
Yes, materialization is necessary either way in order to define assignability for gradual types.
|
|
||
| gradual type | ||
| All types in the Python type system are "gradual". A gradual type may be | ||
| a :term:`fully static type`, or it may be :ref:`Any`, or a type that | ||
| contains ``Any`` or another :term:`gradual form`. A gradual type does not | ||
| necessarily represent a single set of possible runtime values; instead it | ||
| can represent a set of possible static types (a set of possible sets of | ||
| possible runtime values). Gradual types do not participate in the |
There was a problem hiding this comment.
I would prefer to clarify here, by simply saying "Gradual types which are not fully static do not participate...", rather than moving this discussion into the "gradual form" glossary entry. It feels out of scope for the "gradual form" entry, which is about the forms that make a type non-fully-static, not about the behavior of the resulting types.
There was a problem hiding this comment.
Makes sense. Thanks for suggesting this approach.
The existing definition of gradual types implies that no type in the Python type system participates in the subtype relation.
I moved the fragment that introduced the contradiction to the definition of gradual forms, as that is likely a better place for it (facts about types that contain gradual forms aren't inherently about gradual types as a whole).