Skip to content

PEP 747: a few suggested updates #4230

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.

Sign up for GitHub

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

Closed
wants to merge 3 commits into from
Closed

PEP 747: a few suggested updates #4230

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7385382
PEP 747: a few suggested updates
carljm Jan 24, 2025
e8c2576
simplify example
carljm Jan 25, 2025
ac65ab9
TypeForm means TypeForm[Any]
carljm Jan 25, 2025
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
53 changes: 31 additions & 22 deletions peps/pep-0747.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,11 +200,15 @@ that represent a type assignable to ``str | None``::
err1: TypeForm[str | None] = str | int # Error
err2: TypeForm[str | None] = list[str | None] # Error

By this same definition, ``TypeForm[Any]`` describes a type form object
that represents the type ``Any`` or any type that is assignable to ``Any``.
Since all types in the Python type system are assignable to ``Any``,
``TypeForm[Any]`` describes the set of all type form objects
evaluated from all valid type expressions.
By this same definition, ``TypeForm[object]`` describes a type form object that
represents the type ``object`` or any type that is assignable to ``object``.
Since all types in the Python type system are assignable to ``object``,
``TypeForm[object]`` describes the set of all type form objects evaluated from
all valid type expressions.
Comment on lines +203 to +207
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything said here applies to TypeForm[object], so it seems simpler and clearer to simply describe TypeForm[object], and avoid the tendency to wrongly conflate Any and object. To precisely describe TypeForm[Any] would require further discussion of gradual types, which is already present in the spec and doesn't seem necessary here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did end up needing to describe TypeForm[Any], in order to maintain that bare TypeForm has that meaning.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't have a strong opinion about whether to use TypeForm[object] or TypeForm[Any] in this text. If you feel that object is clearer, I'm fine with the change.


``TypeForm[Any]`` describes a ``TypeForm`` type whose type argument is not
statically known, and is thus assignable both to and from any other
``TypeForm`` type (because ``Any`` is assignable both to and from any type.)

The type expression ``TypeForm``, with no type argument provided, is
equivalent to ``TypeForm[Any]``.
Expand Down Expand Up @@ -289,9 +293,9 @@ This explicit syntax serves two purposes. First, it documents the developer's
intent to use the value as a type form object. Second, static type checkers
validate that all rules for type expressions are followed::

x4 = type(int) # No error, evaluates to "type[int]"
x4 = type(1) # No error, evaluates to "type[int]"

x5 = TypeForm(type(int)) # Error: call not allowed in type expression
x5 = TypeForm(type(1)) # Error: call not allowed in type expression


Assignability
Expand Down Expand Up @@ -533,21 +537,26 @@ of ``type``.
Treat ``type[T]`` as a subtype of ``TypeForm[T]``
-------------------------------------------------

It was suggested that type ``type[T]`` should be considered a subtype
of ``TypeForm[T]``. This was ultimately rejected because there are ways to
create an object of type ``type[T]`` that does not encode a valid type expression.
For example, the expression ``type[1]`` is not a valid type expression. Likewise,
the expression ``type[S]`` is not a valid type expression if ``S`` is an
out-of-scope type variable. This same argument applies to other special forms
like objects of type ``UnionType``, which may or may not encode a valid type
expression. Rather than carving out a special case for ``type[T]`` that would
allow for potential unsoundness, it was decided to treat all type forms
consistently. Therefore, ``type[T]`` is not considered a subtype of ``TypeForm[T]``.

It was also pointed out that the expression ``C | C`` (where ``C`` is a class
object) is a valid type expression - and therefore a valid ``TypeForm``,
but its runtime type form encoding is an instance of ``UnionType`` and
therefore is not compatible with ``type[C]``.
It was suggested that type ``type[T]`` should be considered a subtype of
``TypeForm[T]``. This is intuitive because, given a class ``C``, the expression
``C`` both evaluates at runtime to the type object ``C`` (which inhabits the
type ``type[C]``), and is also a valid type expression spelling the type ``C``
(therefore also inhabits the type ``TypeForm[C]``).

The problem is that there are other expressions (for example,
``C().__class__``), which also evaluate to the class object ``C``, but are not
valid type expressions spelling the type ``C``, therefore should not inhabit
``TypeForm[C]``. In order to maintain consistency that ``TypeForm`` types may
only originate in valid type expressions, we say that ``type[T]`` is not a
subtype of ``TypeForm[T]``. (This implies that the type system considers the
objects resulting from ``C`` and ``C().__class__`` to be distinguishable, in
that the former is a valid ``TypeForm`` and the latter is not, even though they
are identical at runtime.)

``TypeForm[T]`` is also not a subtype of ``type[T]``, because the expression
``C | C`` (where ``C`` is a class object) is a valid type expression - and
therefore a valid ``TypeForm``, but its runtime type form encoding is an
instance of ``UnionType`` and therefore does not inhabit ``type[C]``.
Comment on lines +540 to +559
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The rationale for these changes is described more fully in comments on #4204

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't agree with this change. My previous wording explains my argument for why type[T] cannot be a subtype of TypeForm[T]. I guess that you still don't agree with (or understand) my argument.

The argument you make above doesn't make sense to me as a justification for this limitation. If this reasoning makes sense to you and it's enough to convince you that type[T] cannot be a subtype of TypeForm[T], then it's probably not worth debating this any further because we've reached the same conclusion. However, as co-author of the PEP, I'd prefer to revert this change so the PEP accurately reflects my understanding.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, the argument currently made in the text doesn't make sense to me; I explained why in #4204 (comment)

I feel uncomfortable moving forward with the PEP if we can't even reach an agreed description of why type[T] is not a subtype of TypeForm[T], because it suggests that the semantics of TypeForm[T] aren't clear enough even for you and I (after much discussion) to share an understanding of them, which seems to leave little chance of the rest of the world reaching a consistent understanding.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In re-reading my version, I agree it's not as clear as it could be. I'll take another run at modifying it to see if I can clear up the confusion.

Your proposed text doesn't make sense to me as a justification for excluding type[T] as a subtype of TypeForm[T]. I don't understand why C().__class__ is at all relevant to the argument. That is definitely not the argument I'm making for this limitation.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll be happy to look at your updated version!

Perhaps the specific choice of C().__class__ is confusing. That particular expression is unimportant. It could just as well be any expression that evaluates at runtime to the class object C (and would be typed by a type checker as type[C]), but is not a valid type expression.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, on further reflection I'm beginning to think that my argument against it is circular, and that type[C] should be a subtype of TypeForm[C]. Ultimately my argument boiled down to the idea that anywhere we see an expression in context of a TypeForm annotation, it should be a valid type expression. But that's already not true, because the expression might be a value expression which evaluates to a TypeForm type, e.g. a call to a function which returns a TypeForm. So we can't avoid the need for potentially double evaluation (first as value expression, then as type expression) of expressions in TypeForm context.

So I will wait for your argument, to see if the updated version of it makes more sense to me. I think what would really clarify is a code example, which would pass a type checker with no errors if type[C] were a subtype of TypeForm[C], but results in some kind of unsoundness.


If a function wishes to indicate that it accepts values of type ``TypeForm[T]``
_and_ ``type[T]``, the parameter can simply be annotated with a union of these
Expand Down
Loading