diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index a119c8d0..c13321b6 100644 --- a/docs/spec/concepts.rst +++ b/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 `_ +* `Victor Lanvin. A semantic foundation for gradual set-theoretic types. `_ Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222