Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

new "type system concepts" section #1743

Merged
merged 48 commits into from
Jun 24, 2024
Merged
Show file tree
Hide file tree
Changes from 47 commits
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
b323afb
initial draft of new concepts section
carljm May 22, 2024
bd4416e
review feedback
carljm May 22, 2024
3c332bf
prefer 'assignable to' over 'consistent subtype of'
carljm May 22, 2024
6603f43
minor tweaks
carljm May 22, 2024
4e2a1ce
Merge branch 'main' into concepts
carljm May 22, 2024
137ab2a
terms have types
carljm May 22, 2024
24e6ee5
review comments
carljm May 22, 2024
9e9ebb4
use asymmetric example of assignable-to
carljm May 22, 2024
1271558
Any is equivalent to Any
carljm May 22, 2024
2ddd4ad
add a short para on the gradual guarantee
carljm May 22, 2024
971e9f2
conciseness tweak
carljm May 22, 2024
10fda4e
use 'assignable to' in Any description
carljm May 22, 2024
f4110bb
incorporate some of Eric Traut's feedback
carljm May 23, 2024
ac6273e
more on union
carljm May 24, 2024
15c0d56
add an example of bounded gradual type
carljm May 24, 2024
efdbc5f
add section on attributes and methods
carljm May 24, 2024
e4537ac
more feedback and tweaks
carljm May 26, 2024
c3bbb52
Merge branch 'main' into concepts
carljm Jun 1, 2024
6bebab4
review comments
carljm Jun 1, 2024
2900cce
a bit more on gradual unions
carljm Jun 1, 2024
182a058
a few more review comments
carljm Jun 1, 2024
351136e
add terms to glossary
carljm Jun 1, 2024
cd03de8
Update glossary.rst
carljm Jun 2, 2024
07941d7
Update glossary.rst
carljm Jun 2, 2024
c55d40a
review comments on glossary
carljm Jun 2, 2024
b1775b1
re-apply review comment
carljm Jun 2, 2024
1a71a72
Apply suggestions from code review
carljm Jun 2, 2024
c18d9e1
audit remainder of type spec for terminology usage
carljm Jun 2, 2024
cca3bcd
review comments
carljm Jun 2, 2024
3d6b406
some review comments
carljm Jun 2, 2024
5d40036
one more review tweak on protocol wording
carljm Jun 2, 2024
1e0d118
Merge branch 'main' into concepts
carljm Jun 12, 2024
cbe6e23
add equivalent, narrow, and wide to glossary
carljm Jun 12, 2024
8954595
add table of type relations
carljm Jun 12, 2024
efaa7ab
explicitly allow inference on missing function annotations
carljm Jun 12, 2024
12ae9eb
some review comments
carljm Jun 12, 2024
ccfef86
Update docs/spec/callables.rst
carljm Jun 12, 2024
e990bda
more review comments
carljm Jun 12, 2024
045d7c2
link 'assignable' to glossary more often in callables doc
carljm Jun 14, 2024
dd6ffd1
add nominal/structural to concepts and glossary
carljm Jun 14, 2024
673a467
don't use 'compatible' in callables doc
carljm Jun 14, 2024
0f5fba4
equivalence of gradual types and union simplification
carljm Jun 14, 2024
a6b3ab0
simplify description of structural subtyping
carljm Jun 15, 2024
e5943a4
define equivalence of gradual types in glossary
carljm Jun 15, 2024
effcdec
more review comments
carljm Jun 17, 2024
9ebaef8
review comments
carljm Jun 19, 2024
6a3b716
Update glossary.rst
carljm Jun 20, 2024
ab7f9ac
review comments
carljm Jun 20, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions docs/spec/annotations.rst
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,18 @@ 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 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.

It is recommended but not required that checked functions have
annotations for all arguments and the return type. For a checked
Expand Down
162 changes: 81 additions & 81 deletions docs/spec/callables.rst
carljm marked this conversation as resolved.
Show resolved Hide resolved

Large diffs are not rendered by default.

7 changes: 4 additions & 3 deletions docs/spec/class-compat.rst
carljm marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
.. _`class-compat`:

Class type compatibility
Class type assignability
========================

.. _`classvar`:
Expand Down Expand Up @@ -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
:term:`assignable` to the type of the overridden method.


.. code-block:: python
Expand Down
382 changes: 374 additions & 8 deletions docs/spec/concepts.rst

Large diffs are not rendered by default.

15 changes: 8 additions & 7 deletions docs/spec/constructors.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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.

::

Expand Down Expand Up @@ -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.
carljm marked this conversation as resolved.
Show resolved Hide resolved

::

Expand All @@ -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 the type of a class object can be
:term:`assignable` to a callable type.

::

Expand Down
6 changes: 0 additions & 6 deletions docs/spec/directives.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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
carljm marked this conversation as resolved.
Show resolved Hide resolved
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``
Expand Down
2 changes: 1 addition & 1 deletion docs/spec/enums.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
81 changes: 39 additions & 42 deletions docs/spec/generics.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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=<type>`` (when
using the ``TypeVar`` constructor) or using ``: <type>`` (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::
A type variable may specify an upper bound using ``bound=<type>`` (when using
the ``TypeVar`` constructor) or using ``: <type>`` (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
Expand All @@ -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
carljm marked this conversation as resolved.
Show resolved Hide resolved
*exactly* one of the constraint types, while an upper bound just requires that
the actual type is :term:`assignable` to the bound.

.. _`variance`:

Expand All @@ -523,13 +522,12 @@ introduction to these concepts can be found on `Wikipedia
<https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29>`_ 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
Expand Down Expand Up @@ -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 :term:`assignable` to ``T2``'s bound.

::

Expand Down Expand Up @@ -2022,8 +2020,8 @@ normal subscription rules, non-overridden defaults should be substituted.
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
If both ``bound`` and ``default`` are passed, ``default`` must be
:term:`assignable` to ``bound``. If not, the type checker should generate an
error.

::
Expand Down Expand Up @@ -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 :term:`assignable` to the current
class.

::

Expand Down Expand Up @@ -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 assignable to
# OrdinalLinkedList, but the type checker allows it.
xs = OrdinalLinkedList(value=1, next=LinkedList[int](value=2))

if xs.next:
Expand Down Expand Up @@ -2469,11 +2468,11 @@ 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 :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:

::

Expand Down Expand Up @@ -2705,16 +2704,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
carljm marked this conversation as resolved.
Show resolved Hide resolved
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.
Expand All @@ -2737,9 +2735,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:

Expand Down
Loading