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.

Sign up for GitHub

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

Glossary: Clarify which types don't participate in subtyping #1907

Merged
merged 2 commits into from
Feb 10, 2025
Merged

Glossary: Clarify which types don't participate in subtyping #1907

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0f20821
Glossary: Improve gradual form and gradual type definitions
Jan 12, 2025
1112fd5
Glossary: Restore the original order of notes on not fully static gra…
Feb 8, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions docs/spec/glossary.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 <: Any
  • tuple[S, ...] <: tuple[T, ...] if S <: T
  • Callable[..., S] <: Callable[T, ...] if S <: T

Copy link
Author

@bswck bswck Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

@carljm carljm Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

@carljm carljm Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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".

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, materialization is necessary either way in order to define assignability for gradual types.

in the :term:`subtype` relation, but they do participate in
:term:`consistency <consistent>` and :term:`assignability <assignable>`.
They can be :term:`materialized <materialize>` to a more static, or fully static,
type. See :ref:`type-system-concepts`.

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
:term:`subtype` relation, but they do participate in :term:`consistency
<consistent>` and :term:`assignability <assignable>`. They can be
:term:`materialized <materialize>` to a more static, or fully static,
type. See :ref:`type-system-concepts`.
possible runtime values).

inline
Inline type annotations are annotations that are included in the
Expand Down
Loading