PEP 747: a few suggested updates #4230
Conversation
| 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. |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
I did end up needing to describe TypeForm[Any], in order to maintain that bare TypeForm has that meaning.
There was a problem hiding this comment.
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.
peps/pep-0747.rst
Outdated
| @@ -289,7 +295,7 @@ 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(int) # No error, evaluates to "type[type]" | |||
There was a problem hiding this comment.
The expression type(int) evaluates to the object builtins.type (because that is the type of the class int), which does not inhabit type[int].
Actually, I think it might be clearer to use type(1) and type[int] here instead, will push that update.
There was a problem hiding this comment.
Good catch.
More accurately, type(int) evaluates to type[type[int]], not type[type] (which is the same as type[type[Any]]).
There was a problem hiding this comment.
Yes (although I seem to recall noticing that there isn't consistent agreement among type checkers about whether type is type[Any] or type[object]).
In any case, I updated this example to use type(1) and type[int] instead; it makes the same point without getting into these weeds.
There was a problem hiding this comment.
I seem to recall noticing that there isn't consistent agreement among type checkers about whether type is
type[Any]ortype[object]).
The spec is clear on this point. type is equivalent to type[Any]. Mypy treats the two differently, which means that it's not conformant with the spec in this regard.
| 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]``. |
There was a problem hiding this comment.
The rationale for these changes is described more fully in comments on #4204
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
A few suggested updates to the text of PEP 747. Rationale for the changes commented inline, and at #4204
@erictraut I can't add you as an explicit review request, but would like for your feedback on these changes.
📚 Documentation preview 📚: https://pep-previews--4230.org.readthedocs.build/