diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index ee230f23..d2d0353c 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -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``. @@ -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. Equivalent gradual types can, however, be simplified from unions; e.g. ``list[Any] | list[Any]`` is equivalent to ``list[Any]``. Similarly, the union