review feedback

docs/spec/concepts.rst

@@ -18,16 +18,16 @@ running a program. Instead, it will check the types of values before performing
 operations on them at runtime. This is not to say that the language is
 "untyped". Values at runtime have a type and their uses obey typing rules. Not
 every operation will be checked, but certain primitive operations in the
-language such as attribute access or arithmetic will be.  Python was
+language such as attribute access or arithmetic will be. Python was
 historically a dynamically-typed language.
 
 **Gradual typing** is the name for a specific way to combine static and dynamic
-typing.  It allows mixing static and dynamic checking at a fine level of
-granularity.  For instance, in Python, individual variables, parameters, and
-return values can be either statically or dynamically typed.  Data structures
-such as objects can have a mix of static and dynamic checking.  As an example,
-a Python dictionary could choose to have static checking of the key type but
-dynamic checking of the value type.
+typing. It allows mixing static and dynamic checking at a fine level of
+granularity. For instance, in type-annotated Python, individual variables,
+parameters, and returns can optionally be given a static type. Data structures
+such as objects can have a mix of static and dynamic-only checking. As an
+example, a Python dictionary could be annotated to have static checking of the
+key type but only dynamic checking of the value type.
 
 In gradual typing, a dynamically typed value is indicated by a special
 "unknown" or "dynamic" type.  In Python, the unknown type is spelled
@@ -43,9 +43,9 @@ Static, dynamic, and gradual types
 ----------------------------------
 
 We will refer to types that do not contain :ref:`Any` as a sub-part as **static
-types**. The dynamic type :ref:`Any` is the **dynamic type**. Any type other
-than :ref:`Any` that does contain :ref:`Any` as a sub-part is a **gradual
-type**.
+types**. :ref:`Any` itself is the **dynamic type**. A **gradual type** can be a
+static type, :ref:`Any` itself, or a type that contains :ref:`Any` as a
+sub-part.
 
 Static types
 ~~~~~~~~~~~~
@@ -86,58 +86,65 @@ language.
 The subtype relation
 --------------------
 
-A static type ``B`` is a **subtype** of another static type ``A`` if (and only
-if) the set of values represented by ``B`` is a subset of the set of values
+A static type ``B`` is a **subtype** of another static type ``A`` if and only
+if the set of values represented by ``B`` is a subset of the set of values
 represented by ``A``. Because the subset relation on sets is transitive and
-reflexive, the subtype relation is also transitive (if ``A`` is a subtype of
-``B`` and ``B`` is a subtype of ``C``, then ``A`` is a subtype of ``C``) and
+reflexive, the subtype relation is also transitive (if ``C`` is a subtype of
+``B`` and ``B`` is a subtype of ``A``, then ``C`` is a subtype of ``A``) and
 reflexive (``A`` is always a subtype of ``A``).
 
 The **supertype** relation is the inverse of subtype: ``A`` is a supertype of
-``B`` if (and only if) ``B`` is a subtype of ``A``; or equivalently, if (and
-only if) the set of values represented by ``A`` is a superset of the values
+``B`` if and only if ``B`` is a subtype of ``A``; or equivalently, if and only
+if the set of values represented by ``A`` is a superset of the values
 represented by ``B``. The supertype relation is also transitive and reflexive.
 
 We also define an **equivalence** relation on static types: the types ``A`` and
-``B`` are equivalent (or "the same type") if (and only if) ``A`` is a subtype
+``B`` are equivalent (or "the same type") if and only if ``A`` is a subtype
 of ``B`` and ``B`` is a subtype of ``A``. This means that the set of values
 represented by ``A`` is both a superset and a subset of the values represented
 by ``B``, meaning ``A`` and ``B`` must represent the same set of values.
 
-We may describe a type ``B`` as "narrower" than a type ``A`` if ``B`` is a
-subtype of ``A`` and ``B`` is not equivalent to ``A``.
+We may describe a type ``B`` as "narrower" than a type ``A`` (or as a "strict
+subtype" of ``A``) if ``B`` is a subtype of ``A`` and ``B`` is not equivalent
+to ``A``.
 
 The consistency relation
 ------------------------
 
-Since :ref:`Any` (the dynamic type) represents an unknown static type, it does
-not represent any known single set of values, and thus it is not in the domain
-of the subtype, supertype, or equivalence relations on static types described
-above.
+Since :ref:`Any` represents an unknown static type, it does not represent any
+known single set of values, and thus it is not in the domain of the subtype,
+supertype, or equivalence relations on static types described above.
 
-We define a **materialization** relation from gradual types to gradual and
-static types as follows: if replacing one or more occurrences of ``Any`` in
-gradual type ``A`` with some gradual or static type results in the gradual or
-static type ``B``, then ``B`` is a materialization of ``A``. For instance,
+We define a **materialization** relation on gradual types as follows: if
+replacing zero or more occurrences of ``Any`` in gradual type ``A`` with some
+gradual type (which can be different for each occurrence of ``Any``) results in
+the gradual type ``B``, then ``B`` is a materialization of ``A``. For instance,
 ``tuple[int, str]`` (a static type) and ``tuple[Any, str]`` (a gradual type)
-are both materializations of ``tuple[Any, Any]``. If ``B`` is a materialization
-of ``A``, we can say that ``B`` is a more precise type than ``A``.
+are both materializations of ``tuple[Any, Any]``.
 
-We define a **consistency** relation over all types (the dynamic type, gradual
-types, and static types.)
+If ``B`` is a materialization of ``A``, we can say that ``B`` is a "more
+static" type than ``A``, and ``A`` is a "more dynamic" type than ``B``.
 
-A static type ``A`` is consistent with another static type ``B`` only if they
-are the same type (``A`` is equivalent to ``B``.)
+The materialization relation is both transitive and reflexive, so it defines a
+preorder on gradual types.
 
-The dynamic type ``Any`` is consistent with every type, and every type is
-consistent with ``Any``.
+We also define a **consistency** relation on gradual types.
+
+A static type ``A`` is consistent with another static type ``B`` if and only if
+they are the same type (``A`` is equivalent to ``B``.)
 
-A gradual type ``C`` is consistent with a gradual or static type ``D``, and
-``D`` is consistent with ``C``, if ``D`` is a materialization of ``C``.
+A gradual type ``A`` is consistent with a gradual type ``B``, and ``B`` is
+consistent with ``A``, if and only if ``B`` is a materialization of ``A`` or
+``A`` is a materialization of ``B``.
+
+The dynamic type ``Any`` is consistent with every type, and every type is
+consistent with ``Any``. (This must follow from the above definitions of
+materialization and consistency, but is worth stating explicitly.)
 
-The consistency relation is not transitive. ``tuple[int, int]`` and
-``tuple[str, int]`` are both consistent with ``tuple[Any, int]]``, but
-``tuple[str, int]`` is not consistent with ``tuple[int, int]``.
+The consistency relation is not transitive. ``tuple[int, int]`` is consistent
+with ``tuple[Any, int]`` and ``tuple[Any, int]`` is consistent with
+``tuple[str, int]``, but ``tuple[int, int]`` is not consistent with
+``tuple[str, int]``.
 
 The consistency relation is symmetric. If ``A`` is consistent with ``B``, ``B``
 is also consistent with ``A``. It is also reflexive: ``A`` is always consistent
@@ -146,7 +153,7 @@ with ``A``.
 The consistent subtype relation
 -------------------------------
 
-Given the consistency relation and the subtyping relation, we define the
+Given the materialization relation and the subtyping relation, we define the
 **consistent subtype** relation over all types. A type ``A`` is a consistent
 subtype of a type ``B`` if there exists a materialization ``A'`` of ``A`` and a
 materialization ``B'`` of ``B``, where ``A'`` and ``B'`` are both static types,
@@ -160,8 +167,8 @@ Consistent subtyping defines assignability
 ------------------------------------------
 
 Consistent subtyping defines "assignability" for Python.  An expression can be
-assigned to a variable (including passed as a parameter, and also returned from
-a function) if it is a consistent subtype of the variable's type annotation
+assigned to a variable (including passed as a parameter or returned from a
+function) if it is a consistent subtype of the variable's type annotation
 (respectively, parameter's type annotation or return type annotation).
 
 We can say that a type ``A`` is "assignable to" a type ``B`` if ``A`` is a
@@ -171,6 +178,6 @@ References
 ----------
 
 The concepts presented here are derived from the research literature in gradual
-typing. See::
+typing. See e.g.:
 
-* `Victor Lanvin. A semantic foundation for gradual set-theoretic types. Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222 <https://theses.hal.science/tel-03853222/file/va_Lanvin_Victor.pdf>`_
+* `Victor Lanvin. A semantic foundation for gradual set-theoretic types. <https://theses.hal.science/tel-03853222/file/va_Lanvin_Victor.pdf>`_ Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222