From b323afb5d08e180b3413444a7b3f8655e57b982c Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 08:04:11 -0400 Subject: [PATCH 01/45] initial draft of new concepts section --- docs/spec/concepts.rst | 263 +++++++++++++++++++++++------------- docs/spec/special-types.rst | 110 +++++++++++++-- 2 files changed, 271 insertions(+), 102 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index c6418c8b..a119c8d0 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -3,97 +3,174 @@ Type system concepts ==================== -.. _`union-types`: +Static, dynamic, and gradual typing +----------------------------------- + +A **statically-typed** programming language runs a type-checker before running +a program. The program is required to be well-typed according to the language's +type system. The type system assigns a type to all expressions in the language +and verifies that their uses obey the typing rules. Normally, a program that is +not well-typed (i.e., one that contains a type error) will not run. Java and +C++ are examples of statically-typed object-oriented languages. + +A **dynamically-typed** programming language does not run a type-checker before +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 +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. + +In gradual typing, a dynamically typed value is indicated by a special +"unknown" or "dynamic" type. In Python, the unknown type is spelled +:ref:`Any`. It indicates to the static type checker that this value should not +be subject to static checking. The system should not signal a static type +error for use of an expression with type :ref:`Any`. Instead, the expression's +value will be dynamically checked, according to the Python runtime's usual +checks on the types of runtime values. + +This specification describes a gradual type system for Python. + +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**. + +Static types +~~~~~~~~~~~~ + +A static type can intuitively be understood as denoting a set of runtime +values. For instance, the Python static type ``object`` is the set of all +Python objects. The Python static type ``bool`` is the set of values ``{ True, +False }``. The Python static type ``str`` is the set of all Python strings; +more precisely, the set of all Python objects whose runtime type (i.e. +``__class__`` attribute) is either ``str`` or a class that inherits ``str``, +including transitively; i.e. a type with ``str`` in its method resolution +order. Static types can also be specified in other ways. For example, +:ref:`Protocols` specify a static type which is the set of all objects which +share a certain set of attributes and/or methods. + +The dynamic type +~~~~~~~~~~~~~~~~ + +The dynamic type :ref:`Any` represents an unknown static type. It denotes some +unknown set of values. + +At first glance, this may appear similar to the static type ``object``, which +represents the set of all Python objects. But it is quite different. + +If a value has the static type ``object``, a static type checker should ensure +that all operations on the value are valid for all Python objects, or else emit +a static type error. This allows very few operations! For example, if ``x`` is +typed as ``object``, ``x.foo`` should be a static type error, because not all +Python objects have an attribute ``foo``. + +A value typed as :ref:`Any`, on the other hand, should be assumed to have +_some_ specific static type, but _which_ static type is not known. A static +checker should not emit any errors that depend on assuming a particular static +type; a static checker should instead assume that the runtime is responsible +for checking the type of operations on this value, as in a dynamically-typed +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 +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 (``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 +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 +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``. + +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. + +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, +``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``. + +We define a **consistency** relation over all types (the dynamic type, gradual +types, and static types.) + +A static type ``A`` is consistent with another static type ``B`` only if they +are the same type (``A`` is equivalent to ``B``.) + +The dynamic type ``Any`` is consistent with every type, and every type is +consistent with ``Any``. + +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``. + +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 symmetric. If ``A`` is consistent with ``B``, ``B`` +is also consistent with ``A``. It is also reflexive: ``A`` is always consistent +with ``A``. + +The consistent subtype relation +------------------------------- + +Given the consistency 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, +and ``A'`` is a subtype of ``B'``. + +For example, ``Any`` is a consistent subtype of ``int``, because ``int`` is a +materialization of ``Any``, and ``int`` is a subtype of ``int``. The same +materialization also gives that ``int`` is a consistent subtype of ``Any``. + +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 +(respectively, parameter's type annotation or return type annotation). -Union types ------------ - -Since accepting a small, limited set of expected types for a single -argument is common, the type system supports union types, created with the -``|`` operator. -Example:: - - def handle_employees(e: Employee | Sequence[Employee]) -> None: - if isinstance(e, Employee): - e = [e] - ... - -A type factored by ``T1 | T2 | ...`` is a supertype -of all types ``T1``, ``T2``, etc., so that a value that -is a member of one of these types is acceptable for an argument -annotated by ``T1 | T2 | ...``. - -One common case of union types are *optional* types. By default, -``None`` is an invalid value for any type, unless a default value of -``None`` has been provided in the function definition. Examples:: - - def handle_employee(e: Employee | None) -> None: ... - -A past version of this specification allowed type checkers to assume an optional -type when the default value is ``None``, as in this code:: - - def handle_employee(e: Employee = None): ... - -This would have been treated as equivalent to:: - - def handle_employee(e: Employee | None = None) -> None: ... - -This is no longer the recommended behavior. Type checkers should move -towards requiring the optional type to be made explicit. - -Support for singleton types in unions -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -A singleton instance is frequently used to mark some special condition, -in particular in situations where ``None`` is also a valid value -for a variable. Example:: - - _empty = object() - - def func(x=_empty): - if x is _empty: # default argument value - return 0 - elif x is None: # argument was provided and it's None - return 1 - else: - return x * 2 - -To allow precise typing in such situations, the user should use -a union type in conjunction with the ``enum.Enum`` class provided -by the standard library, so that type errors can be caught statically:: - - from enum import Enum - - class Empty(Enum): - token = 0 - _empty = Empty.token - - def func(x: int | None | Empty = _empty) -> int: - - boom = x * 42 # This fails type check - - if x is _empty: - return 0 - elif x is None: - return 1 - else: # At this point typechecker knows that x can only have type int - return x * 2 - -Since the subclasses of ``Enum`` cannot be further subclassed, -the type of variable ``x`` can be statically inferred in all branches -of the above example. The same approach is applicable if more than one -singleton object is needed: one can use an enumeration that has more than -one value:: - - class Reason(Enum): - timeout = 1 - error = 2 - - def process(response: str | Reason = '') -> str: - if response is Reason.timeout: - return 'TIMEOUT' - elif response is Reason.error: - return 'ERROR' - else: - # response can be only str, all other possible values exhausted - return 'PROCESSED: ' + response +We can say that a type ``A`` is "assignable to" a type ``B`` if ``A`` is a +consistent subtype of ``B``. + +References +---------- + +The concepts presented here are derived from the research literature in gradual +typing. See:: + +* `Victor Lanvin. A semantic foundation for gradual set-theoretic types. Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222 `_ diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index b94222e6..69362d62 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -8,16 +8,13 @@ Special types in annotations ``Any`` ------- -A special kind of type is ``Any``. Every type is consistent with -``Any``. It can be considered a type that has all values and all methods. -Note that ``Any`` and builtin type ``object`` are completely different. +``Any`` is the dynamic type. It represents some unknown static type, whose use +should not be checked statically. -When the type of a value is ``object``, the type checker will reject -almost all operations on it, and assigning it to a variable (or using -it as a return value) of a more specialized type is a type error. On -the other hand, when a value has type ``Any``, the type checker will -allow all operations on it, and a value of type ``Any`` can be assigned -to a variable (or used as a return value) of a more constrained type. +Every type is consistent with ``Any``, every type is a consistent subtype of +``Any``, and ``Any`` is a consistent subtype of every type. + +See :ref:`type-system-concepts` for more discussion of ``Any``. A function parameter without an annotation is assumed to be annotated with ``Any``. If a generic type is used without specifying type parameters, @@ -218,3 +215,98 @@ subtype of ``type[Base]``:: def new_pro_user(pro_user_class: type[ProUser]): user = new_user(pro_user_class) # OK ... + +.. _`union-types`: + +Union types +----------- + +Since accepting a small, limited set of expected types for a single +argument is common, the type system supports union types, created with the +``|`` operator. +Example:: + + def handle_employees(e: Employee | Sequence[Employee]) -> None: + if isinstance(e, Employee): + e = [e] + ... + +A type factored by ``T1 | T2 | ...`` is a supertype +of all types ``T1``, ``T2``, etc., so that a value that +is a member of one of these types is acceptable for an argument +annotated by ``T1 | T2 | ...``. + +One common case of union types are *optional* types. By default, +``None`` is an invalid value for any type, unless a default value of +``None`` has been provided in the function definition. Examples:: + + def handle_employee(e: Employee | None) -> None: ... + +A past version of this specification allowed type checkers to assume an optional +type when the default value is ``None``, as in this code:: + + def handle_employee(e: Employee = None): ... + +This would have been treated as equivalent to:: + + def handle_employee(e: Employee | None = None) -> None: ... + +This is no longer the recommended behavior. Type checkers should move +towards requiring the optional type to be made explicit. + +Support for singleton types in unions +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +A singleton instance is frequently used to mark some special condition, +in particular in situations where ``None`` is also a valid value +for a variable. Example:: + + _empty = object() + + def func(x=_empty): + if x is _empty: # default argument value + return 0 + elif x is None: # argument was provided and it's None + return 1 + else: + return x * 2 + +To allow precise typing in such situations, the user should use +a union type in conjunction with the ``enum.Enum`` class provided +by the standard library, so that type errors can be caught statically:: + + from enum import Enum + + class Empty(Enum): + token = 0 + _empty = Empty.token + + def func(x: int | None | Empty = _empty) -> int: + + boom = x * 42 # This fails type check + + if x is _empty: + return 0 + elif x is None: + return 1 + else: # At this point typechecker knows that x can only have type int + return x * 2 + +Since the subclasses of ``Enum`` cannot be further subclassed, +the type of variable ``x`` can be statically inferred in all branches +of the above example. The same approach is applicable if more than one +singleton object is needed: one can use an enumeration that has more than +one value:: + + class Reason(Enum): + timeout = 1 + error = 2 + + def process(response: str | Reason = '') -> str: + if response is Reason.timeout: + return 'TIMEOUT' + elif response is Reason.error: + return 'ERROR' + else: + # response can be only str, all other possible values exhausted + return 'PROCESSED: ' + response From bd4416ea1fddbcbed8c8467ab468b449ff7d9242 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 12:06:09 -0400 Subject: [PATCH 02/45] review feedback --- docs/spec/concepts.rst | 97 ++++++++++++++++++++++-------------------- 1 file changed, 52 insertions(+), 45 deletions(-) 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 From 3c332bff052f52d376eb7be3a851c522b6bbc538 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 12:25:07 -0400 Subject: [PATCH 03/45] prefer 'assignable to' over 'consistent subtype of' --- docs/spec/concepts.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index c13321b6..64730b91 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -174,6 +174,11 @@ function) if it is a consistent subtype of the variable's type annotation We can say that a type ``A`` is "assignable to" a type ``B`` if ``A`` is a consistent subtype of ``B``. +In the remainder of this specification, we will usually prefer the term +**assignable to** over "consistent subtype of". The two are synonyms, but +"assignable to" is shorter, and may communicate a clearer intuition to many +readers. + References ---------- From 6603f4337eaf2da3641c520aa93e3ca4a7212b6e Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 13:55:43 -0400 Subject: [PATCH 04/45] minor tweaks --- docs/spec/concepts.rst | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 64730b91..9ad638c6 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -43,9 +43,12 @@ Static, dynamic, and gradual types ---------------------------------- We will refer to types that do not contain :ref:`Any` as a sub-part as **static -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. +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 ~~~~~~~~~~~~ @@ -120,7 +123,8 @@ 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]``. +are both materializations of ``tuple[Any, Any]``. ``tuple[int, str]`` is also a +materialization of ``tuple[Any, str]``. 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``. From 137ab2a25439b3c6d4782ef4f0344049c80cf1b8 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 14:24:50 -0400 Subject: [PATCH 05/45] terms have types --- docs/spec/concepts.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 9ad638c6..404c3c75 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -73,17 +73,17 @@ unknown set of values. At first glance, this may appear similar to the static type ``object``, which represents the set of all Python objects. But it is quite different. -If a value has the static type ``object``, a static type checker should ensure -that all operations on the value are valid for all Python objects, or else emit -a static type error. This allows very few operations! For example, if ``x`` is +If a term has the static type ``object``, a static type checker should ensure +that operations on the term are valid for all Python objects, or else emit a +static type error. This allows very few operations! For example, if ``x`` is typed as ``object``, ``x.foo`` should be a static type error, because not all Python objects have an attribute ``foo``. -A value typed as :ref:`Any`, on the other hand, should be assumed to have +A term typed as :ref:`Any`, on the other hand, should be assumed to have _some_ specific static type, but _which_ static type is not known. A static checker should not emit any errors that depend on assuming a particular static type; a static checker should instead assume that the runtime is responsible -for checking the type of operations on this value, as in a dynamically-typed +for checking the type of operations on this term, as in a dynamically-typed language. The subtype relation From 24e6ee5330d8d5fd27960ed98da72f1714aa1979 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 15:06:29 -0400 Subject: [PATCH 06/45] review comments --- docs/spec/concepts.rst | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 404c3c75..314f2d9c 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -22,12 +22,12 @@ 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 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. +typing. Type-annotated Python allows mixing static and dynamic checking at a +fine level of granularity. 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. For example, a 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 @@ -118,13 +118,16 @@ 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 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]``. ``tuple[int, str]`` is also a -materialization of ``tuple[Any, str]``. +We define a **materialization** relation on gradual types. The intuition for +materialization is that it transforms a "more dynamic" type to a "more static" +type. Given a gradual type ``A``, if we replace zero or more occurrences of +``Any`` in ``A`` with some gradual type (which can be different for each +occurrence of ``Any``), the resulting gradual type ``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]``. ``tuple[int, +str]`` is also a materialization of ``tuple[Any, str]``. 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``. @@ -138,15 +141,15 @@ 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 ``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``. +consistent with ``A``, if and only if there exists some static type ``C`` which +is a materialization of both ``A`` and ``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]`` is consistent -with ``tuple[Any, int]`` and ``tuple[Any, int]`` is consistent with +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]``. From 9e9ebb496ec288b53374266985848adc83b3a275 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 15:22:11 -0400 Subject: [PATCH 07/45] use asymmetric example of assignable-to --- docs/spec/concepts.rst | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 314f2d9c..08b04882 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -157,22 +157,15 @@ 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 with ``A``. -The consistent subtype relation -------------------------------- +The assignable-to (or consistent subtyping) relation +---------------------------------------------------- -Given the materialization relation and the subtyping relation, we define the +Given the materialization relation and the subtyping relation, we can 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, and ``A'`` is a subtype of ``B'``. -For example, ``Any`` is a consistent subtype of ``int``, because ``int`` is a -materialization of ``Any``, and ``int`` is a subtype of ``int``. The same -materialization also gives that ``int`` is a consistent subtype of ``Any``. - -Consistent subtyping defines assignability ------------------------------------------- - Consistent subtyping defines "assignability" for Python. An expression can be 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 @@ -182,10 +175,20 @@ We can say that a type ``A`` is "assignable to" a type ``B`` if ``A`` is a consistent subtype of ``B``. In the remainder of this specification, we will usually prefer the term -**assignable to** over "consistent subtype of". The two are synonyms, but +**assignable to** over "consistent subtype of". The two are synonymous, but "assignable to" is shorter, and may communicate a clearer intuition to many readers. +For example, ``Any`` is assignable to ``int``, because ``int`` is a +materialization of ``Any``, and ``int`` is a subtype of ``int``. The same +materialization also gives that ``int`` is assignable to ``Any``. + +The assignable-to relation is not generally symmetric, though. If ``B`` is a +subtype of ``A``, then ``tuple[Any, B]`` is assignable to ``tuple[int, A]``, +because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a +subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to +``tuple[Any, B]``. + References ---------- From 12715589238a207c18afdf22c340f565e8b2ef6c Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 15:32:49 -0400 Subject: [PATCH 08/45] Any is equivalent to Any --- docs/spec/concepts.rst | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 08b04882..37fed966 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -116,14 +116,17 @@ The consistency relation 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 on gradual types. The intuition for -materialization is that it transforms a "more dynamic" type to a "more static" -type. Given a gradual type ``A``, if we replace zero or more occurrences of -``Any`` in ``A`` with some gradual type (which can be different for each -occurrence of ``Any``), the resulting gradual type ``B`` is a materialization -of ``A``. +supertype, or equivalence relations on static types described above. (We do +find it convenient to say, however, that ``Any`` is both subtype and supertype +of -- that is, equivalent to -- only itself. This can allow us to simplify +redundant multiple occurrences of ``Any`` out of more complex types.) + +To relate gradual types more generally, we define a **materialization** +relation. The intuition for materialization is that it transforms a "more +dynamic" type to a "more static" type. Given a gradual type ``A``, if we +replace zero or more occurrences of ``Any`` in ``A`` with some gradual type +(which can be different for each occurrence of ``Any``), the resulting gradual +type ``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]``. ``tuple[int, From 2ddd4adecfbec35cc32ea78044306272099940b3 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 16:26:38 -0400 Subject: [PATCH 09/45] add a short para on the gradual guarantee --- docs/spec/concepts.rst | 38 ++++++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 37fed966..9382fc68 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -29,13 +29,13 @@ mix of static and dynamic-only checking. For example, a 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 -:ref:`Any`. It indicates to the static type checker that this value should not -be subject to static checking. The system should not signal a static type -error for use of an expression with type :ref:`Any`. Instead, the expression's -value will be dynamically checked, according to the Python runtime's usual -checks on the types of runtime values. +In gradual typing, a dynamically typed term is indicated by a special "unknown" +or "dynamic" type. In Python, the unknown type is spelled :ref:`Any`. It +indicates to the static type checker that this term should not be subject to +static checking. The system should not signal a static type error for use of a +term with type :ref:`Any`. Instead, the term's type will be dynamically +checked, according to the Python runtime's usual checks on the types of runtime +values. This specification describes a gradual type system for Python. @@ -60,9 +60,11 @@ False }``. The Python static type ``str`` is the set of all Python strings; more precisely, the set of all Python objects whose runtime type (i.e. ``__class__`` attribute) is either ``str`` or a class that inherits ``str``, including transitively; i.e. a type with ``str`` in its method resolution -order. Static types can also be specified in other ways. For example, -:ref:`Protocols` specify a static type which is the set of all objects which -share a certain set of attributes and/or methods. +order. + +Static types can also be specified in other ways. For example, :ref:`Protocols` +specify a static type which is the set of all objects which share a certain set +of attributes and/or methods. The dynamic type ~~~~~~~~~~~~~~~~ @@ -86,6 +88,22 @@ type; a static checker should instead assume that the runtime is responsible for checking the type of operations on this term, as in a dynamically-typed language. +The gradual guarantee +~~~~~~~~~~~~~~~~~~~~~ + +:ref:`Any` allows gradually adding static types to a dynamically-typed program. +For a dynamically-typed program, a static checker has the type :ref:`Any` for +all terms, and should emit no errors on such a program. Adding more static type +annotations to the program (making the program more statically typed) may +result in static type errors, if the program is not correct or if the static +type annotations aren't able to fully represent the runtime types. Removing +static type annotations (making the program more dynamic) should not result in +additional static type errors. This is often referred to as the **gradual +guarantee**. + +In Python's type system, we don't take the gradual guarantee as a strict +requirement, but it's a useful guideline. + The subtype relation -------------------- From 971e9f2438a19f64df95c1c9000c61b0d61f2f0b Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 16:29:57 -0400 Subject: [PATCH 10/45] conciseness tweak --- docs/spec/concepts.rst | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 9382fc68..fe7a31ab 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -92,14 +92,13 @@ The gradual guarantee ~~~~~~~~~~~~~~~~~~~~~ :ref:`Any` allows gradually adding static types to a dynamically-typed program. -For a dynamically-typed program, a static checker has the type :ref:`Any` for -all terms, and should emit no errors on such a program. Adding more static type -annotations to the program (making the program more statically typed) may -result in static type errors, if the program is not correct or if the static -type annotations aren't able to fully represent the runtime types. Removing -static type annotations (making the program more dynamic) should not result in -additional static type errors. This is often referred to as the **gradual -guarantee**. +For a fully dynamically-typed program, a static checker has the type :ref:`Any` +for all terms, and should emit no errors. Adding more static type annotations +to the program (making the program more statically typed) may result in static +type errors, if the program is not correct or if the static type annotations +aren't able to fully represent the runtime types. Removing static type +annotations (making the program more dynamic) should not result in additional +static type errors. This is often referred to as the **gradual guarantee**. In Python's type system, we don't take the gradual guarantee as a strict requirement, but it's a useful guideline. From 10fda4e05ce3d7bfde0f3f538d600d844faa3520 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 22 May 2024 17:57:15 -0400 Subject: [PATCH 11/45] use 'assignable to' in Any description --- docs/spec/special-types.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index 69362d62..303361c0 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -11,8 +11,7 @@ Special types in annotations ``Any`` is the dynamic type. It represents some unknown static type, whose use should not be checked statically. -Every type is consistent with ``Any``, every type is a consistent subtype of -``Any``, and ``Any`` is a consistent subtype of every type. +Every type is assignable to ``Any``, and ``Any`` is assignable to every type. See :ref:`type-system-concepts` for more discussion of ``Any``. From f4110bb3433bb331fb2b0a540de21a656f21717e Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 23 May 2024 09:57:25 -0400 Subject: [PATCH 12/45] incorporate some of Eric Traut's feedback --- docs/spec/concepts.rst | 267 +++++++++++++++++++++++++----------- docs/spec/special-types.rst | 98 +------------ 2 files changed, 185 insertions(+), 180 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index fe7a31ab..44aa1492 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -14,86 +14,85 @@ not well-typed (i.e., one that contains a type error) will not run. Java and C++ are examples of statically-typed object-oriented languages. A **dynamically-typed** programming language does not run a type-checker before -running a program. Instead, it will check the types of values before performing +running a program. Instead, it checks 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 -historically a dynamically-typed language. - -**Gradual typing** is the name for a specific way to combine static and dynamic -typing. Type-annotated Python allows mixing static and dynamic checking at a -fine level of granularity. 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. For example, a dictionary could be +language such as attribute access or arithmetic are. Python is a +dynamically-typed language. + +**Gradual typing** is a way to combine static and dynamic typing. +Type-annotated Python allows opting in to static type checking at a fine level +of granularity, so that some type errors can be caught statically, before +running the program. Variables, parameters, and returns can optionally be given +a static type annotation. Even within the type of a single data structure, +static type checking is opt-in and granular. For example, a dictionary can be annotated to have static checking of the key type but only dynamic checking of the value type. -In gradual typing, a dynamically typed term is indicated by a special "unknown" -or "dynamic" type. In Python, the unknown type is spelled :ref:`Any`. It -indicates to the static type checker that this term should not be subject to -static checking. The system should not signal a static type error for use of a -term with type :ref:`Any`. Instead, the term's type will be dynamically -checked, according to the Python runtime's usual checks on the types of runtime -values. - -This specification describes a gradual type system for Python. +In gradual typing, a special "unknown" or "dynamic" type is used in the static +type system for names or expressions whose type is not known statically. In +Python, this type is spelled :ref:`Any`. Because :ref:`Any` indicates a +statically-unknown type, the static type checker can't check type correctness +of operations on expressions typed as :ref:`Any`. These operations are only +dynamically checked, via the Python runtime's usual dynamic checking. -Static, dynamic, and gradual types ----------------------------------- +The Python type system also uses ``...`` within :ref:`callable` and :ref:`Tuple +` types to indicate a statically-unknown component of a type. The +detailed rules for these usages are discussed in their respective sections of +the specification. -We will refer to types that do not contain :ref:`Any` as a sub-part as **static -types**. +This specification describes a gradual type system for Python. -:ref:`Any` itself is the **dynamic type**. +Fully static and gradual types +------------------------------ -A **gradual type** can be a static type, :ref:`Any` itself, or a type that -contains :ref:`Any` as a sub-part. +We will refer to types that do not contain :ref:`Any` (or the ``...`` in +callable or tuple types) as a sub-part as **fully static types**. -Static types -~~~~~~~~~~~~ +A **gradual type** can be a fully static type, :ref:`Any` itself, or a type +that contains :ref:`Any` (or ``...``) as a sub-part. -A static type can intuitively be understood as denoting a set of runtime -values. For instance, the Python static type ``object`` is the set of all -Python objects. The Python static type ``bool`` is the set of values ``{ True, -False }``. The Python static type ``str`` is the set of all Python strings; -more precisely, the set of all Python objects whose runtime type (i.e. -``__class__`` attribute) is either ``str`` or a class that inherits ``str``, -including transitively; i.e. a type with ``str`` in its method resolution -order. +Fully static types +~~~~~~~~~~~~~~~~~~ -Static types can also be specified in other ways. For example, :ref:`Protocols` -specify a static type which is the set of all objects which share a certain set -of attributes and/or methods. +A fully static type denotes a set of potential runtime values. For instance, +the Python static type ``object`` is the set of all Python objects. The Python +static type ``bool`` is the set of values ``{ True, False }``. The Python +static type ``str`` is the set of all Python strings; more precisely, the set +of all Python objects whose runtime type (``__class__`` attribute) is either +``str`` or a class that inherits directly or indirectly from ``str``. A +:ref:`Protocol ` denotes the set of all objects which share a +certain set of attributes and/or methods. -The dynamic type -~~~~~~~~~~~~~~~~ +Gradual types +~~~~~~~~~~~~~ -The dynamic type :ref:`Any` represents an unknown static type. It denotes some -unknown set of values. +:ref:`Any` represents an unknown static type. It denotes some unknown set of +values. -At first glance, this may appear similar to the static type ``object``, which -represents the set of all Python objects. But it is quite different. +This may appear similar to the fully static type ``object``, which represents +the set of all Python objects, but it is quite different. -If a term has the static type ``object``, a static type checker should ensure -that operations on the term are valid for all Python objects, or else emit a -static type error. This allows very few operations! For example, if ``x`` is -typed as ``object``, ``x.foo`` should be a static type error, because not all -Python objects have an attribute ``foo``. +If an expression has the type ``object``, a static type checker should ensure +that operations on the expression are valid for all Python objects, or else +emit a static type error. This allows very few operations! For example, if +``x`` is typed as ``object``, ``x.foo`` should be a static type error because +not all Python objects have an attribute ``foo``. -A term typed as :ref:`Any`, on the other hand, should be assumed to have +An expression typed as :ref:`Any`, on the other hand, should be assumed to have _some_ specific static type, but _which_ static type is not known. A static -checker should not emit any errors that depend on assuming a particular static -type; a static checker should instead assume that the runtime is responsible -for checking the type of operations on this term, as in a dynamically-typed -language. +checker should not emit any errors that depend on assuming a particular type. A +static checker should instead assume that the runtime is responsible for +checking the type of operations on this expression, as usual in a +dynamically-typed language. The gradual guarantee ~~~~~~~~~~~~~~~~~~~~~ :ref:`Any` allows gradually adding static types to a dynamically-typed program. For a fully dynamically-typed program, a static checker has the type :ref:`Any` -for all terms, and should emit no errors. Adding more static type annotations +for all expressions, and should emit no errors. Adding static type annotations to the program (making the program more statically typed) may result in static type errors, if the program is not correct or if the static type annotations aren't able to fully represent the runtime types. Removing static type @@ -103,14 +102,14 @@ static type errors. This is often referred to as the **gradual guarantee**. In Python's type system, we don't take the gradual guarantee as a strict requirement, but it's a useful guideline. -The subtype relation --------------------- +Subtype, supertype, and type equivalence +---------------------------------------- -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 ``C`` is a subtype of -``B`` and ``B`` is a subtype of ``A``, then ``C`` is a subtype of ``A``) and +A fully static type ``B`` is a **subtype** of another fully 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 ``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 @@ -118,25 +117,24 @@ The **supertype** relation is the inverse of subtype: ``A`` is a supertype of 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 -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 also define an **equivalence** relation on fully static types: the types +``A`` and ``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`` (or as a "strict +We may describe a type ``B`` as "narrower" than a type ``A`` (or as a "proper subtype" of ``A``) if ``B`` is a subtype of ``A`` and ``B`` is not equivalent -to ``A``. +to ``A``. In the same scenario we can describe the type ``A`` as "wider" than +``B``, or a "proper supertype" of ``B``. -The consistency relation ------------------------- +Materialization +--------------- 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 do -find it convenient to say, however, that ``Any`` is both subtype and supertype -of -- that is, equivalent to -- only itself. This can allow us to simplify -redundant multiple occurrences of ``Any`` out of more complex types.) +supertype, or equivalence relations on static types described above. To relate gradual types more generally, we define a **materialization** relation. The intuition for materialization is that it transforms a "more @@ -155,18 +153,22 @@ static" type than ``A``, and ``A`` is a "more dynamic" type than ``B``. The materialization relation is both transitive and reflexive, so it defines a preorder on gradual types. -We also define a **consistency** relation on gradual types. +Consistency +----------- + +We define a **consistency** relation on gradual types, based on +materialization. -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 fully static type ``A`` is consistent with another fully static type ``B`` if +and only if they are the same type (``A`` is equivalent to ``B``.) A gradual type ``A`` is consistent with a gradual type ``B``, and ``B`` is -consistent with ``A``, if and only if there exists some static type ``C`` which -is a materialization of both ``A`` and ``B``. +consistent with ``A``, if and only if there exists some fully static type ``C`` +which is a materialization of both ``A`` and ``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.) +``Any`` is consistent with every type, and every type is consistent with +``Any``. (This follows from the definitions of materialization and consistency +but is worth stating explicitly.) The consistency relation is not transitive. ``tuple[int, int]`` is consistent with ``tuple[Any, int]``, and ``tuple[Any, int]`` is consistent with @@ -209,6 +211,105 @@ because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to ``tuple[Any, B]``. +.. _`union-types`: + +Union types +----------- + +Since accepting a small, limited set of expected types for a single +argument is common, the type system supports union types, created with the +``|`` operator. +Example:: + + def handle_employees(e: Employee | Sequence[Employee]) -> None: + if isinstance(e, Employee): + e = [e] + ... + +A (fully static) union type ``T1 | T2 | ...`` represents the set of values +formed by the union of all the sets of values represented by ``T1``, ``T2``, +etc. Thus, by the definition of the supertype relation, the union ``T1 | T2`` +is a supertype of both ``T1`` and ``T2``. Via materialization, the gradual +types ``S1`` and ``S2`` are both assignable to a gradual union type ``S1 | +S2``. + +One common case of union types are *optional* types, which are a union with +``None``. Example:: + + def handle_employee(e: Employee | None) -> None: ... + +Either an instance of ``Employee`` or the value ``None`` are assignable to the +union ``Employee | None``. + +A past version of this specification allowed type checkers to assume an optional +type when the default value is ``None``, as in this code:: + + def handle_employee(e: Employee = None): ... + +This would have been treated as equivalent to:: + + def handle_employee(e: Employee | None = None) -> None: ... + +This is no longer the recommended behavior. Type checkers should move +towards requiring the optional type to be made explicit. + +Support for singleton types in unions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A singleton instance is frequently used to mark some special condition, +in particular in situations where ``None`` is also a valid value +for a variable. Example:: + + _empty = object() + + def func(x=_empty): + if x is _empty: # default argument value + return 0 + elif x is None: # argument was provided and it's None + return 1 + else: + return x * 2 + +To allow precise typing in such situations, the user should use +a union type in conjunction with the ``enum.Enum`` class provided +by the standard library, so that type errors can be caught statically:: + + from enum import Enum + + class Empty(Enum): + token = 0 + _empty = Empty.token + + def func(x: int | None | Empty = _empty) -> int: + + boom = x * 42 # This fails type check + + if x is _empty: + return 0 + elif x is None: + return 1 + else: # At this point typechecker knows that x can only have type int + return x * 2 + +Since the subclasses of ``Enum`` cannot be further subclassed, +the type of variable ``x`` can be statically inferred in all branches +of the above example. The same approach is applicable if more than one +singleton object is needed: one can use an enumeration that has more than +one value:: + + class Reason(Enum): + timeout = 1 + error = 2 + + def process(response: str | Reason = '') -> str: + if response is Reason.timeout: + return 'TIMEOUT' + elif response is Reason.error: + return 'ERROR' + else: + # response can be only str, all other possible values exhausted + return 'PROCESSED: ' + response + References ---------- diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index 303361c0..985ffeca 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -8,8 +8,7 @@ Special types in annotations ``Any`` ------- -``Any`` is the dynamic type. It represents some unknown static type, whose use -should not be checked statically. +``Any`` represents an unknown static type. Every type is assignable to ``Any``, and ``Any`` is assignable to every type. @@ -214,98 +213,3 @@ subtype of ``type[Base]``:: def new_pro_user(pro_user_class: type[ProUser]): user = new_user(pro_user_class) # OK ... - -.. _`union-types`: - -Union types ------------ - -Since accepting a small, limited set of expected types for a single -argument is common, the type system supports union types, created with the -``|`` operator. -Example:: - - def handle_employees(e: Employee | Sequence[Employee]) -> None: - if isinstance(e, Employee): - e = [e] - ... - -A type factored by ``T1 | T2 | ...`` is a supertype -of all types ``T1``, ``T2``, etc., so that a value that -is a member of one of these types is acceptable for an argument -annotated by ``T1 | T2 | ...``. - -One common case of union types are *optional* types. By default, -``None`` is an invalid value for any type, unless a default value of -``None`` has been provided in the function definition. Examples:: - - def handle_employee(e: Employee | None) -> None: ... - -A past version of this specification allowed type checkers to assume an optional -type when the default value is ``None``, as in this code:: - - def handle_employee(e: Employee = None): ... - -This would have been treated as equivalent to:: - - def handle_employee(e: Employee | None = None) -> None: ... - -This is no longer the recommended behavior. Type checkers should move -towards requiring the optional type to be made explicit. - -Support for singleton types in unions -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -A singleton instance is frequently used to mark some special condition, -in particular in situations where ``None`` is also a valid value -for a variable. Example:: - - _empty = object() - - def func(x=_empty): - if x is _empty: # default argument value - return 0 - elif x is None: # argument was provided and it's None - return 1 - else: - return x * 2 - -To allow precise typing in such situations, the user should use -a union type in conjunction with the ``enum.Enum`` class provided -by the standard library, so that type errors can be caught statically:: - - from enum import Enum - - class Empty(Enum): - token = 0 - _empty = Empty.token - - def func(x: int | None | Empty = _empty) -> int: - - boom = x * 42 # This fails type check - - if x is _empty: - return 0 - elif x is None: - return 1 - else: # At this point typechecker knows that x can only have type int - return x * 2 - -Since the subclasses of ``Enum`` cannot be further subclassed, -the type of variable ``x`` can be statically inferred in all branches -of the above example. The same approach is applicable if more than one -singleton object is needed: one can use an enumeration that has more than -one value:: - - class Reason(Enum): - timeout = 1 - error = 2 - - def process(response: str | Reason = '') -> str: - if response is Reason.timeout: - return 'TIMEOUT' - elif response is Reason.error: - return 'ERROR' - else: - # response can be only str, all other possible values exhausted - return 'PROCESSED: ' + response From ac6273ef02130a3d32228602547a7b96d68ae410 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 23 May 2024 18:34:01 -0600 Subject: [PATCH 13/45] more on union --- docs/spec/concepts.rst | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 44aa1492..fc92af54 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -226,12 +226,25 @@ Example:: e = [e] ... -A (fully static) union type ``T1 | T2 | ...`` represents the set of values -formed by the union of all the sets of values represented by ``T1``, ``T2``, -etc. Thus, by the definition of the supertype relation, the union ``T1 | T2`` -is a supertype of both ``T1`` and ``T2``. Via materialization, the gradual -types ``S1`` and ``S2`` are both assignable to a gradual union type ``S1 | -S2``. +A union type ``T1 | T2``, where ``T1`` and ``T2`` are fully static types, +represents the set of values formed by the union of all the sets of values +represented by ``T1`` and ``T2``. Thus, by the definition of the supertype +relation, the union ``T1 | T2`` is a supertype of both ``T1`` and ``T2``. Via +materialization, the gradual types ``S1`` and ``S2`` are both assignable to a +gradual union type ``S1 | S2``. + +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 +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. + +As a special case, the union ``Any | Any`` can be simplified to ``Any``: the +union of two unknown sets of objects is an unknown set of objects. + +Union with None +~~~~~~~~~~~~~~~ One common case of union types are *optional* types, which are a union with ``None``. Example:: @@ -316,4 +329,5 @@ References The concepts presented here are derived from the research literature in gradual typing. See e.g.: +* `Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual Typing: A New Perspective. `_ Proc. ACM Program. Lang. 3, POPL, Article 16 (January 2019), 112 pages * `Victor Lanvin. A semantic foundation for gradual set-theoretic types. `_ Computer science. Université Paris Cité, 2021. English. NNT : 2021UNIP7159. tel-03853222 From 15c0d56692df1b53121b15f26a1c57f4dc8ba442 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 23 May 2024 19:31:22 -0600 Subject: [PATCH 14/45] add an example of bounded gradual type --- docs/spec/concepts.rst | 39 ++++++++++++++++++++++++++++++++------- 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index fc92af54..aa2278a0 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -34,7 +34,7 @@ In gradual typing, a special "unknown" or "dynamic" type is used in the static type system for names or expressions whose type is not known statically. In Python, this type is spelled :ref:`Any`. Because :ref:`Any` indicates a statically-unknown type, the static type checker can't check type correctness -of operations on expressions typed as :ref:`Any`. These operations are only +of operations on expressions typed as :ref:`Any`. These operations are dynamically checked, via the Python runtime's usual dynamic checking. The Python type system also uses ``...`` within :ref:`callable` and :ref:`Tuple @@ -81,12 +81,36 @@ emit a static type error. This allows very few operations! For example, if not all Python objects have an attribute ``foo``. An expression typed as :ref:`Any`, on the other hand, should be assumed to have -_some_ specific static type, but _which_ static type is not known. A static -checker should not emit any errors that depend on assuming a particular type. A -static checker should instead assume that the runtime is responsible for -checking the type of operations on this expression, as usual in a +_some_ specific static type, but _which_ static type is not known. Thus, a +static checker should not emit errors that depend on assuming a particular +type. A static checker should instead assume that the runtime is responsible +for checking the type of operations on this expression, as usual in a dynamically-typed language. +Similarly, a gradual type such as ``tuple[int, Any]`` (see :ref:`tuples`) or +``int | Any`` (see :ref:`union-types`) does not represent a single set of +Python objects; rather, it represents a (bounded) range of possible sets of +values. + +In the same way that ``Any`` does not represent "the set of all Python objects" +but rather "an unknown set of objects", ``tuple[int, Any]`` does not represent +"the set of all length-two tuples whose first element is an integer." That is a +fully static type, spelled ``tuple[int, object]``. In contrast, ``tuple[int, +Any]`` represents some unknown set of tuple values; it might be the set of all +tuples of two integers, or the set of all tuples of an integer and a string, or +some other set of tuple values. + +In practice, this difference is seen (for example) in the fact that we can +assign an expression of type ``tuple[int, Any]`` to a target typed as +``tuple[int, int]``, whereas assigning ``tuple[int, object]`` to ``tuple[int, +int]`` is a static type error. (We formalize this difference in the below +definitions of materialization and assignability.) + +In the same way that the fully static type ``object`` is the upper bound for +the possible sets of values represented by ``Any``, the fully static type +``tuple[int, object]`` is the upper bound for the possible sets of values +represented by ``tuple[int, Any]``. + The gradual guarantee ~~~~~~~~~~~~~~~~~~~~~ @@ -133,8 +157,9 @@ Materialization --------------- 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. +known single set of values (it represents an unknown set of values.) Thus it is +not in the domain of the subtype, supertype, or equivalence relations on static +types described above. To relate gradual types more generally, we define a **materialization** relation. The intuition for materialization is that it transforms a "more From efdbc5f2cb98457a6d5a4e3e8bb507877d11b870 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 23 May 2024 21:13:08 -0600 Subject: [PATCH 15/45] add section on attributes and methods --- docs/spec/concepts.rst | 41 ++++++++++++++++++++++++++++++++++------- 1 file changed, 34 insertions(+), 7 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index aa2278a0..176d4340 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -81,11 +81,11 @@ emit a static type error. This allows very few operations! For example, if not all Python objects have an attribute ``foo``. An expression typed as :ref:`Any`, on the other hand, should be assumed to have -_some_ specific static type, but _which_ static type is not known. Thus, a -static checker should not emit errors that depend on assuming a particular -type. A static checker should instead assume that the runtime is responsible -for checking the type of operations on this expression, as usual in a -dynamically-typed language. +_some_ specific static type, but _which_ static type is not known. A static +type checker should not emit static type errors on an expression or statement +if :ref:`Any` might represent a static type which would avoid the error. (This +intuition is made more precise below, in our definitions of materialization and +assignability.) Similarly, a gradual type such as ``tuple[int, Any]`` (see :ref:`tuples`) or ``int | Any`` (see :ref:`union-types`) does not represent a single set of @@ -103,8 +103,8 @@ some other set of tuple values. In practice, this difference is seen (for example) in the fact that we can assign an expression of type ``tuple[int, Any]`` to a target typed as ``tuple[int, int]``, whereas assigning ``tuple[int, object]`` to ``tuple[int, -int]`` is a static type error. (We formalize this difference in the below -definitions of materialization and assignability.) +int]`` is a static type error. (Again, we formalize this difference in the +below definitions of materialization and assignability.) In the same way that the fully static type ``object`` is the upper bound for the possible sets of values represented by ``Any``, the fully static type @@ -236,6 +236,33 @@ because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to ``tuple[Any, B]``. +Attributes and methods +---------------------- + +In Python, we can do more with objects at runtime than just assign them to +names, pass them to functions, or return them from functions. We can also +get/set attributes and call methods. + +In the Python object model, the operations that can be performed on a value all +de-sugar to method calls. For example, ``a + b`` is syntactic sugar for either +``a.__add__(b)`` or ``b.__radd__(a)``. + +For a static type checker, accessing ``a.foo`` is a type error unless all +possible objects in the set represented by the type of ``a`` have the ``foo`` +attribute. + +If all objects in the set represented by the fully static type ``A`` have a +``foo`` attribute, we can say that the type ``A`` has the ``foo`` attribute. + +If the type ``A`` of ``a`` in ``a.foo`` is a gradual type, it may not represent +a single set of objects. In this case, ``a.foo`` is not a type error if and +only if there exists a materialization of ``A`` which has the ``foo`` +attribute. + +Equivalently, we can say that ``a.foo`` is a type error unless the type of +``a`` is assignable to a type that has the ``foo`` attribute. + + .. _`union-types`: Union types From e4537ac46b34fc94e581159ba0321aaec1242e11 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sun, 26 May 2024 14:23:28 -0600 Subject: [PATCH 16/45] more feedback and tweaks --- docs/spec/concepts.rst | 52 ++++++++++++++++++++++-------------------- 1 file changed, 27 insertions(+), 25 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 176d4340..2ec92085 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -37,10 +37,10 @@ statically-unknown type, the static type checker can't check type correctness of operations on expressions typed as :ref:`Any`. These operations are dynamically checked, via the Python runtime's usual dynamic checking. -The Python type system also uses ``...`` within :ref:`callable` and :ref:`Tuple -` types to indicate a statically-unknown component of a type. The -detailed rules for these usages are discussed in their respective sections of -the specification. +The Python type system also uses ``...`` within :ref:`Callable` types and +within ``tuple[Any, ...]`` (see :ref:`tuples`) to indicate a statically-unknown +component of a type. The detailed rules for these usages are discussed in their +respective sections of the specification. This specification describes a gradual type system for Python. @@ -48,22 +48,23 @@ Fully static and gradual types ------------------------------ We will refer to types that do not contain :ref:`Any` (or the ``...`` in -callable or tuple types) as a sub-part as **fully static types**. +``Callable`` or ``tuple[Any, ...]``) as a sub-part as **fully static types**. A **gradual type** can be a fully static type, :ref:`Any` itself, or a type -that contains :ref:`Any` (or ``...``) as a sub-part. +that contains :ref:`Any` (or the ``...`` in ``Callable`` or ``tuple[Any, +...]``) as a sub-part. Fully static types ~~~~~~~~~~~~~~~~~~ A fully static type denotes a set of potential runtime values. For instance, -the Python static type ``object`` is the set of all Python objects. The Python -static type ``bool`` is the set of values ``{ True, False }``. The Python -static type ``str`` is the set of all Python strings; more precisely, the set -of all Python objects whose runtime type (``__class__`` attribute) is either -``str`` or a class that inherits directly or indirectly from ``str``. A -:ref:`Protocol ` denotes the set of all objects which share a -certain set of attributes and/or methods. +the fully static type ``object`` is the set of all Python objects. The fully +static type ``bool`` is the set of values ``{ True, False }``. The fully static +type ``str`` is the set of all Python strings; more precisely, the set of all +Python objects whose runtime type (``__class__`` attribute) is either ``str`` +or a class that inherits directly or indirectly from ``str``. A :ref:`Protocol +` denotes the set of all objects which share a certain set of +attributes and/or methods. Gradual types ~~~~~~~~~~~~~ @@ -103,7 +104,7 @@ some other set of tuple values. In practice, this difference is seen (for example) in the fact that we can assign an expression of type ``tuple[int, Any]`` to a target typed as ``tuple[int, int]``, whereas assigning ``tuple[int, object]`` to ``tuple[int, -int]`` is a static type error. (Again, we formalize this difference in the +int]`` is a static type error. (Again, we formalize this distinction in the below definitions of materialization and assignability.) In the same way that the fully static type ``object`` is the upper bound for @@ -168,8 +169,8 @@ replace zero or more occurrences of ``Any`` in ``A`` with some gradual type (which can be different for each occurrence of ``Any``), the resulting gradual type ``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]``. ``tuple[int, +For instance, ``tuple[int, str]`` (a fully static type) and ``tuple[Any, str]`` +(a gradual type) are both materializations of ``tuple[Any, Any]``. ``tuple[int, str]`` is also a materialization of ``tuple[Any, str]``. If ``B`` is a materialization of ``A``, we can say that ``B`` is a "more @@ -207,19 +208,19 @@ with ``A``. The assignable-to (or consistent subtyping) relation ---------------------------------------------------- -Given the materialization relation and the subtyping relation, we can 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, -and ``A'`` is a subtype of ``B'``. +Given the materialization relation and the subtyping relation, we can define +the **consistent subtype** relation over all types. A type ``B`` is a +consistent subtype of a type ``A`` if there exists a materialization ``A'`` of +``A`` and a materialization ``B'`` of ``B``, where ``A'`` and ``B'`` are both +fully static types, and ``B'`` is a subtype of ``A'``. Consistent subtyping defines "assignability" for Python. An expression can be 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 -consistent subtype of ``B``. +We can say that a type ``B`` is "assignable to" a type ``A`` if ``B`` is a +consistent subtype of ``A``. In the remainder of this specification, we will usually prefer the term **assignable to** over "consistent subtype of". The two are synonymous, but @@ -249,7 +250,8 @@ de-sugar to method calls. For example, ``a + b`` is syntactic sugar for either For a static type checker, accessing ``a.foo`` is a type error unless all possible objects in the set represented by the type of ``a`` have the ``foo`` -attribute. +attribute. (We consider an implementation of ``__getattr__`` to be a getter for +all attribute names, and similarly for ``__setattr__`` and ``__delattr__``). If all objects in the set represented by the fully static type ``A`` have a ``foo`` attribute, we can say that the type ``A`` has the ``foo`` attribute. @@ -279,7 +281,7 @@ Example:: ... A union type ``T1 | T2``, where ``T1`` and ``T2`` are fully static types, -represents the set of values formed by the union of all the sets of values +represents the set of values formed by the union of the sets of values represented by ``T1`` and ``T2``. Thus, by the definition of the supertype relation, the union ``T1 | T2`` is a supertype of both ``T1`` and ``T2``. Via materialization, the gradual types ``S1`` and ``S2`` are both assignable to a From 6bebab446c1ee8de987184c3fd3478b16e49b92b Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 13:37:20 -0600 Subject: [PATCH 17/45] review comments --- docs/spec/concepts.rst | 103 ++++++++++++++++++++++------------------- 1 file changed, 55 insertions(+), 48 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 2ec92085..7c32282b 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -6,39 +6,39 @@ Type system concepts Static, dynamic, and gradual typing ----------------------------------- -A **statically-typed** programming language runs a type-checker before running -a program. The program is required to be well-typed according to the language's +A **statically typed** programming language runs a type checker before running +a program. The program is required to be well typed according to the language's type system. The type system assigns a type to all expressions in the language and verifies that their uses obey the typing rules. Normally, a program that is -not well-typed (i.e., one that contains a type error) will not run. Java and -C++ are examples of statically-typed object-oriented languages. +not well typed (i.e., one that contains a type error) will not run. Java and +C++ are examples of statically typed object-oriented languages. -A **dynamically-typed** programming language does not run a type-checker before +A **dynamically typed** programming language does not run a type-checker before running a program. Instead, it checks 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 are. Python is a -dynamically-typed language. +dynamically typed language. **Gradual typing** is a way to combine static and dynamic typing. Type-annotated Python allows opting in to static type checking at a fine level -of granularity, so that some type errors can be caught statically, before +of granularity, so that some type errors can be caught statically, without running the program. Variables, parameters, and returns can optionally be given a static type annotation. Even within the type of a single data structure, -static type checking is opt-in and granular. For example, a dictionary can be -annotated to have static checking of the key type but only dynamic checking of -the value type. - -In gradual typing, a special "unknown" or "dynamic" type is used in the static -type system for names or expressions whose type is not known statically. In -Python, this type is spelled :ref:`Any`. Because :ref:`Any` indicates a -statically-unknown type, the static type checker can't check type correctness -of operations on expressions typed as :ref:`Any`. These operations are +static type checking is optional and granular. For example, a dictionary can be +annotated to enable static checking of the key type but only have dynamic +runtime checking of the value type. + +A **gradual** type system is one in which a special "unknown" or "dynamic" type +is used to describe names or expressions whose types are not known statically. +In Python, this type is spelled :ref:`Any`. Because :ref:`Any` indicates a +statically unknown type, the static type checker can't check type correctness +of operations on expressions typed as :ref:`Any`. These operations are still dynamically checked, via the Python runtime's usual dynamic checking. The Python type system also uses ``...`` within :ref:`Callable` types and -within ``tuple[Any, ...]`` (see :ref:`tuples`) to indicate a statically-unknown +within ``tuple[Any, ...]`` (see :ref:`tuples`) to indicate a statically unknown component of a type. The detailed rules for these usages are discussed in their respective sections of the specification. @@ -70,7 +70,7 @@ Gradual types ~~~~~~~~~~~~~ :ref:`Any` represents an unknown static type. It denotes some unknown set of -values. +runtime values. This may appear similar to the fully static type ``object``, which represents the set of all Python objects, but it is quite different. @@ -115,14 +115,15 @@ represented by ``tuple[int, Any]``. The gradual guarantee ~~~~~~~~~~~~~~~~~~~~~ -:ref:`Any` allows gradually adding static types to a dynamically-typed program. -For a fully dynamically-typed program, a static checker has the type :ref:`Any` -for all expressions, and should emit no errors. Adding static type annotations -to the program (making the program more statically typed) may result in static -type errors, if the program is not correct or if the static type annotations -aren't able to fully represent the runtime types. Removing static type -annotations (making the program more dynamic) should not result in additional -static type errors. This is often referred to as the **gradual guarantee**. +:ref:`Any` allows gradually adding static types to a dynamically typed program. +In a fully dynamically typed program, a static checker assigns the type +:ref:`Any` to all expressions, and should emit no errors. Inferring static +types or adding type annotations to the program (making the program more +statically typed) may result in static type errors, if the program is not +correct or if the static types aren't able to fully represent the runtime +types. Removing type annotations (making the program more dynamic) should not +result in additional static type errors. This is often referred to as the +**gradual guarantee**. In Python's type system, we don't take the gradual guarantee as a strict requirement, but it's a useful guideline. @@ -158,16 +159,16 @@ Materialization --------------- Since :ref:`Any` represents an unknown static type, it does not represent any -known single set of values (it represents an unknown set of values.) Thus it is +known single set of values (it represents an unknown set of values). Thus it is not in the domain of the subtype, supertype, or equivalence relations on static types described above. To relate gradual types more generally, we define a **materialization** -relation. The intuition for materialization is that it transforms a "more -dynamic" type to a "more static" type. Given a gradual type ``A``, if we -replace zero or more occurrences of ``Any`` in ``A`` with some gradual type -(which can be different for each occurrence of ``Any``), the resulting gradual -type ``B`` is a materialization of ``A``. +relation. Materialization transforms a "more dynamic" type to a "more static" +type. Given a gradual type ``A``, if we replace zero or more occurrences of +``Any`` in ``A`` with some gradual type (which can be different for each +occurrence of ``Any``), the resulting gradual type ``B`` is a materialization +of ``A``. For instance, ``tuple[int, str]`` (a fully static type) and ``tuple[Any, str]`` (a gradual type) are both materializations of ``tuple[Any, Any]``. ``tuple[int, @@ -186,7 +187,7 @@ We define a **consistency** relation on gradual types, based on materialization. A fully static type ``A`` is consistent with another fully static type ``B`` if -and only if they are the same type (``A`` is equivalent to ``B``.) +and only if they are the same type (``A`` is equivalent to ``B``). A gradual type ``A`` is consistent with a gradual type ``B``, and ``B`` is consistent with ``A``, if and only if there exists some fully static type ``C`` @@ -216,7 +217,7 @@ fully static types, and ``B'`` is a subtype of ``A'``. Consistent subtyping defines "assignability" for Python. An expression can be 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 +function) if its type 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 ``B`` is "assignable to" a type ``A`` if ``B`` is a @@ -229,9 +230,9 @@ readers. For example, ``Any`` is assignable to ``int``, because ``int`` is a materialization of ``Any``, and ``int`` is a subtype of ``int``. The same -materialization also gives that ``int`` is assignable to ``Any``. +materialization also shows that ``int`` is assignable to ``Any``. -The assignable-to relation is not generally symmetric, though. If ``B`` is a +The assignable-to relation is not generally symmetric, however. If ``B`` is a subtype of ``A``, then ``tuple[Any, B]`` is assignable to ``tuple[int, A]``, because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to @@ -245,8 +246,9 @@ names, pass them to functions, or return them from functions. We can also get/set attributes and call methods. In the Python object model, the operations that can be performed on a value all -de-sugar to method calls. For example, ``a + b`` is syntactic sugar for either -``a.__add__(b)`` or ``b.__radd__(a)``. +de-sugar to method calls. For example, ``a + b`` is (roughly, eliding some +details) syntactic sugar for either ``type(a).__add__(a, b)`` or +``type(b).__radd__(b, a)``. For a static type checker, accessing ``a.foo`` is a type error unless all possible objects in the set represented by the type of ``a`` have the ``foo`` @@ -257,12 +259,12 @@ If all objects in the set represented by the fully static type ``A`` have a ``foo`` attribute, we can say that the type ``A`` has the ``foo`` attribute. If the type ``A`` of ``a`` in ``a.foo`` is a gradual type, it may not represent -a single set of objects. In this case, ``a.foo`` is not a type error if and -only if there exists a materialization of ``A`` which has the ``foo`` +a single set of objects. In this case, ``a.foo`` is a type error if and only if +there does not exist any materialization of ``A`` which has the ``foo`` attribute. -Equivalently, we can say that ``a.foo`` is a type error unless the type of -``a`` is assignable to a type that has the ``foo`` attribute. +Equivalently, ``a.foo`` is a type error unless the type of ``a`` is assignable +to a type that has the ``foo`` attribute. .. _`union-types`: @@ -280,12 +282,17 @@ Example:: e = [e] ... -A union type ``T1 | T2``, where ``T1`` and ``T2`` are fully static types, -represents the set of values formed by the union of the sets of values -represented by ``T1`` and ``T2``. Thus, by the definition of the supertype -relation, the union ``T1 | T2`` is a supertype of both ``T1`` and ``T2``. Via -materialization, the gradual types ``S1`` and ``S2`` are both assignable to a -gradual union type ``S1 | S2``. +A fully static union type ``T1 | T2``, where ``T1`` and ``T2`` are fully static +types, represents the set of values formed by the union of the sets of values +represented by ``T1`` and ``T2``, respectively. Thus, by the definition of the +supertype relation, the union ``T1 | T2`` is a supertype of both ``T1`` and +``T2``, and ``T1`` and ``T2`` are both subtypes of ``T1 | T2``. + +A gradual union type ``S1 | S2``, where ``S1`` and ``S2`` are gradual types, +represents all possible sets of values that could be formed by union of the +possible sets of values represented by materializations of ``S1`` and ``S2``, +respectively. Thus, via materialization, the gradual types ``S1`` and ``S2`` +are both assignable to a gradual union type ``S1 | S2``. If ``B`` is a subtype of ``A``, ``B | A`` is equivalent to ``A``. From 2900cceb0e6a801b67ba4e72240ec54e1386bcb0 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 13:56:25 -0600 Subject: [PATCH 18/45] a bit more on gradual unions --- docs/spec/concepts.rst | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 7c32282b..daceed39 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -291,8 +291,11 @@ supertype relation, the union ``T1 | T2`` is a supertype of both ``T1`` and A gradual union type ``S1 | S2``, where ``S1`` and ``S2`` are gradual types, represents all possible sets of values that could be formed by union of the possible sets of values represented by materializations of ``S1`` and ``S2``, -respectively. Thus, via materialization, the gradual types ``S1`` and ``S2`` -are both assignable to a gradual union type ``S1 | S2``. +respectively. + +For any materialization of ``S1`` to ``T1`` and ``S2`` to ``T2``, ``S1 | S2`` +can likewise be materialized to ``T1 | T2``. Thus, the gradual types ``S1`` and +``S2`` are both assignable to the gradual union type ``S1 | S2``. If ``B`` is a subtype of ``A``, ``B | A`` is equivalent to ``A``. From 182a05896aa2dbd54f8264d31be0398671df21bf Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 14:14:16 -0600 Subject: [PATCH 19/45] a few more review comments --- docs/spec/concepts.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index daceed39..f3dc9590 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -13,7 +13,7 @@ and verifies that their uses obey the typing rules. Normally, a program that is not well typed (i.e., one that contains a type error) will not run. Java and C++ are examples of statically typed object-oriented languages. -A **dynamically typed** programming language does not run a type-checker before +A **dynamically typed** programming language does not run a type checker before running a program. Instead, it checks 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 @@ -85,7 +85,7 @@ An expression typed as :ref:`Any`, on the other hand, should be assumed to have _some_ specific static type, but _which_ static type is not known. A static type checker should not emit static type errors on an expression or statement if :ref:`Any` might represent a static type which would avoid the error. (This -intuition is made more precise below, in our definitions of materialization and +is defined more precisely below, in terms of materialization and assignability.) Similarly, a gradual type such as ``tuple[int, Any]`` (see :ref:`tuples`) or @@ -96,7 +96,7 @@ values. In the same way that ``Any`` does not represent "the set of all Python objects" but rather "an unknown set of objects", ``tuple[int, Any]`` does not represent "the set of all length-two tuples whose first element is an integer." That is a -fully static type, spelled ``tuple[int, object]``. In contrast, ``tuple[int, +fully static type, spelled ``tuple[int, object]``. By contrast, ``tuple[int, Any]`` represents some unknown set of tuple values; it might be the set of all tuples of two integers, or the set of all tuples of an integer and a string, or some other set of tuple values. @@ -246,7 +246,7 @@ names, pass them to functions, or return them from functions. We can also get/set attributes and call methods. In the Python object model, the operations that can be performed on a value all -de-sugar to method calls. For example, ``a + b`` is (roughly, eliding some +desugar to method calls. For example, ``a + b`` is (roughly, eliding some details) syntactic sugar for either ``type(a).__add__(a, b)`` or ``type(b).__radd__(b, a)``. From 351136e69651725b2687c13bb423e6a8556803ec Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 15:22:55 -0600 Subject: [PATCH 20/45] add terms to glossary --- docs/spec/concepts.rst | 4 ++- docs/spec/glossary.rst | 78 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 1 deletion(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index f3dc9590..c924fefa 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -168,7 +168,9 @@ relation. Materialization transforms a "more dynamic" type to a "more static" type. Given a gradual type ``A``, if we replace zero or more occurrences of ``Any`` in ``A`` with some gradual type (which can be different for each occurrence of ``Any``), the resulting gradual type ``B`` is a materialization -of ``A``. +of ``A``. (We can also materialize a :ref:`Callable` type by replacing ``...`` +with a bracketed list of types, and materialize ``tuple[Any, ...]`` by +replacing it with a determinate-length tuple type.) For instance, ``tuple[int, str]`` (a fully static type) and ``tuple[Any, str]`` (a gradual type) are both materializations of ``tuple[Any, Any]``. ``tuple[int, diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 3c8314d7..3cd03321 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -12,15 +12,77 @@ This section defines a few terms that may be used elsewhere in the specification :term:`type expression`, sometimes with additional :term:`type qualifiers `. See :ref:`"Type and annotation expression" ` for details. + assignable + If a type ``B`` is "assignable to" a type ``A``, a type checker should + not error on the assignment ``x: A = b``, where ``b`` is some expression + whose type is ``B``. Similarly for function calls and returns: ``f(b)`` + where ``def f(x: A): ...`` and ``return b`` inside ``def f(...) -> A:`` + are both valid (not a type error) if and only if ``B`` is assignable to + ``A``. In this case ``A`` is "assignable from" ``B``. For :term:`fully + static types `, "assignable to" is equivalent to + ":term:`subtype` of" and "assignable from" is equivalent to + ":term:`supertype` of". For :term:`gradual types `, a type + ``B`` is assignable to a type ``A`` if there exist :term:`fully static + ` :term:`materializations ` ``A'`` and + ``B'`` of ``A`` and ``B``, respectively, such that ``B'`` is a + :term:`subtype` of ``A'``. See :ref:`type-system-concepts`. + + consistent + Two :term:`fully static types ` are "consistent with" + each other if they are the same type. Two gradual types are "consistent + with" each other if they could :term:`materialize` to the same type. See + :ref:`type-system-concepts`. + + consistent subtype + "Consistent subtype" is synonymous with ":term:`assignable` to" (and + "consistent supertype" is synonymous with ":term:`assignable` from"). See + :ref:`type-system-concepts`. + distribution The packaged file which is used to publish and distribute a release. (:pep:`426`) + fully static type + A type is "fully static" if it does not contain any :term:`gradual form`. + Fully static types represent a set of possible runtime values. Fully + static types participate in the :term:`subtype` relation. See + :ref:`type-system-concepts`. + + gradual form + A gradual form is a :term:`type expression` which makes the type it is + part of not a :term:`fully static type`, but rather represent a set of + possible static types. See :ref:`type-system-concepts`. The 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 ` types.) + + gradual type + Types in the Python type system are "gradual types". A gradual type may + be a :term:`fully static type`, or it may be :ref:`Any`, or a type that + contains :ref:`Any` or another :term:`gradual form`. Unlike :term:`fully + static types `, gradual types do not necessarily + represent a single set of possible runtime values; instead they represent + a set of possible static types. Gradual types do not participate in the + :term:`subtype` relation, but they do participate in :term:`consistency + ` and :term:`assignability `. They can be + :term:`materialized ` to a fully static type. See + :ref:`type-system-concepts`. + inline Inline type annotations are annotations that are included in the runtime code using :pep:`526` and :pep:`3107` syntax (the filename ends in ``.py``). + materialize + A :term:`gradual type` can be materialized to a more static type + (possibly a :term:`fully static type`) by replacing :ref:`Any` with a + type, or by replacing the `...` in a :ref:`Callable` type with a list of + types, or by replacing ``tuple[Any, ...]`` with a specific-length tuple + type. This materialization relation is key to defining + :term:`assignability ` for gradual types. See + :ref:`type-system-concepts`. + module A file containing Python runtime code or stubbed type information. @@ -42,6 +104,22 @@ This section defines a few terms that may be used elsewhere in the specification A file containing only type information, empty of runtime code (the filename ends in ``.pyi``). See :ref:`stub-files`. + subtype + A :term:`fully static type` ``B`` is a subtype of a :term:`fully static + type` ``A`` if and only if the set of possible runtime values represented + by ``B`` is a subset of the set of possible runtime values represented by + ``A``. For nominal types (classes), subtyping is defined by inheritance. + For structural types (see :ref:`Protocols`), subtyping is defined by a + shared set of attributes and methods. Subtype is the inverse of + :term:`supertype`. See :ref:`type-system-concepts`. + + supertype + A :term:`fully static type` ``A`` is a supertype of a :term:`fully static + type` ``B`` if and only if the set of possible runtime values represented + by ``A`` is a superset of the set of possible runtime values represented + by ``B``. Supertype is the inverse of :term:`subtype`. See + :ref:`type-system-concepts`. + type expression An expression that represents a type. The type system requires the use of type expressions within :term:`annotation expression` and also in several other contexts. From cd03de8971c62e299aac3510d9ed480cdefa4367 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 18:11:19 -0600 Subject: [PATCH 21/45] Update glossary.rst Co-authored-by: Jelle Zijlstra --- docs/spec/glossary.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 3cd03321..6a5fc296 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -55,7 +55,7 @@ This section defines a few terms that may be used elsewhere in the specification 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 ` types.) + other :ref:`tuple ` types). gradual type Types in the Python type system are "gradual types". A gradual type may From 07941d7a002af2fba22b0bc48e8b36035911e6c0 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 18:14:44 -0600 Subject: [PATCH 22/45] Update glossary.rst Co-authored-by: Alex Waygood --- docs/spec/glossary.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 6a5fc296..0e9232c8 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -58,7 +58,7 @@ This section defines a few terms that may be used elsewhere in the specification other :ref:`tuple ` types). gradual type - Types in the Python type system are "gradual types". A gradual type may + 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 :ref:`Any` or another :term:`gradual form`. Unlike :term:`fully static types `, gradual types do not necessarily From c55d40ae5f165e5eee18b6413d0df289add5b3b9 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 18:46:25 -0600 Subject: [PATCH 23/45] review comments on glossary --- docs/spec/glossary.rst | 53 +++++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 0e9232c8..39c5e5f4 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -22,16 +22,17 @@ This section defines a few terms that may be used elsewhere in the specification static types `, "assignable to" is equivalent to ":term:`subtype` of" and "assignable from" is equivalent to ":term:`supertype` of". For :term:`gradual types `, a type - ``B`` is assignable to a type ``A`` if there exist :term:`fully static - ` :term:`materializations ` ``A'`` and - ``B'`` of ``A`` and ``B``, respectively, such that ``B'`` is a - :term:`subtype` of ``A'``. See :ref:`type-system-concepts`. + ``B`` is assignable to a type ``A`` if there exist fully static + :term:`materializations ` ``A'`` and ``B'`` of ``A`` and + ``B``, respectively, such that ``B'`` is a subtype of ``A'``. See + :ref:`type-system-concepts`. consistent Two :term:`fully static types ` are "consistent with" each other if they are the same type. Two gradual types are "consistent with" each other if they could :term:`materialize` to the same type. See - :ref:`type-system-concepts`. + :ref:`type-system-concepts`. If two types are consistent, they are both + :term:`assignable` to and from each other. consistent subtype "Consistent subtype" is synonymous with ":term:`assignable` to" (and @@ -50,24 +51,24 @@ This section defines a few terms that may be used elsewhere in the specification gradual form A gradual form is a :term:`type expression` which makes the type it is - part of not a :term:`fully static type`, but rather represent a set of - possible static types. See :ref:`type-system-concepts`. The 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 + part of not a :term:`fully static type`, but rather a representation of a + set of possible static types. See :ref:`type-system-concepts`. The + 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 ` types). gradual type - Types in the Python type system are "gradual". A gradual type may + Types in the Python type system are "gradual types". A gradual type may be a :term:`fully static type`, or it may be :ref:`Any`, or a type that - contains :ref:`Any` or another :term:`gradual form`. Unlike :term:`fully - static types `, gradual types do not necessarily - represent a single set of possible runtime values; instead they represent - a set of possible static types. Gradual types do not participate in the + 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 ` and :term:`assignability `. They can be - :term:`materialized ` to a fully static type. See - :ref:`type-system-concepts`. + :term:`materialized ` to a more static, or fully static, + type. See :ref:`type-system-concepts`. inline Inline type annotations are annotations that are included in the @@ -105,19 +106,19 @@ This section defines a few terms that may be used elsewhere in the specification (the filename ends in ``.pyi``). See :ref:`stub-files`. subtype - A :term:`fully static type` ``B`` is a subtype of a :term:`fully static - type` ``A`` if and only if the set of possible runtime values represented - by ``B`` is a subset of the set of possible runtime values represented by + A :term:`fully static type` ``B`` is a subtype of a fully static type + ``A`` if and only if the set of possible runtime values represented by + ``B`` is a subset of the set of possible runtime values represented by ``A``. For nominal types (classes), subtyping is defined by inheritance. - For structural types (see :ref:`Protocols`), subtyping is defined by a - shared set of attributes and methods. Subtype is the inverse of - :term:`supertype`. See :ref:`type-system-concepts`. + For structural types (see :ref:`Protocols`, :ref:`TypedDict`), subtyping + is defined by a shared set of attributes/methods or keys. Subtype is the + inverse of :term:`supertype`. See :ref:`type-system-concepts`. supertype - A :term:`fully static type` ``A`` is a supertype of a :term:`fully static - type` ``B`` if and only if the set of possible runtime values represented - by ``A`` is a superset of the set of possible runtime values represented - by ``B``. Supertype is the inverse of :term:`subtype`. See + A :term:`fully static type` ``A`` is a supertype of a fully static type + ``B`` if and only if the set of possible runtime values represented by + ``A`` is a superset of the set of possible runtime values represented by + ``B``. Supertype is the inverse of :term:`subtype`. See :ref:`type-system-concepts`. type expression From b1775b16eacb8b25b5b88e01164d95e23ae55ace Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 19:10:05 -0600 Subject: [PATCH 24/45] re-apply review comment --- docs/spec/glossary.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 39c5e5f4..7d90ee2a 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -59,8 +59,8 @@ This section defines a few terms that may be used elsewhere in the specification other :ref:`tuple ` types). gradual type - Types in the Python type system are "gradual types". A gradual type may - be a :term:`fully static type`, or it may be :ref:`Any`, or a type that + 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 From 1a71a7296b72256767daa9377f3fe052ab62c6fe Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 19:18:07 -0600 Subject: [PATCH 25/45] Apply suggestions from code review Co-authored-by: Alex Waygood --- docs/spec/glossary.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 7d90ee2a..c94259d6 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -36,7 +36,7 @@ This section defines a few terms that may be used elsewhere in the specification consistent subtype "Consistent subtype" is synonymous with ":term:`assignable` to" (and - "consistent supertype" is synonymous with ":term:`assignable` from"). See + "consistent supertype" is synonymous with "assignable from"). See :ref:`type-system-concepts`. distribution @@ -53,7 +53,7 @@ This section defines a few terms that may be used elsewhere in the specification A gradual form is a :term:`type expression` which makes the type it is part of not a :term:`fully static type`, but rather a representation of a set of possible static types. See :ref:`type-system-concepts`. The - primary gradual form is :ref:`Any`. The ellipsis (`...`) is a gradual + 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 ` types). @@ -64,7 +64,7 @@ This section defines a few terms that may be used elsewhere in the specification 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 + possible runtime values). Gradual types do not participate in the :term:`subtype` relation, but they do participate in :term:`consistency ` and :term:`assignability `. They can be :term:`materialized ` to a more static, or fully static, From c18d9e168cd597731d6244436d5e3c4749465737 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 19:32:50 -0600 Subject: [PATCH 26/45] audit remainder of type spec for terminology usage --- docs/spec/annotations.rst | 12 ++-- docs/spec/callables.rst | 135 ++++++++++++++++++------------------ docs/spec/class-compat.rst | 7 +- docs/spec/concepts.rst | 8 +++ docs/spec/constructors.rst | 15 ++-- docs/spec/directives.rst | 6 -- docs/spec/generics.rst | 70 +++++++++---------- docs/spec/literal.rst | 40 +++++------ docs/spec/namedtuples.rst | 9 +-- docs/spec/narrowing.rst | 7 +- docs/spec/protocol.rst | 101 +++++++++++++-------------- docs/spec/qualifiers.rst | 2 +- docs/spec/special-types.rst | 8 ++- docs/spec/tuples.rst | 13 ++-- docs/spec/typeddict.rst | 38 ++++------ 15 files changed, 232 insertions(+), 239 deletions(-) diff --git a/docs/spec/annotations.rst b/docs/spec/annotations.rst index 0b0ce641..4ebfd01b 100644 --- a/docs/spec/annotations.rst +++ b/docs/spec/annotations.rst @@ -16,13 +16,17 @@ hinting is used by filling function annotation slots with classes:: This states that the expected type of the ``name`` argument is ``str``. Analogically, the expected return type is ``str``. -Expressions whose type is a subtype of a specific argument type are -also accepted for that argument. +Expressions whose type is :term:`assignable` to a specific argument type are +also accepted for that argument. Similarly, an expression whose type is +assignable to the annotated return type can be returned from the function. .. _`missing-annotations`: -Any function without annotations should be treated as having the most -general type possible, or ignored, by any type checker. +Any function without annotations should be treated as having :ref:`Any` +annotations on all arguments and the return type. + +Type checkers may choose to entirely ignore (not type check) the bodies of +functions with no annotations, but this behavior is not required. It is recommended but not required that checked functions have annotations for all arguments and the return type. For a checked diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index 3ec63bfa..bc9c5396 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -71,8 +71,8 @@ may be given as an ellipsis. For example:: def func(x: AnyStr, y: AnyStr = ...) -> AnyStr: ... If a non-ellipsis default value is present and its type can be statically -evaluated, a type checker should verify that this type is compatible with the -declared parameter's type:: +evaluated, a type checker should verify that this type is :term:`assignable` to +the declared parameter's type:: def func(x: int = 0): ... # OK def func(x: int | None = None): ... # OK @@ -282,8 +282,8 @@ unpacked in the destination callable invocation:: dest = src # WRONG! dest(**animal) # Fails at runtime. -Similar situation can happen even without inheritance as compatibility -between ``TypedDict``\s is based on structural subtyping. +A similar situation can happen even without inheritance as :term:`assignability +` between ``TypedDict``\s is structural. Source contains untyped ``**kwargs`` """""""""""""""""""""""""""""""""""" @@ -423,11 +423,9 @@ the section on `Callback protocols`_. Meaning of ``...`` in ``Callable`` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The ``Callable`` special form supports the use of ``...`` in place of the -list of parameter types. This indicates that the type is consistent with -any input signature. Just as ``Any`` means "any conceivable type that could be -compatible", ``(...)`` means "any conceivable set of parameters that could be -compatible":: +The ``Callable`` special form supports the use of ``...`` in place of the list +of parameter types. This is a :term:`gradual form` indicating that the type is +:term:`consistent` with any input signature:: cb1: Callable[..., str] cb1 = lambda x: str(x) # OK @@ -475,7 +473,7 @@ and are retained as part of the signature:: pass class B(A): - # This override is OK because it is consistent with the parent's method. + # This override is OK because it is assignable to the parent's method. def method(self, a: float, /, b: int, *, k: str, m: str) -> None: pass @@ -490,7 +488,7 @@ For example:: f: Callback[...] = cb # OK If ``...`` is used with signature concatenation, the ``...`` portion continues -to mean "any conceivable set of parameters that could be compatible":: +to be :term:`consistent` with any input parameters:: type CallbackWithInt[**P] = Callable[Concatenate[int, P], str] type CallbackWithStr[**P] = Callable[Concatenate[str, P], str] @@ -522,21 +520,21 @@ and overloads. They can be defined as protocols with a ``__call__`` member:: ... comb: Combiner = good_cb # OK - comb = bad_cb # Error! Argument 2 has incompatible type because of + comb = bad_cb # Error! Argument 2 is not assignable because of # different parameter name and kind in the callback Callback protocols and ``Callable[...]`` types can generally be used interchangeably. -Subtyping rules for callables ------------------------------ +Assignability rules for callables +--------------------------------- -A callable type ``A`` is a subtype of callable type ``B`` if the return type -of ``A`` is a subtype of the return type of ``B`` and the input signature -of ``A`` accepts all possible combinations of arguments that the input -signature of ``B`` accepts. All of the specific subtyping rules described below -derive from this general rule. +A callable type ``B`` is :term:`assignable` to callable type ``A`` if the +return type of ``B`` is assignable to the return type of ``A`` and the input +signature of ``B`` accepts all possible combinations of arguments that the +input signature of ``A`` accepts. All of the specific assignability rules +described below derive from this general rule. Parameter types @@ -544,9 +542,9 @@ Parameter types Callable types are covariant with respect to their return types but contravariant with respect to their parameter types. This means a callable -``A`` is a subtype of callable ``B`` if the types of the parameters of -``B`` are subtypes of the parameters of ``A``. For example, -``(x: float) -> int`` is a subtype of ``(x: int) -> float``:: +``B`` is assignable to callable ``A`` if the types of the parameters of +``A`` are assignable to the parameters of ``B``. For example, +``(x: float) -> int`` is assignable to ``(x: int) -> float``:: def func(cb: Callable[[float], int]): f1: Callable[[int], float] = cb # OK @@ -555,11 +553,11 @@ contravariant with respect to their parameter types. This means a callable Parameter kinds ^^^^^^^^^^^^^^^ -Callable ``A`` is a subtype of callable ``B`` if all keyword-only parameters -in ``B`` are present in ``A`` as either keyword-only parameters or standard -(positional or keyword) parameters. For example, ``(a: int) -> None`` is a -subtype of ``(*, a: int) -> None``, but the converse is not true. The order -of keyword-only parameters is ignored for purposes of subtyping:: +Callable ``B`` is assignable to callable ``A`` only if all keyword-only +parameters in ``A`` are present in ``B`` as either keyword-only parameters or +standard (positional or keyword) parameters. For example, ``(a: int) -> None`` +is assignable to ``(*, a: int) -> None``, but the converse is not true. The +order of keyword-only parameters is ignored for purposes of assignability:: class KwOnly(Protocol): def __call__(self, *, b: int, a: int) -> None: ... @@ -571,10 +569,10 @@ of keyword-only parameters is ignored for purposes of subtyping:: f1: KwOnly = standard # OK f2: Standard = kw_only # Error -Likewise, callable ``A`` is a subtype of callable ``B`` if all positional-only -parameters in ``B`` are present in ``A`` as either positional-only parameters -or standard (positional or keyword) parameters. The names of positional-only -parameters are ignored for purposes of subtyping:: +Likewise, callable ``B`` is assignable to callable ``A`` only if all +positional-only parameters in ``A`` are present in ``B`` as either +positional-only parameters or standard (positional or keyword) parameters. The +names of positional-only parameters are ignored for purposes of assignability:: class PosOnly(Protocol): def __call__(self, not_a: int, /) -> None: ... @@ -590,9 +588,9 @@ parameters are ignored for purposes of subtyping:: ``*args`` parameters ^^^^^^^^^^^^^^^^^^^^ -If a callable ``B`` has a signature with a ``*args`` parameter, callable ``A`` -must also have a ``*args`` parameter to be a subtype of ``B``, and the type of -``B``'s ``*args`` parameter must be a subtype of ``A``'s ``*args`` parameter:: +If a callable ``A`` has a signature with a ``*args`` parameter, callable ``B`` +must also have a ``*args`` parameter to be assignable to ``A``, and the type of +``A``'s ``*args`` parameter must be assignable to ``B``'s ``*args`` parameter:: class NoArgs(Protocol): def __call__(self) -> None: ... @@ -611,12 +609,12 @@ must also have a ``*args`` parameter to be a subtype of ``B``, and the type of f4: IntArgs = float_args # OK f5: FloatArgs = no_args # Error: missing *args parameter - f6: FloatArgs = int_args # Error: float is not subtype of int + f6: FloatArgs = int_args # Error: float is not assignable to int -If a callable ``B`` has a signature with one or more positional-only parameters, -a callable ``A`` is a subtype of ``B`` if ``A`` has an ``*args`` parameter whose -type is a supertype of the types of any otherwise-unmatched positional-only -parameters in ``B``:: +If a callable ``A`` has a signature with one or more positional-only +parameters, a callable ``B`` is assignable to ``A`` only if ``B`` has an +``*args`` parameter whose type is assignable from the types of any +otherwise-unmatched positional-only parameters in ``A``:: class PosOnly(Protocol): def __call__(self, a: int, b: str, /) -> None: ... @@ -634,15 +632,15 @@ parameters in ``B``:: def __call__(self, a: int, b: str) -> None: ... def func(int_args: IntArgs, int_str_args: IntStrArgs, str_args: StrArgs): - f1: PosOnly = int_args # Error: str is not subtype of int + f1: PosOnly = int_args # Error: str is not assignable to int f2: PosOnly = int_str_args # OK f3: PosOnly = str_args # OK - f4: IntStrArgs = str_args # Error: int | str is not subtype of str - f5: IntStrArgs = int_args # Error: int | str is not subtype of int + f4: IntStrArgs = str_args # Error: int | str is not assignable to str + f5: IntStrArgs = int_args # Error: int | str is not assignable to int f6: StrArgs = int_str_args # OK - f7: StrArgs = int_args # Error: str is not subtype of int + f7: StrArgs = int_args # Error: str is not assignable to int f8: IntArgs = int_str_args # OK - f9: IntArgs = str_args # Error: int is not subtype of str + f9: IntArgs = str_args # Error: int is not assignable to str f10: Standard = int_str_args # Error: keyword parameters a and b missing f11: Standard = str_args # Error: keyword parameter b missing @@ -650,10 +648,10 @@ parameters in ``B``:: ``**kwargs`` parameters ^^^^^^^^^^^^^^^^^^^^^^^ -If a callable ``B`` has a signature with a ``**kwargs`` parameter (without -an unpacked ``TypedDict`` type annotation), callable ``A`` must also have a -``**kwargs`` parameter to be a subtype of ``B``, and the type of -``B``'s ``**kwargs`` parameter must be a subtype of ``A``'s ``**kwargs`` +If a callable ``A`` has a signature with a ``**kwargs`` parameter (without +an unpacked ``TypedDict`` type annotation), callable ``B`` must also have a +``**kwargs`` parameter to be assignable to ``A``, and the type of +``A``'s ``**kwargs`` parameter must be assignable to ``B``'s ``**kwargs`` parameter:: class NoKwargs(Protocol): @@ -673,12 +671,12 @@ parameter:: f4: IntKwargs = float_kwargs # OK f5: FloatKwargs = no_kwargs # Error: missing **kwargs parameter - f6: FloatKwargs = int_kwargs # Error: float is not subtype of int + f6: FloatKwargs = int_kwargs # Error: float is not assignable to int -If a callable ``B`` has a signature with one or more keyword-only parameters, -a callable ``A`` is a subtype of ``B`` if ``A`` has a ``**kwargs`` parameter -whose type is a supertype of the types of any otherwise-unmatched keyword-only -parameters in ``B``:: +If a callable ``A`` has a signature with one or more keyword-only parameters, +a callable ``B`` is assignable to ``A`` if ``B`` has a ``**kwargs`` parameter +whose type is assignable from the types of any otherwise-unmatched keyword-only +parameters in ``A``:: class KwOnly(Protocol): def __call__(self, *, a: int, b: str) -> None: ... @@ -696,19 +694,19 @@ parameters in ``B``:: def __call__(self, a: int, b: str) -> None: ... def func(int_kwargs: IntKwargs, int_str_kwargs: IntStrKwargs, str_kwargs: StrKwargs): - f1: KwOnly = int_kwargs # Error: str is not subtype of int + f1: KwOnly = int_kwargs # Error: str is not assignable to int f2: KwOnly = int_str_kwargs # OK f3: KwOnly = str_kwargs # OK - f4: IntStrKwargs = str_kwargs # Error: int | str is not subtype of str - f5: IntStrKwargs = int_kwargs # Error: int | str is not subtype of int + f4: IntStrKwargs = str_kwargs # Error: int | str is not assignable to str + f5: IntStrKwargs = int_kwargs # Error: int | str is not assignable to int f6: StrKwargs = int_str_kwargs # OK - f7: StrKwargs = int_kwargs # Error: str is not subtype of int + f7: StrKwargs = int_kwargs # Error: str is not assignable to int f8: IntKwargs = int_str_kwargs # OK - f9: IntKwargs = str_kwargs # Error: int is not subtype of str + f9: IntKwargs = str_kwargs # Error: int is not assignable to str f10: Standard = int_str_kwargs # Error: Does not accept positional arguments f11: Standard = str_kwargs # Error: Does not accept positional arguments -Subtyping relationships for callable signatures that contain a ``**kwargs`` +Assignability relationships for callable signatures that contain a ``**kwargs`` with an unpacked ``TypedDict`` are described in the section :ref:`above `. @@ -732,10 +730,10 @@ to a ``Callable`` parameterized by ``P``:: Default argument values ^^^^^^^^^^^^^^^^^^^^^^^ -If a callable ``A`` has a parameter ``x`` with a default argument value and -``B`` is the same as ``A`` except that ``x`` has no default argument, then -``A`` is a subtype of ``B``. ``A`` is also a subtype of ``C`` -if ``C`` is the same as ``A`` with parameter ``x`` removed:: +If a callable ``C`` has a parameter ``x`` with a default argument value and +``A`` is the same as ``C`` except that ``x`` has no default argument, then +``C`` is assignable to ``A``. ``C`` is also assignable to ``A`` +if ``A`` is the same as ``C`` with parameter ``x`` removed:: class DefaultArg(Protocol): def __call__(self, x: int = 0) -> None: ... @@ -754,9 +752,9 @@ if ``C`` is the same as ``A`` with parameter ``x`` removed:: Overloads ^^^^^^^^^ -If a callable ``A`` is overloaded with two or more signatures, it is a subtype -of callable ``B`` if *at least one* of the overloaded signatures in ``A`` is -a subtype of ``B``:: +If a callable ``B`` is overloaded with two or more signatures, it is assignable +to callable ``A`` if *at least one* of the overloaded signatures in ``B`` is +assignable to ``A``:: class Overloaded(Protocol): @overload @@ -778,8 +776,9 @@ a subtype of ``B``:: f2: StrArg = overloaded # OK f3: FloatArg = overloaded # Error -If a callable ``B`` is overloaded with two or more signatures, callable ``A`` -is a subtype of ``B`` if ``A`` is a subtype of *all* of the signatures in ``B``:: +If a callable ``A`` is overloaded with two or more signatures, callable ``B`` +is assignable to ``A`` if ``B`` is assignable to *all* of the signatures in +``A``:: class Overloaded(Protocol): @overload diff --git a/docs/spec/class-compat.rst b/docs/spec/class-compat.rst index b49a2034..c1f47ffb 100644 --- a/docs/spec/class-compat.rst +++ b/docs/spec/class-compat.rst @@ -1,6 +1,6 @@ .. _`class-compat`: -Class type compatibility +Class type assignability ======================== .. _`classvar`: @@ -97,8 +97,9 @@ annotated in ``__init__`` or other methods, rather than in the class:: (Originally specified by :pep:`698`.) When type checkers encounter a method decorated with ``@typing.override`` they -should treat it as a type error unless that method is overriding a compatible -method or attribute in some ancestor class. +should treat it as a type error unless that method is overriding a method or +attribute in some ancestor class, and the type of the overriding method is +assignable to the type of the overridden method. .. code-block:: python diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index c924fefa..7d2a48ff 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -66,6 +66,10 @@ or a class that inherits directly or indirectly from ``str``. A :ref:`Protocol ` denotes the set of all objects which share a certain set of attributes and/or methods. +If an object ``v`` is a member of the set of objects denoted by a fully static +type ``T``, we can say that ``v`` is a "member of" the type ``T``, or ``v`` +"inhabits" ``T``. + Gradual types ~~~~~~~~~~~~~ @@ -182,6 +186,8 @@ static" type than ``A``, and ``A`` is a "more dynamic" type than ``B``. The materialization relation is both transitive and reflexive, so it defines a preorder on gradual types. +.. _`consistent`: + Consistency ----------- @@ -208,6 +214,8 @@ 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 with ``A``. +.. _`assignable`: + The assignable-to (or consistent subtyping) relation ---------------------------------------------------- diff --git a/docs/spec/constructors.rst b/docs/spec/constructors.rst index 0eb34b84..547d736f 100644 --- a/docs/spec/constructors.rst +++ b/docs/spec/constructors.rst @@ -105,11 +105,11 @@ unrelated class. If the evaluated return type of ``__new__`` is not the class being constructed (or a subclass thereof), a type checker should assume that the ``__init__`` -method will not be called. This is consistent with the runtime behavior of -the ``type.__call__`` method. If the ``__new__`` method return type is -a union with one or more subtypes that are not instances of the class being -constructed (or a subclass thereof), a type checker should likewise assume that -the ``__init__`` method will not be called. +method will not be called. This is consistent with the runtime behavior of the +``type.__call__`` method. If the ``__new__`` method return type is a union with +one or more members that are not the class being constructed (or a subclass +thereof), a type checker should likewise assume that the ``__init__`` method +will not be called. :: @@ -337,7 +337,7 @@ Consistency of ``__new__`` and ``__init__`` ------------------------------------------- Type checkers may optionally validate that the ``__new__`` and ``__init__`` -methods for a class have consistent signatures. +methods for a class have :term:`consistent` signatures. :: @@ -353,7 +353,8 @@ methods for a class have consistent signatures. Converting a Constructor to Callable ------------------------------------ -Class objects are callable, which means they are compatible with callable types. +Class objects are callable, which means they are :term:`assignable` to callable +types. :: diff --git a/docs/spec/directives.rst b/docs/spec/directives.rst index 01c0f6bd..7fca698a 100644 --- a/docs/spec/directives.rst +++ b/docs/spec/directives.rst @@ -86,12 +86,6 @@ At runtime a cast always returns the expression unchanged -- it does not check the type, and it does not convert or coerce the value. -Casts differ from type comments (see the previous section). When using -a type comment, the type checker should still verify that the inferred -type is consistent with the stated type. When using a cast, the type -checker should blindly believe the programmer. Also, casts can be used -in expressions, while type comments only apply to assignments. - .. _`if-type-checking`: ``TYPE_CHECKING`` diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst index 53d8626f..b87641d9 100644 --- a/docs/spec/generics.rst +++ b/docs/spec/generics.rst @@ -479,7 +479,7 @@ using the ``TypeVar`` constructor) or using ``: `` (when using the native syntax for generics). The bound itself cannot be parameterized by type variables. This means that an actual type substituted (explicitly or implicitly) for the type variable must -be a subtype of the boundary type. Example:: +be :term:`assignable` to the boundary type. Example:: from typing import TypeVar from collections.abc import Sized @@ -496,11 +496,10 @@ be a subtype of the boundary type. Example:: longer({1}, {1, 2}) # ok, return type set[int] longer([1], {1, 2}) # ok, return type a supertype of list[int] and set[int] -An upper bound cannot be combined with type constraints (as used in -``AnyStr``, see the example earlier); type constraints cause the -inferred type to be *exactly* one of the constraint types, while an -upper bound just requires that the actual type is a subtype of the -boundary type. +An upper bound cannot be combined with type constraints (as used in ``AnyStr``, +see the example earlier); type constraints cause the inferred type to be +*exactly* one of the constraint types, while an upper bound just requires that +the actual type is :term:`assignable` to the boundary type. .. _`variance`: @@ -523,13 +522,12 @@ introduction to these concepts can be found on `Wikipedia `_ and in :pep:`483`; here we just show how to control a type checker's behavior. -By default generic types declared using the old ``TypeVar`` syntax -are considered *invariant* in all type variables, -which means that values for variables annotated with types like -``list[Employee]`` must exactly match the type annotation -- no subclasses or -superclasses of the type parameter (in this example ``Employee``) are -allowed. See below for the behavior when using the built-in generic syntax -in Python 3.12 and higher. +By default generic types declared using the old ``TypeVar`` syntax are +considered *invariant* in all type variables, which means that e.g. +``list[Manager]`` is neither a supertype nor a subtype of ``list[Employee]``. + +See below for the behavior when using the built-in generic syntax in Python +3.12 and higher. To facilitate the declaration of container types where covariant or contravariant type checking is acceptable, type variables accept keyword @@ -1926,7 +1924,7 @@ Using a type parameter from an outer scope as a default is not supported. Bound Rules ^^^^^^^^^^^ -``T1``'s bound must be a subtype of ``T2``'s bound. +``T1``'s bound must be a :term:`consistent subtype` of ``T2``'s bound. :: @@ -2023,8 +2021,8 @@ Using ``bound`` and ``default`` """"""""""""""""""""""""""""""" If both ``bound`` and ``default`` are passed, ``default`` must be a -subtype of ``bound``. If not, the type checker should generate an -error. +:term:`consistent subtype` of ``bound``. If not, the type checker should +generate an error. :: @@ -2268,7 +2266,8 @@ Use in Attribute Annotations ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Another use for ``Self`` is to annotate attributes. One example is where we -have a ``LinkedList`` whose elements must be subclasses of the current class. +have a ``LinkedList`` whose elements must be consistent subtypes of the current +class. :: @@ -2298,8 +2297,8 @@ constructions with subclasses: def ordinal_value(self) -> str: return as_ordinal(self.value) - # Should not be OK because LinkedList[int] is not a subclass of - # OrdinalLinkedList, # but the type checker allows it. + # Should not be OK because LinkedList[int] is not a consistent subtype of + # OrdinalLinkedList, but the type checker allows it. xs = OrdinalLinkedList(value=1, next=LinkedList[int](value=2)) if xs.next: @@ -2469,11 +2468,10 @@ See :pep:`PEP 544 <544#self-types-in-protocols>` for details on the behavior of TypeVars bound to protocols. -Checking a class for compatibility with a protocol: If a protocol uses -``Self`` in methods or attribute annotations, then a class ``Foo`` is -considered compatible with the protocol if its corresponding methods and -attribute annotations use either ``Self`` or ``Foo`` or any of ``Foo``’s -subclasses. See the examples below: +Checking a class for assignability to a protocol: If a protocol uses ``Self`` +in methods or attribute annotations, then a class ``Foo`` is assignable to the +protocol if its corresponding methods and attribute annotations use either +``Self`` or ``Foo`` or any of ``Foo``’s subclasses. See the examples below: :: @@ -2705,16 +2703,15 @@ by the ``TypeVar`` constructor call. No further inference is needed. 3. Create two specialized versions of the class. We'll refer to these as ``upper`` and ``lower`` specializations. In both of these specializations, replace all type parameters other than the one being inferred by a dummy type -instance (a concrete anonymous class that is type compatible with itself and -assumed to meet the bounds or constraints of the type parameter). In -the ``upper`` specialized class, specialize the target type parameter with -an ``object`` instance. This specialization ignores the type parameter's -upper bound or constraints. In the ``lower`` specialized class, specialize -the target type parameter with itself (i.e. the corresponding type argument -is the type parameter itself). - -4. Determine whether ``lower`` can be assigned to ``upper`` using normal type -compatibility rules. If so, the target type parameter is covariant. If not, +instance (a concrete anonymous class that is assumed to meet the bounds or +constraints of the type parameter). In the ``upper`` specialized class, +specialize the target type parameter with an ``object`` instance. This +specialization ignores the type parameter's upper bound or constraints. In the +``lower`` specialized class, specialize the target type parameter with itself +(i.e. the corresponding type argument is the type parameter itself). + +4. Determine whether ``lower`` can be assigned to ``upper`` using normal +assignability rules. If so, the target type parameter is covariant. If not, determine whether ``upper`` can be assigned to ``lower``. If so, the target type parameter is contravariant. If neither of these combinations are assignable, the target type parameter is invariant. @@ -2737,9 +2734,8 @@ To determine the variance of ``T1``, we specialize ``ClassA`` as follows: upper = ClassA[object, Dummy, Dummy] lower = ClassA[T1, Dummy, Dummy] -We find that ``upper`` is not assignable to ``lower`` using normal type -compatibility rules defined in :pep:`484`. Likewise, ``lower`` is not assignable -to ``upper``, so we conclude that ``T1`` is invariant. +We find that ``upper`` is not assignable to ``lower``. Likewise, ``lower`` is +not assignable to ``upper``, so we conclude that ``T1`` is invariant. To determine the variance of ``T2``, we specialize ``ClassA`` as follows: diff --git a/docs/spec/literal.rst b/docs/spec/literal.rst index d0ca618c..ac4552c0 100644 --- a/docs/spec/literal.rst +++ b/docs/spec/literal.rst @@ -24,9 +24,8 @@ concrete value. For example, if we define some variable ``foo`` to have type ``Literal[3]``, we are declaring that ``foo`` must be exactly equal to ``3`` and no other value. -Given some value ``v`` that is a member of type ``T``, the type -``Literal[v]`` shall be treated as a subtype of ``T``. For example, -``Literal[3]`` is a subtype of ``int``. +Given some value ``v`` that is a member of type ``T``, the type ``Literal[v]`` +is a subtype of ``T``. For example, ``Literal[3]`` is a subtype of ``int``. All methods from the parent type will be directly inherited by the literal type. So, if we have some variable ``foo`` of type ``Literal[3]`` @@ -304,13 +303,13 @@ special-casing. For example, programs like the following are type safe:: # Legal: Literal["foo"] is a subtype of str expects_str(var) -This also means non-Literal expressions in general should not automatically -be cast to Literal. For example:: +This also means non-Literal types in general are not assignable to Literal +types. For example:: def expects_literal(x: Literal["foo"]) -> None: ... def runner(my_str: str) -> None: - # ILLEGAL: str is not a subclass of Literal["foo"] + # ILLEGAL: str is not assignable to Literal["foo"] expects_literal(my_str) **Note:** If the user wants their API to support accepting both literals @@ -398,9 +397,8 @@ maintain backwards-compatibility. Interactions with generics """""""""""""""""""""""""" -Types like ``Literal[3]`` are meant to be just plain old subclasses of -``int``. This means you can use types like ``Literal[3]`` anywhere -you could use normal types, such as with generics. +Since a type like ``Literal[3]`` is a subtype of ``int``, you can use +``Literal[3]`` anywhere you could use ``int``, such as with generics. This means that it is legal to parameterize generic functions or classes using Literal types:: @@ -584,7 +582,7 @@ Type inference Inferring ``LiteralString`` """"""""""""""""""""""""""" -Any literal string type is compatible with ``LiteralString``. For +Any literal string type is assignable to ``LiteralString``. For example, ``x: LiteralString = "foo"`` is valid because ``"foo"`` is inferred to be of type ``Literal["foo"]``. @@ -592,20 +590,20 @@ We also infer ``LiteralString`` in the following cases: + Addition: ``x + y`` is of type ``LiteralString`` if both ``x`` and - ``y`` are compatible with ``LiteralString``. + ``y`` are assignable to ``LiteralString``. + Joining: ``sep.join(xs)`` is of type ``LiteralString`` if ``sep``'s - type is compatible with ``LiteralString`` and ``xs``'s type is - compatible with ``Iterable[LiteralString]``. + type is assignable to ``LiteralString`` and ``xs``'s type is + assignable to ``Iterable[LiteralString]``. + In-place addition: If ``s`` has type ``LiteralString`` and ``x`` has - type compatible with ``LiteralString``, then ``s += x`` preserves + type assignable to ``LiteralString``, then ``s += x`` preserves ``s``'s type as ``LiteralString``. -+ String formatting: An f-string has type ``LiteralString`` if and only - if its constituent expressions are literal strings. ``s.format(...)`` - has type ``LiteralString`` if and only if ``s`` and the arguments have - types compatible with ``LiteralString``. ++ String formatting: An f-string has type ``LiteralString`` if and only if its + constituent expressions are literal strings. ``s.format(...)`` is assignable + to ``LiteralString`` if and only if ``s`` and the arguments have types + assignable to ``LiteralString``. In all other cases, if one or more of the composed values has a non-literal type ``str``, the composition of types will have type @@ -613,7 +611,7 @@ non-literal type ``str``, the composition of types will have type has type ``str``. This matches the pre-existing behavior of type checkers. -``LiteralString`` is compatible with the type ``str``. It inherits all +``LiteralString`` is assignable to the type ``str``. It inherits all methods from ``str``. So, if we have a variable ``s`` of type ``LiteralString``, it is safe to write ``s.startswith("hello")``. @@ -626,7 +624,7 @@ check: if s == "bar": reveal_type(s) # => Literal["bar"] -Such a refined type in the if-block is also compatible with +Such a refined type in the if-block is also assignable to ``LiteralString`` because its type is ``Literal["bar"]``. @@ -699,7 +697,7 @@ Format strings using literal strings: expect_literal_string("hello {}".format(username)) # Not OK -Other literal types, such as literal integers, are not compatible with ``LiteralString``: +Other literal types, such as literal integers, are not assignable to ``LiteralString``: :: diff --git a/docs/spec/namedtuples.rst b/docs/spec/namedtuples.rst index 835d196f..1ac14136 100644 --- a/docs/spec/namedtuples.rst +++ b/docs/spec/namedtuples.rst @@ -133,11 +133,12 @@ this:: x, y = p # Type error (too few values to unpack) -Type Compatibility Rules ------------------------- +Assignability +------------- -A named tuple is a subtype of a ``tuple`` with a known length and parameterized -by types corresponding to the named tuple's individual field types:: +A named tuple is :term:`assignable` to a ``tuple`` with a known length and +parameterized by types corresponding to the named tuple's individual field +types:: p = Point(x=1, y=2, units="inches") v1: tuple[int, int, str] = p # OK diff --git a/docs/spec/narrowing.rst b/docs/spec/narrowing.rst index cbab74f0..b7c6cc0d 100644 --- a/docs/spec/narrowing.rst +++ b/docs/spec/narrowing.rst @@ -149,8 +149,8 @@ To specify the behavior of ``TypeIs``, we use the following terminology: else: assert_type(val, NN) -The return type ``R`` must be consistent with ``I``. The type checker should -emit an error if this condition is not met. +The return type ``R`` must be :term:`assignable` to ``I``. The type checker +should emit an error if this condition is not met. Formally, type *NP* should be narrowed to :math:`A \land R`, the intersection of *A* and *R*, and type *NN* should be narrowed to @@ -193,7 +193,8 @@ argument's previously-known type:: else: assert_type(x, int) -It is an error to narrow to a type that is not consistent with the input type:: +It is an error to narrow to a type that is not :term:`assignable` to the input +type:: from typing import TypeIs diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index 5532276f..e6b39ad8 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -22,19 +22,17 @@ The distinction is not important most of the time, and in other cases we can just add a qualifier such as *protocol classes* when referring to the static type concept. -If a class includes a protocol in its MRO, the class is called -an *explicit* subclass of the protocol. If a class is a structural subtype -of a protocol, it is said to implement the protocol and to be compatible -with a protocol. If a class is compatible with a protocol but the protocol -is not included in the MRO, the class is an *implicit* subtype -of the protocol. (Note that one can explicitly subclass a protocol and -still not implement it if a protocol attribute is set to ``None`` -in the subclass, see Python :py:ref:`data model ` -for details.) - -The attributes (variables and methods) of a protocol that are mandatory -for another class in order to be considered a structural subtype are called -protocol members. +If a class includes a protocol in its MRO, the class is called an *explicit* +subclass of the protocol. If a class is a structural consistent subtype of a +protocol, it is said to implement the protocol and to be assignable to the +protocol. If a class is assignable to a protocol but the protocol is not +included in the MRO, the class is *implicitly* assignable to the protocol. +(Note that one can explicitly subclass a protocol and still not implement it if +a protocol attribute is set to ``None`` in the subclass, see Python +:py:ref:`data model ` for details.) + +The attributes (variables and methods) of a protocol that are mandatory for +another class to be assignable to the protocol are called protocol members. .. _protocol-definition: @@ -51,9 +49,9 @@ at the end of the list. Here is a simple example:: def close(self) -> None: ... -Now if one defines a class ``Resource`` with a ``close()`` method that has -a compatible signature, it would implicitly be a subtype of -``SupportsClose``, since the structural subtyping is used for +Now if one defines a class ``Resource`` with a ``close()`` method whose type +signature is assignable to ``SupportsClose.close``, it would implicitly be +assignable to ``SupportsClose``, since structural assignability is used for protocol types:: class Resource: @@ -74,10 +72,9 @@ be used in every context where normal types can:: close_all([f, r]) # OK! close_all([1]) # Error: 'int' has no 'close' method -Note that both the user-defined class ``Resource`` and the built-in -``IO`` type (the return type of ``open()``) are considered subtypes of -``SupportsClose``, because they provide a ``close()`` method with -a compatible type signature. +Note that both the user-defined class ``Resource`` and the built-in ``IO`` type +(the return type of ``open()``) are assignable to ``SupportsClose``, because +they provide a ``close()`` method with an assignable type signature. Protocol members @@ -147,9 +144,9 @@ expected to automatically detect that a class implements a given protocol. So while it's possible to subclass a protocol explicitly, it's *not necessary* to do so for the sake of type-checking. -The default implementations cannot be used if -the subtype relationship is implicit and only via structural -subtyping -- the semantics of inheritance is not changed. Examples:: +The default implementations cannot be used if the assignable-to relationship is +implicit and only structural -- the semantics of inheritance is not changed. +Examples:: class PColor(Protocol): @abstractmethod @@ -181,10 +178,10 @@ subtyping -- the semantics of inheritance is not changed. Examples:: represent(nice) # OK represent(another) # Also OK -Note that there is little difference between explicit and implicit +Note that there is little difference between explicit and implicit consistent subtypes; the main benefit of explicit subclassing is to get some protocol -methods "for free". In addition, type checkers can statically verify that -the class actually implements the protocol correctly:: +methods "for free". In addition, type checkers can statically verify that the +class actually implements the protocol correctly:: class RGB(Protocol): rgb: tuple[int, int, int] @@ -201,9 +198,9 @@ the class actually implements the protocol correctly:: A class can explicitly inherit from multiple protocols and also from normal classes. In this case methods are resolved using normal MRO and a type checker -verifies that all subtyping are correct. The semantics of ``@abstractmethod`` -is not changed; all of them must be implemented by an explicit subclass -before it can be instantiated. +verifies that all member assignability is correct. The semantics of +``@abstractmethod`` is not changed; all of them must be implemented by an +explicit subclass before it can be instantiated. Merging and extending protocols @@ -248,7 +245,7 @@ with ``typing.Sized``:: The two definitions of ``SizedAndClosable`` are equivalent. Subclass relationships between protocols are not meaningful when -considering subtyping, since structural compatibility is +considering assignability, since structural assignability is the criterion, not the MRO. If ``Protocol`` is included in the base class list, all the other base classes @@ -303,7 +300,7 @@ the declared variance. Examples:: var: Proto[float] another_var: Proto[int] - var = another_var # Error! 'Proto[float]' is incompatible with 'Proto[int]'. + var = another_var # Error! 'Proto[float]' is not assignable to 'Proto[int]'. Note that unlike nominal classes, de facto covariant protocols cannot be declared as invariant, since this can break transitivity of subtyping. @@ -328,7 +325,7 @@ like trees in an abstract fashion:: def leaves(self) -> Iterable['Traversable']: ... -Note that for recursive protocols, a class is considered a subtype of +Note that for recursive protocols, a class is considered assignable to the protocol in situations where the decision depends on itself. Continuing the previous example:: @@ -345,7 +342,7 @@ Continuing the previous example:: def walk(graph: Traversable) -> None: ... tree: Tree[float] = Tree() - walk(tree) # OK, 'Tree[float]' is a subtype of 'Traversable' + walk(tree) # OK, 'Tree[float]' is assignable to 'Traversable' Self-types in protocols @@ -371,26 +368,26 @@ The self-types in protocols follow the c = One() # OK c = Other() # Also OK -Subtyping relationships with other types -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Assignability relationships with other types +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Protocols cannot be instantiated, so there are no values whose runtime type is a protocol. For variables and parameters with protocol types, -subtyping relationships are subject to the following rules: +assignability relationships are subject to the following rules: -* A protocol is never a subtype of a concrete type. -* A concrete type ``X`` is a subtype of protocol ``P`` +* A protocol is never assignable to a concrete type. +* A concrete type ``X`` is assignable to a protocol ``P`` if and only if ``X`` implements all protocol members of ``P`` with - compatible types. In other words, subtyping with respect to a protocol is + assignable types. In other words, assignability with respect to a protocol is always structural. -* A protocol ``P1`` is a subtype of another protocol ``P2`` if ``P1`` defines - all protocol members of ``P2`` with compatible types. +* A protocol ``P1`` is assignable to another protocol ``P2`` if ``P1`` defines + all protocol members of ``P2`` with assignable types. Generic protocol types follow the same rules of variance as non-protocol types. Protocol types can be used in all contexts where any other types can be used, such as in unions, ``ClassVar``, type variables bounds, etc. Generic protocols follow the rules for generic abstract classes, except for -using structural compatibility instead of compatibility defined by +using structural assignability instead of assignability defined by inheritance relationships. Static type checkers will recognize protocol implementations, even if the @@ -460,8 +457,8 @@ Example:: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Variables and parameters annotated with ``type[Proto]`` accept only concrete -(non-protocol) subtypes of ``Proto``. The main reason for this is to allow -instantiation of parameters with such types. For example:: +(non-protocol) consistent subtypes of ``Proto``. The main reason for this is to +allow instantiation of parameters with such types. For example:: class Proto(Protocol): @abstractmethod @@ -489,7 +486,7 @@ For normal (non-abstract) classes, the behavior of ``type[]`` is not changed. A class object is considered an implementation of a protocol if accessing -all members on it results in types compatible with the protocol members. +all members on it results in types assignable to the types of the protocol members. For example:: from typing import Any, Protocol @@ -538,7 +535,7 @@ Modules as implementations of protocols ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ A module object is accepted where a protocol is expected if the public -interface of the given module is compatible with the expected protocol. +interface of the given module is assignable to the expected protocol. For example:: # file default_config.py @@ -560,7 +557,7 @@ For example:: setup(default_config) # OK -To determine compatibility of module level functions, the ``self`` argument +To determine assignability of module level functions, the ``self`` argument of the corresponding protocol methods is dropped. For example:: # callbacks.py @@ -622,11 +619,11 @@ the risks for this feature, the following rules are applied. if it only contains methods as members (for example ``Sized``, ``Iterator``, etc). A protocol that contains at least one non-method member (like ``x: int``) is called a data protocol. -* *Unsafe overlap*: A type ``X`` is called unsafely overlapping with - a protocol ``P``, if ``X`` is not a subtype of ``P``, but it is a subtype - of the type erased version of ``P`` where all members have type ``Any``. - In addition, if at least one element of a union unsafely overlaps with - a protocol ``P``, then the whole union is unsafely overlapping with ``P``. +* *Unsafe overlap*: A type ``X`` is called unsafely overlapping with a protocol + ``P``, if ``X`` is not assignable to ``P``, but it is assignable to the type + erased version of ``P`` where all members have type ``Any``. In addition, if + at least one element of a union unsafely overlaps with a protocol ``P``, then + the whole union is unsafely overlapping with ``P``. **Specification**: diff --git a/docs/spec/qualifiers.rst b/docs/spec/qualifiers.rst index 49ec63f2..13cd842b 100644 --- a/docs/spec/qualifiers.rst +++ b/docs/spec/qualifiers.rst @@ -255,7 +255,7 @@ details of the syntax: V == Annotated[list[tuple[int, int]], MaxLen(10)] -* As with most :term:`special forms `, ``Annotated`` is not type compatible with +* As with most :term:`special forms `, ``Annotated`` is not assignable to ``type`` or ``type[T]``:: v1: type[int] = Annotated[int, ""] # Type error diff --git a/docs/spec/special-types.rst b/docs/spec/special-types.rst index 985ffeca..46e1f2bf 100644 --- a/docs/spec/special-types.rst +++ b/docs/spec/special-types.rst @@ -10,7 +10,8 @@ Special types in annotations ``Any`` represents an unknown static type. -Every type is assignable to ``Any``, and ``Any`` is assignable to every type. +Every type is :term:`assignable` to ``Any``, and ``Any`` is assignable to every +type. See :ref:`type-system-concepts` for more discussion of ``Any``. @@ -93,8 +94,9 @@ is unreachable and will behave accordingly:: ``Never`` --------- -Since Python 3.11, the ``typing`` module contains a :term:`special form` ``Never``. It -represents the bottom type, a type that has no members. +Since Python 3.11, the ``typing`` module contains a :term:`special form` +``Never``. It represents the bottom type, a type that represents the empty set +of Python objects. The ``Never`` type is equivalent to ``NoReturn``, which is discussed above. The ``NoReturn`` type is conventionally used in return annotations of diff --git a/docs/spec/tuples.rst b/docs/spec/tuples.rst index 4f04b914..1209cc02 100644 --- a/docs/spec/tuples.rst +++ b/docs/spec/tuples.rst @@ -29,10 +29,10 @@ Arbitrary-length homogeneous tuples are sometimes referred to as "unbounded tuples". Both of these terms appear within the typing spec, and they refer to the same concept. -The type ``tuple[Any, ...]`` is special in that it is bidirectionally -compatible with any tuple of any length. This is useful for gradual typing. -The type ``tuple`` (with no type arguments provided) is equivalent to -``tuple[Any, ...]``. +The type ``tuple[Any, ...]`` is special in that it is :term:`consistent` with +all tuple types, and :term:`assignable` to a tuple of any length. This is +useful for gradual typing. The type ``tuple`` (with no type arguments provided) +is equivalent to ``tuple[Any, ...]``. Arbitrary-length tuples have exactly two type arguments -- the type and an ellipsis. Any other tuple form that uses an ellipsis is invalid:: @@ -61,8 +61,7 @@ more elements of type ``str``. The type ``tuple[*tuple[int, ...]]`` is equivalent to ``tuple[int, ...]``. If an unpacked ``*tuple[Any, ...]`` is embedded within another tuple, that -portion of the tuple is bidirectionally type compatible with any tuple of -any length. +portion of the tuple is :term:`consistent` with any tuple of any length. Only one unbounded tuple can be used within another tuple:: @@ -100,7 +99,7 @@ to a union of tuples of different lengths. That means ``tuple[()]``, ``tuple[int, ...]``. The converse is not true; ``tuple[int, ...]`` is not a subtype of ``tuple[int]``. -The type ``tuple[Any, ...]`` is bidirectionally compatible with any tuple:: +The type ``tuple[Any, ...]`` is :term:`consistent` with any tuple:: def func(t1: tuple[int], t2: tuple[int, ...], t3: tuple[Any, ...]): v1: tuple[int, ...] = t1 # OK diff --git a/docs/spec/typeddict.rst b/docs/spec/typeddict.rst index 6d632655..2903c040 100644 --- a/docs/spec/typeddict.rst +++ b/docs/spec/typeddict.rst @@ -27,13 +27,13 @@ supported by ``typing.NamedTuple``. Other features include TypedDict inheritance and totality (specifying whether keys are required or not). -This section also provides a sketch of how a type checker is expected -to support type checking operations involving TypedDict objects. -Similar to :pep:`484`, this discussion is left somewhat vague on purpose, -to allow experimentation with a wide variety of different type -checking approaches. In particular, type compatibility should be -based on structural compatibility: a more specific TypedDict type can -be compatible with a smaller (more general) TypedDict type. +This section also provides a sketch of how a type checker is expected to +support type checking operations involving TypedDict objects. Similar to +:pep:`484`, this discussion is left somewhat vague on purpose, to allow +experimentation with a wide variety of different type checking approaches. In +particular, :term:`assignability ` should be structural: a more +specific TypedDict type can be assignable to a smaller (more general) +TypedDict type. Class-based Syntax @@ -284,24 +284,16 @@ refers to a dictionary object does not need to be supported, to simplify implementation. -Type Consistency -^^^^^^^^^^^^^^^^ +Assignability +^^^^^^^^^^^^^ -Informally speaking, *type consistency* is a generalization of the -is-subtype-of relation to support the ``Any`` type. It is defined -more formally in :pep:`483`. This section introduces the -new, non-trivial rules needed to support type consistency for -TypedDict types. +First, any TypedDict type is :term:`assignable` to ``Mapping[str, object]``. -First, any TypedDict type is consistent with ``Mapping[str, object]``. -Second, a TypedDict type ``A`` is consistent with TypedDict ``B`` if -``A`` is structurally compatible with ``B``. This is true if and only -if both of these conditions are satisfied: +Second, a TypedDict type ``B`` is :term:`assignable` to a TypedDict ``A`` if +and only if both of these conditions are satisfied: -* For each key in ``B``, ``A`` has the corresponding key and the - corresponding value type in ``A`` is consistent with the value type - in ``B``. For each key in ``B``, the value type in ``B`` is also - consistent with the corresponding value type in ``A``. +* For each key in ``A``, ``B`` has the corresponding key and the corresponding + value type in ``B`` is :term:`consistent` with the value type in ``A``. * For each required key in ``B``, the corresponding key is required in ``A``. For each non-required key in ``B``, the corresponding key @@ -323,7 +315,7 @@ Discussion: a['x'] = None b: B = {'x': 0} - f(b) # Type check error: 'B' not compatible with 'A' + f(b) # Type check error: 'B' not assignable to 'A' b['x'] + 1 # Runtime error: None + 1 * A TypedDict type with a required key is not consistent with a From cca3bcd2f4d200bdd93ea131b24554b45cd8b894 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 19:48:59 -0600 Subject: [PATCH 27/45] review comments --- docs/spec/concepts.rst | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 7d2a48ff..fddbdd9d 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -40,19 +40,19 @@ dynamically checked, via the Python runtime's usual dynamic checking. The Python type system also uses ``...`` within :ref:`Callable` types and within ``tuple[Any, ...]`` (see :ref:`tuples`) to indicate a statically unknown component of a type. The detailed rules for these usages are discussed in their -respective sections of the specification. +respective sections of the specification. Collectively, along with :ref:`Any`, +these are :term:`gradual forms `. This specification describes a gradual type system for Python. Fully static and gradual types ------------------------------ -We will refer to types that do not contain :ref:`Any` (or the ``...`` in -``Callable`` or ``tuple[Any, ...]``) as a sub-part as **fully static types**. +We will refer to types that do not contain a :term:`gradual form` as a sub-part +as **fully static types**. A **gradual type** can be a fully static type, :ref:`Any` itself, or a type -that contains :ref:`Any` (or the ``...`` in ``Callable`` or ``tuple[Any, -...]``) as a sub-part. +that contains a gradual form as a sub-part. Fully static types ~~~~~~~~~~~~~~~~~~ @@ -173,8 +173,8 @@ type. Given a gradual type ``A``, if we replace zero or more occurrences of ``Any`` in ``A`` with some gradual type (which can be different for each occurrence of ``Any``), the resulting gradual type ``B`` is a materialization of ``A``. (We can also materialize a :ref:`Callable` type by replacing ``...`` -with a bracketed list of types, and materialize ``tuple[Any, ...]`` by -replacing it with a determinate-length tuple type.) +with any type signature, and materialize ``tuple[Any, ...]`` by replacing it +with a determinate-length tuple type.) For instance, ``tuple[int, str]`` (a fully static type) and ``tuple[Any, str]`` (a gradual type) are both materializations of ``tuple[Any, Any]``. ``tuple[int, @@ -263,7 +263,7 @@ details) syntactic sugar for either ``type(a).__add__(a, b)`` or For a static type checker, accessing ``a.foo`` is a type error unless all possible objects in the set represented by the type of ``a`` have the ``foo`` attribute. (We consider an implementation of ``__getattr__`` to be a getter for -all attribute names, and similarly for ``__setattr__`` and ``__delattr__``). +all attribute names, and similarly for ``__setattr__`` and ``__delattr__``.) If all objects in the set represented by the fully static type ``A`` have a ``foo`` attribute, we can say that the type ``A`` has the ``foo`` attribute. From 3d6b40602de740c8d6878b9f2bdca14c0e81378e Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 20:12:43 -0600 Subject: [PATCH 28/45] some review comments --- docs/spec/generics.rst | 16 ++++++++-------- docs/spec/literal.rst | 5 ++--- docs/spec/protocol.rst | 15 ++++++++------- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst index b87641d9..f57beb95 100644 --- a/docs/spec/generics.rst +++ b/docs/spec/generics.rst @@ -474,12 +474,12 @@ classes without a metaclass conflict. Type variables with an upper bound ---------------------------------- -A type variable may specify an upper bound using ``bound=`` (when -using the ``TypeVar`` constructor) or using ``: `` (when using the native -syntax for generics). The bound itself cannot be parameterized by type variables. -This means that an -actual type substituted (explicitly or implicitly) for the type variable must -be :term:`assignable` to the boundary type. Example:: +A type variable may specify an upper bound using ``bound=`` (when using +the ``TypeVar`` constructor) or using ``: `` (when using the native +syntax for generics). The bound itself cannot be parameterized by type +variables. This means that an actual type substituted (explicitly or +implicitly) for the type variable must be :term:`assignable` to the bound. +Example:: from typing import TypeVar from collections.abc import Sized @@ -499,7 +499,7 @@ be :term:`assignable` to the boundary type. Example:: An upper bound cannot be combined with type constraints (as used in ``AnyStr``, see the example earlier); type constraints cause the inferred type to be *exactly* one of the constraint types, while an upper bound just requires that -the actual type is :term:`assignable` to the boundary type. +the actual type is :term:`assignable` to the bound. .. _`variance`: @@ -1924,7 +1924,7 @@ Using a type parameter from an outer scope as a default is not supported. Bound Rules ^^^^^^^^^^^ -``T1``'s bound must be a :term:`consistent subtype` of ``T2``'s bound. +``T1``'s bound must be :term:`assignable` to ``T2``'s bound. :: diff --git a/docs/spec/literal.rst b/docs/spec/literal.rst index ac4552c0..f9decdef 100644 --- a/docs/spec/literal.rst +++ b/docs/spec/literal.rst @@ -397,10 +397,9 @@ maintain backwards-compatibility. Interactions with generics """""""""""""""""""""""""" -Since a type like ``Literal[3]`` is a subtype of ``int``, you can use -``Literal[3]`` anywhere you could use ``int``, such as with generics. +Literal types are types, and can be used anywhere a type is expected. -This means that it is legal to parameterize generic functions or +For example, it is legal to parameterize generic functions or classes using Literal types:: A = TypeVar('A', bound=int) diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index e6b39ad8..0220361b 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -23,13 +23,14 @@ cases we can just add a qualifier such as *protocol classes* when referring to the static type concept. If a class includes a protocol in its MRO, the class is called an *explicit* -subclass of the protocol. If a class is a structural consistent subtype of a -protocol, it is said to implement the protocol and to be assignable to the -protocol. If a class is assignable to a protocol but the protocol is not -included in the MRO, the class is *implicitly* assignable to the protocol. -(Note that one can explicitly subclass a protocol and still not implement it if -a protocol attribute is set to ``None`` in the subclass, see Python -:py:ref:`data model ` for details.) +subclass of the protocol. If a class defines all attributes and methods of a +protocol with types that are assignable to the types of the protocol's +attributes and methods, it is said to implement the protocol and to be +assignable to the protocol. If a class is assignable to a protocol but the +protocol is not included in the MRO, the class is *implicitly* assignable to +the protocol. (Note that one can explicitly subclass a protocol and still not +implement it if a protocol attribute is set to ``None`` in the subclass, see +Python :py:ref:`data model ` for details.) The attributes (variables and methods) of a protocol that are mandatory for another class to be assignable to the protocol are called protocol members. From 5d400362ff69bad94d4ea3cc1dfc91abaa7d56a6 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Sat, 1 Jun 2024 22:58:50 -0600 Subject: [PATCH 29/45] one more review tweak on protocol wording --- docs/spec/protocol.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index 0220361b..71537150 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -179,10 +179,10 @@ Examples:: represent(nice) # OK represent(another) # Also OK -Note that there is little difference between explicit and implicit consistent -subtypes; the main benefit of explicit subclassing is to get some protocol -methods "for free". In addition, type checkers can statically verify that the -class actually implements the protocol correctly:: +Note that there is little difference between explicitly subclassing and +implicitly implementing the protocol; the main benefit of explicit subclassing +is to get some protocol methods "for free". In addition, type checkers can +statically verify that the class actually implements the protocol correctly:: class RGB(Protocol): rgb: tuple[int, int, int] From cbe6e235720545f4cb3b184a22c86dd9ba129669 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 10:30:19 -0400 Subject: [PATCH 30/45] add equivalent, narrow, and wide to glossary --- docs/spec/enums.rst | 2 +- docs/spec/glossary.rst | 22 ++++++++++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/docs/spec/enums.rst b/docs/spec/enums.rst index 6e10a90e..a3fa1ccd 100644 --- a/docs/spec/enums.rst +++ b/docs/spec/enums.rst @@ -350,7 +350,7 @@ literal values during type narrowing and exhaustion detection:: Likewise, a type checker should treat a complete union of all literal members -as compatible with the enum type:: +as :term:`equivalent` to the enum type:: class Answer(Enum): Yes = 1 diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index c94259d6..e90ff7de 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -43,6 +43,12 @@ This section defines a few terms that may be used elsewhere in the specification The packaged file which is used to publish and distribute a release. (:pep:`426`) + equivalent + Two :term:`fully static types ` ``A`` and ``B`` are + equivalent if ``A`` is a :term:`subtype` of ``B`` and ``B`` is a + :term:`subtype` of ``A``. This implies that ``A`` and ``B`` represent the + same set of possible runtime objects. + fully static type A type is "fully static" if it does not contain any :term:`gradual form`. Fully static types represent a set of possible runtime values. Fully @@ -87,6 +93,15 @@ This section defines a few terms that may be used elsewhere in the specification module A file containing Python runtime code or stubbed type information. + narrow + A :term:`fully static type` ``B`` is narrower than a fully static type + ``A`` if ``B`` is a :term:`subtype` of ``A`` and ``B`` is not + :term:`equivalent` to ``A``. This means that ``B`` represents a proper + subset of the possible objects represented by ``A``. "Type narrowing" is + when a type checker infers that a name or expression must have a narrower + type at some locations in control flow, due to some runtime check of its + value. + package A directory or directories that namespace Python modules. (Note the distinction between packages and :term:`distributions `. @@ -132,3 +147,10 @@ This section defines a few terms that may be used elsewhere in the specification can be used around a type to indicate that the annotated value may not be overridden or modified. This term is also used for other special forms that modify a type, but using a different syntactic context, such as the :ref:`@final ` decorator. + + wide + A :term:`fully static type` ``A`` is wider than a fully static type ``B`` + if and only if ``B`` is a :term:`subtype` of ``A`` and ``B`` is not + :term:`equivalent` to ``A``. This means that ``A`` represents a proper + superset of the possible values represented by ``B``. See also + ":term:`narrow`". From 895459571c7b23f52d489339733c88679367fe8a Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 10:45:26 -0400 Subject: [PATCH 31/45] add table of type relations --- docs/spec/concepts.rst | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index fddbdd9d..0669e787 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -248,6 +248,27 @@ because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to ``tuple[Any, B]``. +Summary of type relations +------------------------- + +The subtype, supertype, and equivalence relations establish a partial order on +fully static types. The analogous relations on gradual types (via +materialization) are "assignable-to" (or consistent subtype), "assignable-from" +(or consistent supertype), and "consistent with". We can visualize this analogy +in the following table: + +.. list-table:: + :header-rows: 1 + + * - Fully static types + - Gradual types + * - ``B`` is a :term:`subtype` of ``A`` + - ``B`` is :term:`assignable` to (or a consistent subtype of) ``A`` + * - ``A`` is a :term:`supertype` of ``B`` + - ``A`` is assignable from (or a consistent supertype of) ``B`` + * - ``B`` is :term:`equivalent` to ``A`` + - ``B`` is :term:`consistent` with ``A`` + Attributes and methods ---------------------- From efaa7ab6a3d93641041e738f3217c46279638ca0 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 10:47:55 -0400 Subject: [PATCH 32/45] explicitly allow inference on missing function annotations --- docs/spec/annotations.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/spec/annotations.rst b/docs/spec/annotations.rst index 4ebfd01b..4650ef97 100644 --- a/docs/spec/annotations.rst +++ b/docs/spec/annotations.rst @@ -22,8 +22,9 @@ assignable to the annotated return type can be returned from the function. .. _`missing-annotations`: -Any function without annotations should be treated as having :ref:`Any` -annotations on all arguments and the return type. +Any function without annotations can be treated as having :ref:`Any` +annotations on all arguments and the return type. Type checkers may also +optionally infer more precise types for missing annotations. Type checkers may choose to entirely ignore (not type check) the bodies of functions with no annotations, but this behavior is not required. From 12ae9eb0332de22ac6fb1e2c83baeba608722483 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 11:12:58 -0400 Subject: [PATCH 33/45] some review comments --- docs/spec/callables.rst | 4 ++-- docs/spec/class-compat.rst | 2 +- docs/spec/concepts.rst | 6 +++--- docs/spec/generics.rst | 2 +- docs/spec/literal.rst | 4 ++-- docs/spec/protocol.rst | 15 ++++++++------- 6 files changed, 17 insertions(+), 16 deletions(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index bc9c5396..e86d0ea1 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -1,4 +1,4 @@ -.. _`callables`: +`.. _`callables`: Callables ========= @@ -530,7 +530,7 @@ interchangeably. Assignability rules for callables --------------------------------- -A callable type ``B`` is :term:`assignable` to callable type ``A`` if the +A callable type ``B`` is :term:`assignable` to a callable type ``A`` if the return type of ``B`` is assignable to the return type of ``A`` and the input signature of ``B`` accepts all possible combinations of arguments that the input signature of ``A`` accepts. All of the specific assignability rules diff --git a/docs/spec/class-compat.rst b/docs/spec/class-compat.rst index c1f47ffb..9f88d564 100644 --- a/docs/spec/class-compat.rst +++ b/docs/spec/class-compat.rst @@ -99,7 +99,7 @@ annotated in ``__init__`` or other methods, rather than in the class:: When type checkers encounter a method decorated with ``@typing.override`` they should treat it as a type error unless that method is overriding a method or attribute in some ancestor class, and the type of the overriding method is -assignable to the type of the overridden method. +:term:`assignable` to the type of the overridden method. .. code-block:: python diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 0669e787..930385b0 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -253,9 +253,9 @@ Summary of type relations The subtype, supertype, and equivalence relations establish a partial order on fully static types. The analogous relations on gradual types (via -materialization) are "assignable-to" (or consistent subtype), "assignable-from" -(or consistent supertype), and "consistent with". We can visualize this analogy -in the following table: +materialization) are "assignable-to" (or "consistent subtype"), +"assignable-from" (or "consistent supertype"), and "consistent with". We can +visualize this analogy in the following table: .. list-table:: :header-rows: 1 diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst index 93955775..3ae51c78 100644 --- a/docs/spec/generics.rst +++ b/docs/spec/generics.rst @@ -2266,7 +2266,7 @@ Use in Attribute Annotations ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Another use for ``Self`` is to annotate attributes. One example is where we -have a ``LinkedList`` whose elements must be consistent subtypes of the current +have a ``LinkedList`` whose elements must be :term:`assignable` to the current class. :: diff --git a/docs/spec/literal.rst b/docs/spec/literal.rst index f9decdef..fa66b6ad 100644 --- a/docs/spec/literal.rst +++ b/docs/spec/literal.rst @@ -303,8 +303,8 @@ special-casing. For example, programs like the following are type safe:: # Legal: Literal["foo"] is a subtype of str expects_str(var) -This also means non-Literal types in general are not assignable to Literal -types. For example:: +This also means non-Literal types in general are not :term:`assignable` to +Literal types. For example:: def expects_literal(x: Literal["foo"]) -> None: ... diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index 71537150..8b30a7e1 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -29,11 +29,12 @@ attributes and methods, it is said to implement the protocol and to be assignable to the protocol. If a class is assignable to a protocol but the protocol is not included in the MRO, the class is *implicitly* assignable to the protocol. (Note that one can explicitly subclass a protocol and still not -implement it if a protocol attribute is set to ``None`` in the subclass, see +implement it if a protocol attribute is set to ``None`` in the subclass. See Python :py:ref:`data model ` for details.) The attributes (variables and methods) of a protocol that are mandatory for -another class to be assignable to the protocol are called protocol members. +another class for it to be assignable to the protocol are called "protocol +members". .. _protocol-definition: @@ -75,7 +76,7 @@ be used in every context where normal types can:: Note that both the user-defined class ``Resource`` and the built-in ``IO`` type (the return type of ``open()``) are assignable to ``SupportsClose``, because -they provide a ``close()`` method with an assignable type signature. +each provides a ``close()`` method with an assignable type signature. Protocol members @@ -621,10 +622,10 @@ the risks for this feature, the following rules are applied. ``Iterator``, etc). A protocol that contains at least one non-method member (like ``x: int``) is called a data protocol. * *Unsafe overlap*: A type ``X`` is called unsafely overlapping with a protocol - ``P``, if ``X`` is not assignable to ``P``, but it is assignable to the type - erased version of ``P`` where all members have type ``Any``. In addition, if - at least one element of a union unsafely overlaps with a protocol ``P``, then - the whole union is unsafely overlapping with ``P``. + ``P``, if ``X`` is not assignable to ``P``, but it is assignable to the + type-erased version of ``P`` where all members have type ``Any``. In + addition, if at least one element of a union unsafely overlaps with a + protocol ``P``, then the whole union is unsafely overlapping with ``P``. **Specification**: From ccfef86fb81f47bbc2f05d7cb0d9adebd28d1e89 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 11:34:11 -0400 Subject: [PATCH 34/45] Update docs/spec/callables.rst Co-authored-by: Alex Waygood --- docs/spec/callables.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index e86d0ea1..25325c7b 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -1,4 +1,4 @@ -`.. _`callables`: +.. _`callables`: Callables ========= From e990bda9d913ae1b2a05bfaa6df033e29e6af34b Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 12 Jun 2024 11:35:30 -0400 Subject: [PATCH 35/45] more review comments --- docs/spec/concepts.rst | 5 +++-- docs/spec/constructors.rst | 4 ++-- docs/spec/literal.rst | 10 +++++----- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 930385b0..fc5a3bf5 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -231,7 +231,8 @@ function) if its type 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 ``B`` is "assignable to" a type ``A`` if ``B`` is a -consistent subtype of ``A``. +consistent subtype of ``A``. In this case we can also say that ``A`` is +"assignable from" ``B``. In the remainder of this specification, we will usually prefer the term **assignable to** over "consistent subtype of". The two are synonymous, but @@ -346,7 +347,7 @@ One common case of union types are *optional* types, which are a union with def handle_employee(e: Employee | None) -> None: ... -Either an instance of ``Employee`` or the value ``None`` are assignable to the +Either the type ``Employee`` or the type of ``None`` are assignable to the union ``Employee | None``. A past version of this specification allowed type checkers to assume an optional diff --git a/docs/spec/constructors.rst b/docs/spec/constructors.rst index 547d736f..b8591ba1 100644 --- a/docs/spec/constructors.rst +++ b/docs/spec/constructors.rst @@ -353,8 +353,8 @@ methods for a class have :term:`consistent` signatures. Converting a Constructor to Callable ------------------------------------ -Class objects are callable, which means they are :term:`assignable` to callable -types. +Class objects are callable, which means the type of a class object can be +:term:`assignable` to a callable type. :: diff --git a/docs/spec/literal.rst b/docs/spec/literal.rst index fa66b6ad..174995e9 100644 --- a/docs/spec/literal.rst +++ b/docs/spec/literal.rst @@ -588,16 +588,16 @@ inferred to be of type ``Literal["foo"]``. We also infer ``LiteralString`` in the following cases: -+ Addition: ``x + y`` is of type ``LiteralString`` if both ``x`` and - ``y`` are assignable to ``LiteralString``. ++ Addition: ``x + y`` is of type ``LiteralString`` if the types of both ``x`` + and ``y`` are assignable to ``LiteralString``. + Joining: ``sep.join(xs)`` is of type ``LiteralString`` if ``sep``'s type is assignable to ``LiteralString`` and ``xs``'s type is assignable to ``Iterable[LiteralString]``. -+ In-place addition: If ``s`` has type ``LiteralString`` and ``x`` has - type assignable to ``LiteralString``, then ``s += x`` preserves - ``s``'s type as ``LiteralString``. ++ In-place addition: If ``s`` has type ``LiteralString`` and ``x`` has a type + assignable to ``LiteralString``, then ``s += x`` preserves ``s``'s type as + ``LiteralString``. + String formatting: An f-string has type ``LiteralString`` if and only if its constituent expressions are literal strings. ``s.format(...)`` is assignable From 045d7c29f4dc6daa532c7c81b11aafd01fbd23c9 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:04:14 -0400 Subject: [PATCH 36/45] link 'assignable' to glossary more often in callables doc --- docs/spec/callables.rst | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index 25325c7b..a6382ecf 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -209,8 +209,8 @@ Source and destination contain ``**kwargs`` """"""""""""""""""""""""""""""""""""""""""" Both destination and source functions have a ``**kwargs: Unpack[TypedDict]`` -parameter and the destination function's ``TypedDict`` is assignable to the -source function's ``TypedDict`` and the rest of the parameters are +parameter and the destination function's ``TypedDict`` is :term:`assignable` to +the source function's ``TypedDict`` and the rest of the parameters are compatible:: class Animal(TypedDict): @@ -235,7 +235,7 @@ Source contains ``**kwargs`` and destination doesn't The destination callable doesn't contain ``**kwargs``, the source callable contains ``**kwargs: Unpack[TypedDict]`` and the destination function's keyword -arguments are assignable to the corresponding keys in source function's +arguments are :term:`assignable` to the corresponding keys in source function's ``TypedDict``. Moreover, not required keys should correspond to optional function arguments, whereas required keys should correspond to required function arguments. Again, the rest of the parameters have to be compatible. @@ -301,8 +301,8 @@ Source contains traditionally typed ``**kwargs: T`` The destination callable contains ``**kwargs: Unpack[TypedDict]``, the source callable contains traditionally typed ``**kwargs: T`` and each of the -destination function ``TypedDict``'s fields is assignable to a variable of -type ``T``:: +destination function ``TypedDict``'s fields is :term:`assignable` to a variable +of type ``T``:: class Vehicle: ... @@ -542,9 +542,9 @@ Parameter types Callable types are covariant with respect to their return types but contravariant with respect to their parameter types. This means a callable -``B`` is assignable to callable ``A`` if the types of the parameters of -``A`` are assignable to the parameters of ``B``. For example, -``(x: float) -> int`` is assignable to ``(x: int) -> float``:: +``B`` is :term:`assignable` to callable ``A`` if the types of the parameters of +``A`` are assignable to the parameters of ``B``. For example, ``(x: float) -> +int`` is assignable to ``(x: int) -> float``:: def func(cb: Callable[[float], int]): f1: Callable[[int], float] = cb # OK @@ -553,7 +553,7 @@ contravariant with respect to their parameter types. This means a callable Parameter kinds ^^^^^^^^^^^^^^^ -Callable ``B`` is assignable to callable ``A`` only if all keyword-only +Callable ``B`` is :term:`assignable` to callable ``A`` only if all keyword-only parameters in ``A`` are present in ``B`` as either keyword-only parameters or standard (positional or keyword) parameters. For example, ``(a: int) -> None`` is assignable to ``(*, a: int) -> None``, but the converse is not true. The @@ -589,8 +589,9 @@ names of positional-only parameters are ignored for purposes of assignability:: ^^^^^^^^^^^^^^^^^^^^ If a callable ``A`` has a signature with a ``*args`` parameter, callable ``B`` -must also have a ``*args`` parameter to be assignable to ``A``, and the type of -``A``'s ``*args`` parameter must be assignable to ``B``'s ``*args`` parameter:: +must also have a ``*args`` parameter to be :term:`assignable` to ``A``, and the +type of ``A``'s ``*args`` parameter must be assignable to ``B``'s ``*args`` +parameter:: class NoArgs(Protocol): def __call__(self) -> None: ... @@ -648,9 +649,9 @@ otherwise-unmatched positional-only parameters in ``A``:: ``**kwargs`` parameters ^^^^^^^^^^^^^^^^^^^^^^^ -If a callable ``A`` has a signature with a ``**kwargs`` parameter (without -an unpacked ``TypedDict`` type annotation), callable ``B`` must also have a -``**kwargs`` parameter to be assignable to ``A``, and the type of +If a callable ``A`` has a signature with a ``**kwargs`` parameter (without an +unpacked ``TypedDict`` type annotation), callable ``B`` must also have a +``**kwargs`` parameter to be :term:`assignable` to ``A``, and the type of ``A``'s ``**kwargs`` parameter must be assignable to ``B``'s ``**kwargs`` parameter:: @@ -732,8 +733,8 @@ Default argument values If a callable ``C`` has a parameter ``x`` with a default argument value and ``A`` is the same as ``C`` except that ``x`` has no default argument, then -``C`` is assignable to ``A``. ``C`` is also assignable to ``A`` -if ``A`` is the same as ``C`` with parameter ``x`` removed:: +``C`` is :term:`assignable` to ``A``. ``C`` is also assignable to ``A`` if +``A`` is the same as ``C`` with parameter ``x`` removed:: class DefaultArg(Protocol): def __call__(self, x: int = 0) -> None: ... @@ -752,9 +753,9 @@ if ``A`` is the same as ``C`` with parameter ``x`` removed:: Overloads ^^^^^^^^^ -If a callable ``B`` is overloaded with two or more signatures, it is assignable -to callable ``A`` if *at least one* of the overloaded signatures in ``B`` is -assignable to ``A``:: +If a callable ``B`` is overloaded with two or more signatures, it is +:term:`assignable` to callable ``A`` if *at least one* of the overloaded +signatures in ``B`` is assignable to ``A``:: class Overloaded(Protocol): @overload From dd6ffd1d9e12fc136aebfbcd1b64d82893b01840 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:36:14 -0400 Subject: [PATCH 37/45] add nominal/structural to concepts and glossary --- docs/spec/callables.rst | 2 +- docs/spec/concepts.rst | 28 +++++++++ docs/spec/glossary.rst | 21 +++++-- docs/spec/protocol.rst | 45 +++++++------- docs/spec/typeddict.rst | 127 +++++++++++++++++++++++----------------- 5 files changed, 143 insertions(+), 80 deletions(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index a6382ecf..7c26db44 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -283,7 +283,7 @@ unpacked in the destination callable invocation:: dest(**animal) # Fails at runtime. A similar situation can happen even without inheritance as :term:`assignability -` between ``TypedDict``\s is structural. +` between ``TypedDict``\s is :term:`structural`. Source contains untyped ``**kwargs`` """""""""""""""""""""""""""""""""""" diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index fc5a3bf5..b82956d5 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -159,6 +159,29 @@ subtype" of ``A``) if ``B`` is a subtype of ``A`` and ``B`` is not equivalent to ``A``. In the same scenario we can describe the type ``A`` as "wider" than ``B``, or a "proper supertype" of ``B``. +Nominal and structural types +---------------------------- + +For a type such as ``str`` (or any other class), which describes the set of +values whose ``__class__`` is ``str`` or a direct or indirect subclass of it, +subtyping corresponds directly to subclassing. A subclass ``MyStr`` of ``str`` +is a subtype of ``str``, because ``MyStr`` represents a subset of the values +represented by ``str``. Such types can be called "nominal types" and this is +"nominal subtyping." + +Other types (e.g. :ref:`Protocols` and :ref:`TypedDict`) instead describe a set +of values by the types of their attributes and methods, or the types of their +dictionary keys and values. These are called "structural types." A structural +type may be a subtype of another type without any inheritance or subclassing +relationship, simply because it shares all the attributes/methods (or +keys/values) of the supertype, and adds additional requirements, thus +representing a subset of the possible values. This is "structural subtyping." + +Although the means of specifying the set of values represented by the types +differs, the fundamental concepts are the same for both nominal and structural +types: the type represents a set of possible values and a subtype represents a +subset of the values. + Materialization --------------- @@ -249,6 +272,11 @@ because ``tuple[Any, B]`` can materialize to ``tuple[int, B]``, which is a subtype of ``tuple[int, A]``. But ``tuple[int, A]`` is not assignable to ``tuple[Any, B]``. +For a gradual structural type, consistency and assignability are also +structural. For example, the structural type "all objects with an attribute +``x`` of type ``Any``" is consistent with (and assignable to) the structural +type "all objects with an attribute ``x`` of type ``int``". + Summary of type relations ------------------------- diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index e90ff7de..a6f7d4e8 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -102,6 +102,11 @@ This section defines a few terms that may be used elsewhere in the specification type at some locations in control flow, due to some runtime check of its value. + nominal + A nominal type (e.g. a class name) represents the set of values whose + ``__class__`` is that type, or any of its subclasses, transitively. In + contrast, see :term:`structural` types. + package A directory or directories that namespace Python modules. (Note the distinction between packages and :term:`distributions `. @@ -116,6 +121,14 @@ This section defines a few terms that may be used elsewhere in the specification be imported from the :py:mod:`typing` module or equivalently from ``typing_extensions``, but some special forms are placed in other modules. + structural + A structural type (see e.g. :ref:`Protocols`, :ref:`TypedDict`) defines a + set of values not by their ``__class__``, but by their properties (e.g. + attributes, methods, dictionary key/value types). :ref:`Callable` types + are also structural; a callable type is a subtype of another callable + type based on their signatures, not a subclass relationship. In contrast, + see :term:`nominal` types. + stub A file containing only type information, empty of runtime code (the filename ends in ``.pyi``). See :ref:`stub-files`. @@ -124,10 +137,10 @@ This section defines a few terms that may be used elsewhere in the specification A :term:`fully static type` ``B`` is a subtype of a fully static type ``A`` if and only if the set of possible runtime values represented by ``B`` is a subset of the set of possible runtime values represented by - ``A``. For nominal types (classes), subtyping is defined by inheritance. - For structural types (see :ref:`Protocols`, :ref:`TypedDict`), subtyping - is defined by a shared set of attributes/methods or keys. Subtype is the - inverse of :term:`supertype`. See :ref:`type-system-concepts`. + ``A``. For :term:`nominal` types (classes), subtyping is defined by + inheritance. For :term:`structural` types, subtyping is defined by a + shared set of attributes/methods or keys. Subtype is the inverse of + :term:`supertype`. See :ref:`type-system-concepts`. supertype A :term:`fully static type` ``A`` is a supertype of a fully static type diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index 8b30a7e1..98a720f2 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -8,7 +8,7 @@ Protocols Terminology ^^^^^^^^^^^ -The term *protocols* is used for types supporting structural +The term *protocols* is used for some types supporting :term:`structural` subtyping. The reason is that the term *iterator protocol*, for example, is widely understood in the community, and coming up with a new term for this concept in a statically typed context would just create @@ -52,9 +52,9 @@ at the end of the list. Here is a simple example:: ... Now if one defines a class ``Resource`` with a ``close()`` method whose type -signature is assignable to ``SupportsClose.close``, it would implicitly be -assignable to ``SupportsClose``, since structural assignability is used for -protocol types:: +signature is :term:`assignable` to ``SupportsClose.close``, it would implicitly +be assignable to ``SupportsClose``, since :term:`structural` assignability is +used for protocol types:: class Resource: ... @@ -147,8 +147,8 @@ So while it's possible to subclass a protocol explicitly, it's *not necessary* to do so for the sake of type-checking. The default implementations cannot be used if the assignable-to relationship is -implicit and only structural -- the semantics of inheritance is not changed. -Examples:: +implicit and only :term:`structural` -- the semantics of inheritance is not +changed. Examples:: class PColor(Protocol): @abstractmethod @@ -208,14 +208,14 @@ explicit subclass before it can be instantiated. Merging and extending protocols ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -The general philosophy is that protocols are mostly like regular ABCs, -but a static type checker will handle them specially. Subclassing a protocol -class would not turn the subclass into a protocol unless it also has -``typing.Protocol`` as an explicit base class. Without this base, the class -is "downgraded" to a regular ABC that cannot be used with structural +The general philosophy is that protocols are mostly like regular ABCs, but a +static type checker will handle them specially. Subclassing a protocol class +would not turn the subclass into a protocol unless it also has +``typing.Protocol`` as an explicit base class. Without this base, the class is +"downgraded" to a regular ABC that cannot be used with :term:`structural` subtyping. The rationale for this rule is that we don't want to accidentally -have some class act as a protocol just because one of its base classes -happens to be one. We still slightly prefer nominal subtyping over structural +have some class act as a protocol just because one of its base classes happens +to be one. We still slightly prefer :term:`nominal` subtyping over structural subtyping in the static typing world. A subprotocol can be defined by having *both* one or more protocols as @@ -245,9 +245,9 @@ with ``typing.Sized``:: class SizedAndClosable(Sized, SupportsClose, Protocol): pass -The two definitions of ``SizedAndClosable`` are equivalent. -Subclass relationships between protocols are not meaningful when -considering assignability, since structural assignability is +The two definitions of ``SizedAndClosable`` are equivalent. Subclass +relationships between protocols are not meaningful when considering +assignability, since :term:`structural` :term:`assignability ` is the criterion, not the MRO. If ``Protocol`` is included in the base class list, all the other base classes @@ -378,10 +378,10 @@ runtime type is a protocol. For variables and parameters with protocol types, assignability relationships are subject to the following rules: * A protocol is never assignable to a concrete type. -* A concrete type ``X`` is assignable to a protocol ``P`` - if and only if ``X`` implements all protocol members of ``P`` with - assignable types. In other words, assignability with respect to a protocol is - always structural. +* A concrete type ``X`` is assignable to a protocol ``P`` if and only if ``X`` + implements all protocol members of ``P`` with assignable types. In other + words, :term:`assignability ` with respect to a protocol is + always :term:`structural`. * A protocol ``P1`` is assignable to another protocol ``P2`` if ``P1`` defines all protocol members of ``P2`` with assignable types. @@ -459,8 +459,9 @@ Example:: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Variables and parameters annotated with ``type[Proto]`` accept only concrete -(non-protocol) consistent subtypes of ``Proto``. The main reason for this is to -allow instantiation of parameters with such types. For example:: +(non-protocol) :term:`consistent subtypes ` of ``Proto``. +The main reason for this is to allow instantiation of parameters with such +types. For example:: class Proto(Protocol): @abstractmethod diff --git a/docs/spec/typeddict.rst b/docs/spec/typeddict.rst index 2903c040..94846172 100644 --- a/docs/spec/typeddict.rst +++ b/docs/spec/typeddict.rst @@ -30,10 +30,10 @@ required or not). This section also provides a sketch of how a type checker is expected to support type checking operations involving TypedDict objects. Similar to :pep:`484`, this discussion is left somewhat vague on purpose, to allow -experimentation with a wide variety of different type checking approaches. In -particular, :term:`assignability ` should be structural: a more -specific TypedDict type can be assignable to a smaller (more general) -TypedDict type. +experimentation with a wide variety of different type checking approaches. In +particular, :term:`assignability ` should be :term:`structural`: a +more specific TypedDict type can be assignable to a more general TypedDict +type, without any inheritance relationship between them. Class-based Syntax @@ -172,9 +172,9 @@ TypedDict types using the class-based syntax. In this case the class BookBasedMovie(Movie): based_on: str -Now ``BookBasedMovie`` has keys ``name``, ``year``, and ``based_on``. -It is equivalent to this definition, since TypedDict types use -structural compatibility:: +Now ``BookBasedMovie`` has keys ``name``, ``year``, and ``based_on``. It is +equivalent to this definition, since TypedDict types use :term:`structural` +:term:`assignability `:: class BookBasedMovie(TypedDict): name: str @@ -318,9 +318,9 @@ Discussion: f(b) # Type check error: 'B' not assignable to 'A' b['x'] + 1 # Runtime error: None + 1 -* A TypedDict type with a required key is not consistent with a - TypedDict type where the same key is a non-required key, since the - latter allows keys to be deleted. Example where this is relevant:: +* A TypedDict type with a required key is not :term:`assignable` to a TypedDict + type where the same key is a non-required key, since the latter allows keys + to be deleted. Example where this is relevant:: class A(TypedDict, total=False): x: int @@ -332,14 +332,14 @@ Discussion: del a['x'] b: B = {'x': 0} - f(b) # Type check error: 'B' not compatible with 'A' + f(b) # Type check error: 'B' not assignable to 'A' b['x'] + 1 # Runtime KeyError: 'x' -* A TypedDict type ``A`` with no key ``'x'`` is not consistent with a - TypedDict type with a non-required key ``'x'``, since at runtime - the key ``'x'`` could be present and have an incompatible type - (which may not be visible through ``A`` due to structural subtyping). - Example:: +* A TypedDict type ``A`` with no key ``'x'`` is not :term:`assignable` to a + TypedDict type with a non-required key ``'x'``, since at runtime the key + ``'x'`` could be present and have an :term:`inconsistent ` type + (which may not be visible through ``A`` due to :term:`structural` + assignability). Example:: class A(TypedDict, total=False): x: int @@ -356,16 +356,16 @@ Discussion: a['y'] = 1 def g(b: B) -> None: - f(b) # Type check error: 'B' incompatible with 'A' + f(b) # Type check error: 'B' not assignable to 'A' c: C = {'x': 0, 'y': 'foo'} g(c) c['y'] + 'bar' # Runtime error: int + str -* A TypedDict isn't consistent with any ``Dict[...]`` type, since - dictionary types allow destructive operations, including - ``clear()``. They also allow arbitrary keys to be set, which - would compromise type safety. Example:: +* A TypedDict isn't :term:`assignable` to any ``Dict[...]`` type, since + dictionary types allow destructive operations, including ``clear()``. They + also allow arbitrary keys to be set, which would compromise type safety. + Example:: class A(TypedDict): x: int @@ -377,17 +377,17 @@ Discussion: d['y'] = 0 def g(a: A) -> None: - f(a) # Type check error: 'A' incompatible with Dict[str, int] + f(a) # Type check error: 'A' not assignable to Dict[str, int] b: B = {'x': 0, 'y': 'foo'} g(b) b['y'] + 'bar' # Runtime error: int + str -* A TypedDict with all ``int`` values is not consistent with - ``Mapping[str, int]``, since there may be additional non-``int`` - values not visible through the type, due to structural subtyping. - These can be accessed using the ``values()`` and ``items()`` - methods in ``Mapping``, for example. Example:: +* A TypedDict with all ``int`` values is not :term:`assignable` to + ``Mapping[str, int]``, since there may be additional non-``int`` values not + visible through the type, due to :term:`structural` assignability. These can + be accessed using the ``values()`` and ``items()`` methods in ``Mapping``, + for example. Example:: class A(TypedDict): x: int @@ -403,7 +403,7 @@ Discussion: return n def f(a: A) -> None: - sum_values(a) # Error: 'A' incompatible with Mapping[str, int] + sum_values(a) # Error: 'A' not assignable to Mapping[str, int] b: B = {'x': 0, 'y': 'foo'} f(b) @@ -429,13 +429,13 @@ value is unknown during type checking, and thus can cause some of the above violations. (`Use of Final Values and Literal Types`_ generalizes this to cover final names and literal types.) -The use of a key that is not known to exist should be reported as an -error, even if this wouldn't necessarily generate a runtime type -error. These are often mistakes, and these may insert values with an -invalid type if structural subtyping hides the types of certain items. -For example, ``d['x'] = 1`` should generate a type check error if -``'x'`` is not a valid key for ``d`` (which is assumed to be a -TypedDict type). +The use of a key that is not known to exist should be reported as an error, +even if this wouldn't necessarily generate a runtime type error. These are +often mistakes, and these may insert values with an invalid type if +:term:`structural` :term:`assignability ` hides the types of +certain items. For example, ``d['x'] = 1`` should generate a type check error +if ``'x'`` is not a valid key for ``d`` (which is assumed to be a TypedDict +type). Extra keys included in TypedDict object construction should also be caught. In this example, the ``director`` key is not defined in @@ -460,10 +460,10 @@ objects as unsafe, even though they are valid for normal dictionaries: of ``d.get(e)`` should be ``object`` if the string value of ``e`` cannot be determined statically. -* ``clear()`` is not safe since it could remove required keys, some of - which may not be directly visible because of structural - subtyping. ``popitem()`` is similarly unsafe, even if all known - keys are not required (``total=False``). +* ``clear()`` is not safe since it could remove required keys, some of which + may not be directly visible because of :term:`structural` + :term:`assignability `. ``popitem()`` is similarly unsafe, even + if all known keys are not required (``total=False``). * ``del obj['key']`` should be rejected unless ``'key'`` is a non-required key. @@ -729,26 +729,39 @@ Subclasses can combine these rules:: class User(OptionalIdent): ident: str # Required, mutable, and not an int -Note that these are just consequences of structural typing, but they are highlighted here as the behavior now differs from the rules specified in :pep:`589`. +Note that these are just consequences of :term:`structural` typing, but they +are highlighted here as the behavior now differs from the rules specified in +:pep:`589`. -Type consistency -^^^^^^^^^^^^^^^^ +Assignability +^^^^^^^^^^^^^ -*This section updates the type consistency rules described above that were created prior to the introduction of ReadOnly* +*This section updates the assignability rules described above that were created +prior to the introduction of ReadOnly* -A TypedDict type ``A`` is consistent with TypedDict ``B`` if ``A`` is structurally compatible with ``B``. This is true if and only if all of the following are satisfied: +A TypedDict type ``B`` is :term:`assignable` to a TypedDict type ``A`` if ``B`` +is :term:`structurally ` assignable to ``A``. This is true if and +only if all of the following are satisfied: -* For each item in ``B``, ``A`` has the corresponding key, unless the item in ``B`` is read-only, not required, and of top value type (``ReadOnly[NotRequired[object]]``). -* For each item in ``B``, if ``A`` has the corresponding key, the corresponding value type in ``A`` is consistent with the value type in ``B``. -* For each non-read-only item in ``B``, its value type is consistent with the corresponding value type in ``A``. -* For each required key in ``B``, the corresponding key is required in ``A``. -* For each non-required key in ``B``, if the item is not read-only in ``B``, the corresponding key is not required in ``A``. +* For each item in ``A``, ``B`` has the corresponding key, unless the item in + ``A`` is read-only, not required, and of top value type + (``ReadOnly[NotRequired[object]]``). +* For each item in ``A``, if ``B`` has the corresponding key, the corresponding + value type in ``B`` is assignable to the value type in ``A``. +* For each non-read-only item in ``A``, its value type is assignable to the + corresponding value type in ``B``. +* For each required key in ``A``, the corresponding key is required in ``B``. +* For each non-required key in ``A``, if the item is not read-only in ``A``, + the corresponding key is not required in ``B``. Discussion: -* All non-specified items in a TypedDict implicitly have value type ``ReadOnly[NotRequired[object]]``. +* All non-specified items in a TypedDict implicitly have value type + ``ReadOnly[NotRequired[object]]``. -* Read-only items behave covariantly, as they cannot be mutated. This is similar to container types such as ``Sequence``, and different from non-read-only items, which behave invariantly. Example:: +* Read-only items behave covariantly, as they cannot be mutated. This is + similar to container types such as ``Sequence``, and different from + non-read-only items, which behave invariantly. Example:: class A(TypedDict): x: ReadOnly[int | None] @@ -762,7 +775,13 @@ Discussion: b: B = {"x": 1} f(b) # Accepted by type checker -* A TypedDict type ``A`` with no explicit key ``'x'`` is not consistent with a TypedDict type ``B`` with a non-required key ``'x'``, since at runtime the key ``'x'`` could be present and have an incompatible type (which may not be visible through ``A`` due to structural subtyping). The only exception to this rule is if the item in ``B`` is read-only, and the value type is of top type (``object``). For example:: +* A TypedDict type ``A`` with no explicit key ``'x'`` is not :term:`assignable` + to a TypedDict type ``B`` with a non-required key ``'x'``, since at runtime + the key ``'x'`` could be present and have an :term:`inconsistent + ` type (which may not be visible through ``A`` due to + :term:`structural` typing). The only exception to this rule is if the item in + ``B`` is read-only, and the value type is of top type (``object``). For + example:: class A(TypedDict): x: int @@ -777,7 +796,9 @@ Discussion: Update method ^^^^^^^^^^^^^ -In addition to existing type checking rules, type checkers should error if a TypedDict with a read-only item is updated with another TypedDict that declares that key:: +In addition to existing type checking rules, type checkers should error if a +TypedDict with a read-only item is updated with another TypedDict that declares +that key:: class A(TypedDict): x: ReadOnly[int] From 673a46708cdf256962fcdcd33c9a581e94556f01 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:40:32 -0400 Subject: [PATCH 38/45] don't use 'compatible' in callables doc --- docs/spec/callables.rst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index 7c26db44..580faa4d 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -201,9 +201,8 @@ caller, then an error must be reported by type checkers. Assignment ^^^^^^^^^^ -Assignments of a function typed with ``**kwargs: Unpack[Movie]`` and -another callable type should pass type checking only if they are compatible. -This can happen for the scenarios described below. +Assignments of a function typed with ``**kwargs: Unpack[Movie]`` and another +callable type should pass type checking only for the scenarios described below. Source and destination contain ``**kwargs`` """"""""""""""""""""""""""""""""""""""""""" @@ -211,7 +210,7 @@ Source and destination contain ``**kwargs`` Both destination and source functions have a ``**kwargs: Unpack[TypedDict]`` parameter and the destination function's ``TypedDict`` is :term:`assignable` to the source function's ``TypedDict`` and the rest of the parameters are -compatible:: +assignable:: class Animal(TypedDict): name: str @@ -238,7 +237,7 @@ contains ``**kwargs: Unpack[TypedDict]`` and the destination function's keyword arguments are :term:`assignable` to the corresponding keys in source function's ``TypedDict``. Moreover, not required keys should correspond to optional function arguments, whereas required keys should correspond to required -function arguments. Again, the rest of the parameters have to be compatible. +function arguments. Again, the rest of the parameters have to be assignable. Continuing the previous example:: class Example(TypedDict): @@ -252,7 +251,7 @@ Continuing the previous example:: dest = src # OK! It is worth pointing out that the destination function's parameters that are to -be compatible with the keys and values from the ``TypedDict`` must be keyword +be assignable to the keys and values from the ``TypedDict`` must be keyword only:: def dest(dog: Dog, string: str, number: int = ...): ... @@ -435,7 +434,7 @@ of parameter types. This is a :term:`gradual form` indicating that the type is A ``...`` can also be used with ``Concatenate``. In this case, the parameters prior to the ``...`` are required to be present in the input signature and -be compatible in kind and type, but any additional parameters are permitted:: +be assignable, but any additional parameters are permitted:: cb3: Callable[Concatenate[int, ...], str] cb3 = lambda x: str(x) # OK From 0f5fba4af20525adc9a51c89759ae88e9a7c4a0b Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:46:26 -0400 Subject: [PATCH 39/45] equivalence of gradual types and union simplification --- docs/spec/concepts.rst | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index b82956d5..7c654848 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -298,6 +298,12 @@ visualize this analogy in the following table: * - ``B`` is :term:`equivalent` to ``A`` - ``B`` is :term:`consistent` with ``A`` +In addition to these analogous relations, we can also define equivalence on +gradual types. Two 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``. + Attributes and methods ---------------------- @@ -364,8 +370,10 @@ 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. -As a special case, the union ``Any | Any`` can be simplified to ``Any``: the -union of two unknown sets of objects is an unknown set of objects. +Equivalent gradual types can, however, be simplified from unions; e.g. +``list[Any] | list[Any]`` is equivalent to ``list[Any]``. Similarly, the union +``Any | Any`` can be simplified to ``Any``: the union of two unknown sets of +objects is an unknown set of objects. Union with None ~~~~~~~~~~~~~~~ From a6b3ab0deabad6709e50b8cdc5adba3b984f3652 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:37:33 -0600 Subject: [PATCH 40/45] simplify description of structural subtyping --- docs/spec/concepts.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 7c654848..7d82930e 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -173,9 +173,9 @@ Other types (e.g. :ref:`Protocols` and :ref:`TypedDict`) instead describe a set of values by the types of their attributes and methods, or the types of their dictionary keys and values. These are called "structural types." A structural type may be a subtype of another type without any inheritance or subclassing -relationship, simply because it shares all the attributes/methods (or -keys/values) of the supertype, and adds additional requirements, thus -representing a subset of the possible values. This is "structural subtyping." +relationship, simply because it meets all the requirements of the supertype, +and perhaps adds more, thus representing a subset of the possible values of the +supertype. This is "structural subtyping." Although the means of specifying the set of values represented by the types differs, the fundamental concepts are the same for both nominal and structural From e5943a4fb3bea8d5004246097b18aa67e3817f39 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Fri, 14 Jun 2024 18:37:47 -0600 Subject: [PATCH 41/45] define equivalence of gradual types in glossary --- docs/spec/glossary.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index a6f7d4e8..fc134eb7 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -47,7 +47,10 @@ This section defines a few terms that may be used elsewhere in the specification Two :term:`fully static types ` ``A`` and ``B`` are equivalent if ``A`` is a :term:`subtype` of ``B`` and ``B`` is a :term:`subtype` of ``A``. This implies that ``A`` and ``B`` represent the - same set of possible runtime objects. + same set of possible runtime objects. Two gradual types ``A`` and ``B`` + are equivalent if all :term:`materializations ` of ``A`` are + also materializations of ``B``, and all materializations of ``B`` are + also materializations of ``A``. fully static type A type is "fully static" if it does not contain any :term:`gradual form`. From effcdece9dec0700e08046a33a11f09277308e9d Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Mon, 17 Jun 2024 15:59:33 -0600 Subject: [PATCH 42/45] more review comments --- docs/spec/concepts.rst | 10 +++++----- docs/spec/generics.rst | 8 ++++---- docs/spec/glossary.rst | 8 ++++---- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 7d82930e..33a2044e 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -298,11 +298,11 @@ visualize this analogy in the following table: * - ``B`` is :term:`equivalent` to ``A`` - ``B`` is :term:`consistent` with ``A`` -In addition to these analogous relations, we can also define equivalence on -gradual types. Two 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``. +We can also define equivalence on gradual types. Two 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``. Attributes and methods ---------------------- diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst index 3ae51c78..e9acbecb 100644 --- a/docs/spec/generics.rst +++ b/docs/spec/generics.rst @@ -2020,9 +2020,9 @@ normal subscription rules, non-overridden defaults should be substituted. Using ``bound`` and ``default`` """"""""""""""""""""""""""""""" -If both ``bound`` and ``default`` are passed, ``default`` must be a -:term:`consistent subtype` of ``bound``. If not, the type checker should -generate an error. +If both ``bound`` and ``default`` are passed, ``default`` must be +:term:`assignable` to ``bound``. If not, the type checker should generate an +error. :: @@ -2297,7 +2297,7 @@ constructions with subclasses: def ordinal_value(self) -> str: return as_ordinal(self.value) - # Should not be OK because LinkedList[int] is not a consistent subtype of + # Should not be OK because LinkedList[int] is not assignable to # OrdinalLinkedList, but the type checker allows it. xs = OrdinalLinkedList(value=1, next=LinkedList[int](value=2)) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index fc134eb7..6427dae7 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -29,10 +29,10 @@ This section defines a few terms that may be used elsewhere in the specification consistent Two :term:`fully static types ` are "consistent with" - each other if they are the same type. Two gradual types are "consistent - with" each other if they could :term:`materialize` to the same type. See - :ref:`type-system-concepts`. If two types are consistent, they are both - :term:`assignable` to and from each other. + each other if they are :term:`equivalent`. Two gradual types are + "consistent with" each other if they could :term:`materialize` to the + same type. See :ref:`type-system-concepts`. If two types are consistent, + they are both :term:`assignable` to and from each other. consistent subtype "Consistent subtype" is synonymous with ":term:`assignable` to" (and From 9ebaef874c86afa33a8ccdecda548153f9c24df6 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 19 Jun 2024 17:38:29 -0500 Subject: [PATCH 43/45] review comments --- docs/spec/callables.rst | 5 +++-- docs/spec/concepts.rst | 42 ++++++++++++++++++++--------------------- docs/spec/generics.rst | 7 ++++--- docs/spec/glossary.rst | 23 ++++++++++++---------- docs/spec/protocol.rst | 2 +- 5 files changed, 42 insertions(+), 37 deletions(-) diff --git a/docs/spec/callables.rst b/docs/spec/callables.rst index 580faa4d..56b66bc1 100644 --- a/docs/spec/callables.rst +++ b/docs/spec/callables.rst @@ -706,8 +706,9 @@ parameters in ``A``:: f10: Standard = int_str_kwargs # Error: Does not accept positional arguments f11: Standard = str_kwargs # Error: Does not accept positional arguments -Assignability relationships for callable signatures that contain a ``**kwargs`` -with an unpacked ``TypedDict`` are described in the section :ref:`above `. +Assignability rules for callable signatures that contain a ``**kwargs`` with an +unpacked ``TypedDict`` are described in the section :ref:`above +`. Signatures with ParamSpecs diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 33a2044e..854e64b3 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -25,16 +25,16 @@ dynamically typed language. Type-annotated Python allows opting in to static type checking at a fine level of granularity, so that some type errors can be caught statically, without running the program. Variables, parameters, and returns can optionally be given -a static type annotation. Even within the type of a single data structure, +static type annotations. Even within the type of a single data structure, static type checking is optional and granular. For example, a dictionary can be annotated to enable static checking of the key type but only have dynamic runtime checking of the value type. A **gradual** type system is one in which a special "unknown" or "dynamic" type is used to describe names or expressions whose types are not known statically. -In Python, this type is spelled :ref:`Any`. Because :ref:`Any` indicates a +In Python, this type is spelled :ref:`Any`. Because :ref:`!Any` indicates a statically unknown type, the static type checker can't check type correctness -of operations on expressions typed as :ref:`Any`. These operations are still +of operations on expressions typed as :ref:`!Any`. These operations are still dynamically checked, via the Python runtime's usual dynamic checking. The Python type system also uses ``...`` within :ref:`Callable` types and @@ -88,7 +88,7 @@ not all Python objects have an attribute ``foo``. An expression typed as :ref:`Any`, on the other hand, should be assumed to have _some_ specific static type, but _which_ static type is not known. A static type checker should not emit static type errors on an expression or statement -if :ref:`Any` might represent a static type which would avoid the error. (This +if :ref:`!Any` might represent a static type which would avoid the error. (This is defined more precisely below, in terms of materialization and assignability.) @@ -97,13 +97,13 @@ Similarly, a gradual type such as ``tuple[int, Any]`` (see :ref:`tuples`) or Python objects; rather, it represents a (bounded) range of possible sets of values. -In the same way that ``Any`` does not represent "the set of all Python objects" -but rather "an unknown set of objects", ``tuple[int, Any]`` does not represent -"the set of all length-two tuples whose first element is an integer." That is a -fully static type, spelled ``tuple[int, object]``. By contrast, ``tuple[int, -Any]`` represents some unknown set of tuple values; it might be the set of all -tuples of two integers, or the set of all tuples of an integer and a string, or -some other set of tuple values. +In the same way that :ref:`Any` does not represent "the set of all Python +objects" but rather "an unknown set of objects", ``tuple[int, Any]`` does not +represent "the set of all length-two tuples whose first element is an integer". +That is a fully static type, spelled ``tuple[int, object]``. By contrast, +``tuple[int, Any]`` represents some unknown set of tuple values; it might be +the set of all tuples of two integers, or the set of all tuples of an integer +and a string, or some other set of tuple values. In practice, this difference is seen (for example) in the fact that we can assign an expression of type ``tuple[int, Any]`` to a target typed as @@ -112,7 +112,7 @@ int]`` is a static type error. (Again, we formalize this distinction in the below definitions of materialization and assignability.) In the same way that the fully static type ``object`` is the upper bound for -the possible sets of values represented by ``Any``, the fully static type +the possible sets of values represented by :ref:`Any`, the fully static type ``tuple[int, object]`` is the upper bound for the possible sets of values represented by ``tuple[int, Any]``. @@ -121,7 +121,7 @@ The gradual guarantee :ref:`Any` allows gradually adding static types to a dynamically typed program. In a fully dynamically typed program, a static checker assigns the type -:ref:`Any` to all expressions, and should emit no errors. Inferring static +:ref:`!Any` to all expressions, and should emit no errors. Inferring static types or adding type annotations to the program (making the program more statically typed) may result in static type errors, if the program is not correct or if the static types aren't able to fully represent the runtime @@ -171,16 +171,16 @@ represented by ``str``. Such types can be called "nominal types" and this is Other types (e.g. :ref:`Protocols` and :ref:`TypedDict`) instead describe a set of values by the types of their attributes and methods, or the types of their -dictionary keys and values. These are called "structural types." A structural +dictionary keys and values. These are called "structural types". A structural type may be a subtype of another type without any inheritance or subclassing relationship, simply because it meets all the requirements of the supertype, and perhaps adds more, thus representing a subset of the possible values of the -supertype. This is "structural subtyping." +supertype. This is "structural subtyping". Although the means of specifying the set of values represented by the types differs, the fundamental concepts are the same for both nominal and structural -types: the type represents a set of possible values and a subtype represents a -subset of the values. +types: a type represents a set of possible values and a subtype represents a +subset of those values. Materialization --------------- @@ -224,7 +224,7 @@ A gradual type ``A`` is consistent with a gradual type ``B``, and ``B`` is consistent with ``A``, if and only if there exists some fully static type ``C`` which is a materialization of both ``A`` and ``B``. -``Any`` is consistent with every type, and every type is consistent with +:ref:`Any` is consistent with every type, and every type is consistent with ``Any``. (This follows from the definitions of materialization and consistency but is worth stating explicitly.) @@ -249,7 +249,7 @@ consistent subtype of a type ``A`` if there exists a materialization ``A'`` of fully static types, and ``B'`` is a subtype of ``A'``. Consistent subtyping defines "assignability" for Python. An expression can be -assigned to a variable (including passed as a parameter or returned from a +assigned to a variable (including passed as an argument or returned from a function) if its type is a consistent subtype of the variable's type annotation (respectively, parameter's type annotation or return type annotation). @@ -262,7 +262,7 @@ In the remainder of this specification, we will usually prefer the term "assignable to" is shorter, and may communicate a clearer intuition to many readers. -For example, ``Any`` is assignable to ``int``, because ``int`` is a +For example, ``Any`` is :term:`assignable` to ``int``, because ``int`` is a materialization of ``Any``, and ``int`` is a subtype of ``int``. The same materialization also shows that ``int`` is assignable to ``Any``. @@ -378,7 +378,7 @@ objects is an unknown set of objects. Union with None ~~~~~~~~~~~~~~~ -One common case of union types are *optional* types, which are a union with +One common case of union types are *optional* types, which are unions with ``None``. Example:: def handle_employee(e: Employee | None) -> None: ... diff --git a/docs/spec/generics.rst b/docs/spec/generics.rst index e9acbecb..8637aa14 100644 --- a/docs/spec/generics.rst +++ b/docs/spec/generics.rst @@ -2469,9 +2469,10 @@ See :pep:`PEP 544 details on the behavior of TypeVars bound to protocols. Checking a class for assignability to a protocol: If a protocol uses ``Self`` -in methods or attribute annotations, then a class ``Foo`` is assignable to the -protocol if its corresponding methods and attribute annotations use either -``Self`` or ``Foo`` or any of ``Foo``’s subclasses. See the examples below: +in methods or attribute annotations, then a class ``Foo`` is :term:`assignable` +to the protocol if its corresponding methods and attribute annotations use +either ``Self`` or ``Foo`` or any of ``Foo``’s subclasses. See the examples +below: :: diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 6427dae7..d1b8db89 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -16,9 +16,9 @@ This section defines a few terms that may be used elsewhere in the specification If a type ``B`` is "assignable to" a type ``A``, a type checker should not error on the assignment ``x: A = b``, where ``b`` is some expression whose type is ``B``. Similarly for function calls and returns: ``f(b)`` - where ``def f(x: A): ...`` and ``return b`` inside ``def f(...) -> A:`` - are both valid (not a type error) if and only if ``B`` is assignable to - ``A``. In this case ``A`` is "assignable from" ``B``. For :term:`fully + where ``def f(x: A): ...`` and ``return b`` inside ``def f(...) -> A: + ...`` are both valid (not type errors) if and only if ``B`` is assignable + to ``A``. In this case ``A`` is "assignable from" ``B``. For :term:`fully static types `, "assignable to" is equivalent to ":term:`subtype` of" and "assignable from" is equivalent to ":term:`supertype` of". For :term:`gradual types `, a type @@ -86,10 +86,10 @@ This section defines a few terms that may be used elsewhere in the specification materialize A :term:`gradual type` can be materialized to a more static type - (possibly a :term:`fully static type`) by replacing :ref:`Any` with a - type, or by replacing the `...` in a :ref:`Callable` type with a list of - types, or by replacing ``tuple[Any, ...]`` with a specific-length tuple - type. This materialization relation is key to defining + (possibly a :term:`fully static type`) by replacing :ref:`Any` with any + other type, or by replacing the `...` in a :ref:`Callable` type with a + list of types, or by replacing ``tuple[Any, ...]`` with a specific-length + tuple type. This materialization relation is key to defining :term:`assignability ` for gradual types. See :ref:`type-system-concepts`. @@ -102,8 +102,8 @@ This section defines a few terms that may be used elsewhere in the specification :term:`equivalent` to ``A``. This means that ``B`` represents a proper subset of the possible objects represented by ``A``. "Type narrowing" is when a type checker infers that a name or expression must have a narrower - type at some locations in control flow, due to some runtime check of its - value. + type at some locations in control flow, due to an assignment or a runtime + check of its value. nominal A nominal type (e.g. a class name) represents the set of values whose @@ -143,7 +143,10 @@ This section defines a few terms that may be used elsewhere in the specification ``A``. For :term:`nominal` types (classes), subtyping is defined by inheritance. For :term:`structural` types, subtyping is defined by a shared set of attributes/methods or keys. Subtype is the inverse of - :term:`supertype`. See :ref:`type-system-concepts`. + :term:`supertype`. Types that are not fully static are not a subtype or + supertype of any other type, but via :term:`materialization + ` they can be :term:`assignable` to another type. See + :ref:`type-system-concepts`. supertype A :term:`fully static type` ``A`` is a supertype of a fully static type diff --git a/docs/spec/protocol.rst b/docs/spec/protocol.rst index 98a720f2..e280f0ed 100644 --- a/docs/spec/protocol.rst +++ b/docs/spec/protocol.rst @@ -24,7 +24,7 @@ when referring to the static type concept. If a class includes a protocol in its MRO, the class is called an *explicit* subclass of the protocol. If a class defines all attributes and methods of a -protocol with types that are assignable to the types of the protocol's +protocol with types that are :term:`assignable` to the types of the protocol's attributes and methods, it is said to implement the protocol and to be assignable to the protocol. If a class is assignable to a protocol but the protocol is not included in the MRO, the class is *implicitly* assignable to From 6a3b7165c71d1b28807b8bd6ae142edc2f040dc1 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Wed, 19 Jun 2024 19:07:52 -0600 Subject: [PATCH 44/45] Update glossary.rst Co-authored-by: Alex Waygood --- docs/spec/glossary.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index d1b8db89..41bb2b58 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -143,9 +143,9 @@ This section defines a few terms that may be used elsewhere in the specification ``A``. For :term:`nominal` types (classes), subtyping is defined by inheritance. For :term:`structural` types, subtyping is defined by a shared set of attributes/methods or keys. Subtype is the inverse of - :term:`supertype`. Types that are not fully static are not a subtype or + :term:`supertype`. A type that is not fully static is not a subtype or supertype of any other type, but via :term:`materialization - ` they can be :term:`assignable` to another type. See + ` can be :term:`assignable` to another type. See :ref:`type-system-concepts`. supertype From ab7f9acdf85abf0db85183939bf459f610fdb0b7 Mon Sep 17 00:00:00 2001 From: Carl Meyer Date: Thu, 20 Jun 2024 16:39:41 -0500 Subject: [PATCH 45/45] review comments --- docs/spec/concepts.rst | 31 +++++++++++++++++-------------- docs/spec/glossary.rst | 6 +++--- 2 files changed, 20 insertions(+), 17 deletions(-) diff --git a/docs/spec/concepts.rst b/docs/spec/concepts.rst index 854e64b3..058a5794 100644 --- a/docs/spec/concepts.rst +++ b/docs/spec/concepts.rst @@ -52,7 +52,8 @@ We will refer to types that do not contain a :term:`gradual form` as a sub-part as **fully static types**. A **gradual type** can be a fully static type, :ref:`Any` itself, or a type -that contains a gradual form as a sub-part. +that contains a gradual form as a sub-part. All Python types are gradual types; +fully static types are a subset. Fully static types ~~~~~~~~~~~~~~~~~~ @@ -92,10 +93,9 @@ if :ref:`!Any` might represent a static type which would avoid the error. (This is defined more precisely below, in terms of materialization and assignability.) -Similarly, a gradual type such as ``tuple[int, Any]`` (see :ref:`tuples`) or -``int | Any`` (see :ref:`union-types`) does not represent a single set of -Python objects; rather, it represents a (bounded) range of possible sets of -values. +Similarly, a type such as ``tuple[int, Any]`` (see :ref:`tuples`) or ``int | +Any`` (see :ref:`union-types`) does not represent a single set of Python +objects; rather, it represents a (bounded) range of possible sets of values. In the same way that :ref:`Any` does not represent "the set of all Python objects" but rather "an unknown set of objects", ``tuple[int, Any]`` does not @@ -193,11 +193,11 @@ types described above. To relate gradual types more generally, we define a **materialization** relation. Materialization transforms a "more dynamic" type to a "more static" type. Given a gradual type ``A``, if we replace zero or more occurrences of -``Any`` in ``A`` with some gradual type (which can be different for each -occurrence of ``Any``), the resulting gradual type ``B`` is a materialization -of ``A``. (We can also materialize a :ref:`Callable` type by replacing ``...`` -with any type signature, and materialize ``tuple[Any, ...]`` by replacing it -with a determinate-length tuple type.) +``Any`` in ``A`` with some type (which can be different for each occurrence of +``Any``), the resulting gradual type ``B`` is a materialization of ``A``. (We +can also materialize a :ref:`Callable` type by replacing ``...`` with any type +signature, and materialize ``tuple[Any, ...]`` by replacing it with a +determinate-length tuple type.) For instance, ``tuple[int, str]`` (a fully static type) and ``tuple[Any, str]`` (a gradual type) are both materializations of ``tuple[Any, Any]``. ``tuple[int, @@ -225,8 +225,8 @@ consistent with ``A``, if and only if there exists some fully static type ``C`` which is a materialization of both ``A`` and ``B``. :ref:`Any` is consistent with every type, and every type is consistent with -``Any``. (This follows from the definitions of materialization and consistency -but is worth stating explicitly.) +:ref:`!Any`. (This follows from the definitions of materialization and +consistency but is worth stating explicitly.) The consistency relation is not transitive. ``tuple[int, int]`` is consistent with ``tuple[Any, int]``, and ``tuple[Any, int]`` is consistent with @@ -311,7 +311,7 @@ In Python, we can do more with objects at runtime than just assign them to names, pass them to functions, or return them from functions. We can also get/set attributes and call methods. -In the Python object model, the operations that can be performed on a value all +In the Python data model, the operations that can be performed on a value all desugar to method calls. For example, ``a + b`` is (roughly, eliding some details) syntactic sugar for either ``type(a).__add__(a, b)`` or ``type(b).__radd__(b, a)``. @@ -319,7 +319,10 @@ details) syntactic sugar for either ``type(a).__add__(a, b)`` or For a static type checker, accessing ``a.foo`` is a type error unless all possible objects in the set represented by the type of ``a`` have the ``foo`` attribute. (We consider an implementation of ``__getattr__`` to be a getter for -all attribute names, and similarly for ``__setattr__`` and ``__delattr__``.) +all attribute names, and similarly for ``__setattr__`` and ``__delattr__``. +There are more `complexities +`_; +a full specification of attribute access belongs in its own chapter.) If all objects in the set represented by the fully static type ``A`` have a ``foo`` attribute, we can say that the type ``A`` has the ``foo`` attribute. diff --git a/docs/spec/glossary.rst b/docs/spec/glossary.rst index 41bb2b58..791782e7 100644 --- a/docs/spec/glossary.rst +++ b/docs/spec/glossary.rst @@ -54,7 +54,7 @@ This section defines a few terms that may be used elsewhere in the specification fully static type A type is "fully static" if it does not contain any :term:`gradual form`. - Fully static types represent a set of possible runtime values. Fully + A fully static type represents a set of possible runtime values. Fully static types participate in the :term:`subtype` relation. See :ref:`type-system-concepts`. @@ -68,8 +68,8 @@ This section defines a few terms that may be used elsewhere in the specification other :ref:`tuple ` types). gradual type - 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 + 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