Skip to content

Typing concepts: add that object | Any and Never | Any can be simplified #2052

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

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
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
14 changes: 10 additions & 4 deletions docs/spec/concepts.rst
Original file line number Diff line number Diff line change
Expand Up @@ -298,9 +298,9 @@ visualize this analogy in the following table:
* - ``B`` is :term:`equivalent` to ``A``
- ``B`` is :term:`consistent` with ``A``

We can also define an **equivalence** relation on gradual types: the gradual
types ``A`` and ``B`` are equivalent (that is, the same gradual type, not
merely consistent with one another) if and only if all materializations of
We can also define an **equivalence** relation on gradual types: the gradual
types ``A`` and ``B`` are equivalent (that is, the same gradual type, not
merely consistent with one another) if and only if all materializations of
``A`` are also materializations of ``B``, and all materializations of ``B``
are also materializations of ``A``.

Expand Down Expand Up @@ -368,10 +368,16 @@ can likewise be materialized to ``T1 | T2``. Thus, the gradual types ``S1`` and

If ``B`` is a subtype of ``A``, ``B | A`` is equivalent to ``A``.

This rule applies only to subtypes, not assignable-to. The union ``T | Any`` is
This rule applies only to subtypes, not assignable-to. For any type ``T``
(other than the top and bottom types ``object`` and ``Never``), the union ``T | Any`` is
not reducible to a simpler form. It represents an unknown static type with
lower bound ``T``. That is, it represents an unknown set of objects which may
be as large as ``object``, or as small as ``T``, but no smaller.
The exceptions are ``object`` and ``Never``. The union ``object | Any`` is equivalent to
``object``, because ``object`` is a type containing all values and therefore the ``Any``
cannot add any values. Similarly, ``Never | Any`` is equivalent to ``Any``, because
``Never`` is a type containing no values, so that including it in a union cannot add any
values to the type.
Comment on lines +376 to +380
Copy link

@sharkdp sharkdp Jul 21, 2025

Choose a reason for hiding this comment

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

There is another exception explained in the paragraph below (for equivalent gradual types). To be honest, I'm not sure if it really helps with clarity to add more exceptions here. It feels to me like the original intent of this paragraph was maybe just to explain that T | Any is not generally reducible to a simpler form (Any)?

Also, the existing sentence "It represents an unknown static type with lower bound T" is only true if T is fully-static.

Maybe both of these problems could be solved by going with something like:

This rule applies only to subtypes, not assignable-to. The union T | Any is not generally reducible to a simpler form. For example, int | Any represents an unknown static type with lower bound int. That is, it represents an unknown set of objects which may be as large as object, or as small as int, but no smaller.

Equivalent gradual types can, however, be simplified from unions […]

Comment on lines +378 to +380
Copy link

@jorenham jorenham Jul 21, 2025

Choose a reason for hiding this comment

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

Never | Any ≅ Any can be generalized into Never | T ≅ T (for all types T), but I'm not sure if that axiom is already in the spec.


Equivalent gradual types can, however, be simplified from unions; e.g.
``list[Any] | list[Any]`` is equivalent to ``list[Any]``. Similarly, the union
Expand Down