Clarifications to the typing spec regarding `type[]`

Typing
,
1

Reading through the typing spec and conformance test suite, I have discovered a number of inconsistencies and ambiguities regarding type[] which I believe should be clarified. Some of these I would consider uncontroversial bugs in the spec; others require discussion before we can update the specification. I list the uncontroversial ones first before detailing the ambiguous points at the end which I believe may require discussion.

Inconsistencies in the grammar for type expressions

The grammar at Type annotations — typing documentation currently permits only the following constructs inside type[]:

| <type> '[' <Any> ']'
| <type> '[' name ']'
   (where name must refer to a valid in-scope class
     or TypeVar)

This would incorrectly imply that the following are invalid type expressions:

  • type[Union[str, int]], type[Optional[int]] and type[int | str]. PEP 484 stated:

    Note that it is legal to use a union of classes as the parameter for Type[], as in:

    def new_non_team_user(user_class: Type[Union[BasicUser, ProUser]]):
    user = new_user(user_class)
    ...

    And this wording has been carried over into the spec at Special types in annotations — typing documentation. The grammar should reflect that these are valid type expressions.

  • type[Self]. It’s clearly specified in PEP 673 and the spec at Generics — typing documentation that type[Self] should be permitted.

  • type["quoted_forward_reference"]. I’m not sure it’s anywhere clearly stated that this should be permitted, but I think it follows naturally from various principles implied by the spec as a whole.

  • type[Annotated[int, "metadata]]. The spec at Type qualifiers — typing documentation states that:

    As with most special forms, Annotated is not type compatible with type or type[T]:

    v1: type[int] = Annotated[int, ""]  # Type error

SmallInt: TypeAlias = Annotated[int, ValueRange(0, 100)]
v2: type[Any] = SmallInt  # Type error

    However, it does not specify that Annotated[] should be disallowed inside type[]. Both mypy and pyright allow type[Annotated[int, "metadata"]], and I think it follows naturally from reading the spec that this should be allowed.

Other problems with the spec as written

There are also several problems with the spec at Special types in annotations — typing documentation where it states:

Any other special constructs [other than Union] like tuple or Callable are not allowed as an argument to type.

Firstly, this would appear to disallow type[Self] and type[Annotated[int, "metadata"]]; but, as discussed above, those should probably be permitted type expressions. Secondly, it would appear to disallow type[tuple] – but if this is disallowed, then it is impossible to express in the type system “the class object tuple, or any subclass of that class object”. It looks to me like this sentence was copied over from PEP 484’s equivalent sentence, but the syntax in the example has been incorrectly modernised. PEP 484 mentions "any other special constructs like Tuple and Callable. But whereas typing.Tuple was and is unambiguously a special form in the type system, builtins.tuple serves a dual role following PEP 585: it is simultaneously a special form and a concrete class. As a concrete class, I think it should be valid as an argument to type[].

Suggested improvements to the conformance suite

I suggest that we enhance the conformance suite to ensure that type checkers allow the following constructs:

type[Union[int, str]]
type[int | str]
type[Optional[int]]
type[Annotated[int, "metadata"]]
type[int | Optional[Annotated[str, "metadata"]]]
type[type]
type[tuple]
type["forward_reference"]

(N.B. type[Self] is already tested in the conformance suite tests for Self.)

And that type checkers disallow the following constructs:

type[Protocol]
type[Generic]
type[TypedDict]
type[NamedTuple]  # a factory function at runtime, not a class; this is unsound
type[Literal]
type[Literal[""]]
type[Unpack]
type[Unpack[Ts]]
type[LiteralString]
type[type[int]]
type[Callable]
type[Callable[[int], str]]
type[Tuple]

def foo(x: object) -> type[TypeGuard[str]]: ...

(N.B. x: type[int] = Annotated[int, ""] is already tested in the conformance suite tests for Annotated as something to be disallowed.)

Further ambiguities in the spec

The following questions all require discussion before we decide how to update the spec. I don’t think they would need to be clarified in the same PR as the above proposed clarifications.

  1. Should parameterised classes be acceptable as an argument to type? E.g. x: type[list[int]] = list. I can’t see how this is any more unsound than type[] in general (type checkers generally unsoundly assume that for the set of class objects described by type[T], all items in the set have the same constructor signature as T, which is incorrect). So I would vote “yes” for this question.
  2. Should parameterised tuples be acceptable as an argument to type? E.g. x: type[tuple[int, int]] = tuple. I think the only way to make this vaguely sound would be to require that type checkers synthesize an accurate constructor signature for x here – e.g. the synthesized signature in this instance would be def __new__(cls, tup: tuple[int, int], /) -> Self. If we don’t want to go down that route, I think we should ban type[tuple[int, int]]. On the other hand, I think x: type[tuple[int, ...]] = tuple should probably be allowed; again, it seems no more unsound than type[T] for any other T.
  3. Should it be allowed to use a TypedDict class as the argument to type[]? Currently both mypy and pyright permit this. I can see some use cases for it – if you want to introspect a TypedDict class’s __required_keys__ or __optional_keys__ class variables, for example. But it’s perhaps outside the scope of what type[] was originally intended for; whether or not this should be allowed, the spec should state it clearly.
  4. Should it be allowed to use a Protocol class as the argument to type[]? I know of at least one place where we do so in typeshed, so it’s not without its use cases. But at the very least, as with TypedDict classes, this is underspecified. Whether or not we decide that this should be allowed, the spec should give a clear statement on the matter.

Previous discussion on type[] in the spec

In Inconsistencies between `Type` and `type`, we previously discussed (and came to a consensus) on inconsistencies between type and Type, and the meaning of type[Any] in a type expression. The outcome of that discussion has yet to be reflected in the typing spec; those updates should also be made. (The points being made in this thread are distinct to the points discussed in the earlier thread.)

7 Likes
2

If this is allowed, that implies that type[None] should also be allowed (and should be listed separately as an allowed argument to type[]). Mypy indeed allows it, treating it as equivalent to type[types.NoneType]: mypy Playground. Pyright does too and behaves the same on this sample.

Otherwise, agree with your writeup.

2 Likes
3

Great point; I hadn’t properly considered the question of type[None]. This should have gone into the final section of debatable questions rather than the first section of hopefully-uncontroversial points.

I weakly prefer mypy’s behaviour here. Treating type[None] as type[types.NoneType] (as mypy does) makes sense, since when we use None in type annotations, we actually mean types.NoneType; mypy’s interpretation seems to follow naturally from that. On Python 3.10+, you can say what you mean more clearly by using type[types.NoneType], but that option isn’t available for people using older versions of Python.

4

One further question that I missed when writing this up is: should type[Never] (and type[NoReturn] be allowed in annotation expressions? Although it appears to be forbidden both by the typing spec’s prose describing the type[] special form and the typing spec’s formal grammar for annotation expressions, both mypy and pyright currently allow annotating a variable with type[Never]. It is also possible to get at least mypy to infer a variable as having type type[Never] in some situations where it fails to solve a TypeVar: mypy Playground.

Nonetheless, I would argue that type[Never] and type[NoReturn] should be forbidden in type annotations. I think the logical interpretation of type[Never] as a type is “the empty set of values, where all values would be class objects if there were actually any values in the set”. As a philosophical concept, that feels indistinguishable from Never and somewhat incoherent, so I see no use in changing the spec to explicitly allow Never or NoReturn in annotation expressions. (This does not forbid type checkers from having an internal representation of type[Never], though it does mean that they should treat a value inferred as having type type[Never] in exactly the same way as they would treat a value inferred as having type Never.)

I therefore also propose that we add tests to the conformance suite that ensure that type checkers emit an error complaining about an invalid annotation if an object is annotated as having type type[Never] or type[NoReturn].

2 Likes
5

Would your logic about Never apply more generally to type arguments for generic types? If we want to disallow type[Never], shouldn’t we also disallow list[Never]? What about Union[int, Never]? Clearly we shouldn’t disallow Callable[[Never], None] or Callable[[Any], NoReturn] because those have legit use cases.

My point is that if we want to disallow type[Never], it seems like we should try to define a more general principle for why it would be disallowed and then apply this same principle everywhere. I don’t know if that’s worth it though. Maybe we just leave it unspecified since no one has (to my knowledge) ever run into a problem with type[Never]?

6

I don’t think this is an option, since the typing spec already specifies in the grammar at Type annotations — typing documentation that type[Never] is not a legal annotation expression, and this is also implied by the prose description of type[] where the typing spec states that “any other special constructs [other than Union] like tuple and Callable are not valid as a type”. Some change must be made here one way or the other: both mypy and pyright are, strictly speaking, in violation of the spec as it is currently written when they allow variables to be annotated with type[Never].

Nonetheless, I agree that this is both a low-priority issue and one that should perhaps be considered in the broader context of when and if Never should be valid as an argument to a generic type. I’m fine with deferring the question for now.

7

Yeah, I agree that the grammar should be fixed. My suggestion is to simply remove <type> as a special case in the grammar and treat it just like any other generic class. After all, type is a class, not a special form. That would mean type[Never] would fall under the same grammar rule as, for example, list[Never]. There are additional semantic rules and limitations that apply for type, but those can be spelled out specifically for type outside of the grammar.

2 Likes
8

I feel somewhat reluctant to remove the <type> special case from the grammar, because there are so many constructs that are legal in type expressions generally but are not legal inside type[], and I think the grammar is a really useful way of clarifying the vast majority of these.

As a compromise position, perhaps for now we could update the grammar to reflect the “reality on the ground”, which is that type checkers view type[Never] as a legal annotation, but with the understanding that this could be reconsidered in the future.

2 Likes
9

I don’t see a reason to forbid this at the grammar level, there’s probably a reasonable interpretation for this (the one I see is that it’s a type that can’t exist), and it might be useful in either error messages or places where tests of exhaustiveness is happening.

type[Never] could be the result of type[int | str] after successive negative TypeIs checks, and it could be useful to leave type[Never] as that rather than instantly turning it to Never in some displays.

1 Like
10

What practical implications would this have as compared to the more general type Never? What differences would you expect to see in how type checkers treat variables with the two types respectively?

Sure – as I mentioned above, I don’t want to forbid type checkers having an internal representation of this type or even displaying it to users as an inferred type if they think it’s a helpful type for users. I think it naturally arises as an inferred type from situations where a type parameter is inferred as being impossible to solve, and probably in other situations I haven’t thought of as well.

There are many types that Python’s type checkers can (and must) have internal representations for, however, which are nonetheless inexpressible or illegal as type annotations. This debate is narrowly concerned with whether it makes sense to allow users to annotate a variable as being of type[Never]: does it ever make sense to do so? What would that imply? How would it be treated differently from Never by a type checker?

11

The practical interpretation I’m imagining is that type[Never] should behave identically to Never in the type system.

I can see an argument that if type[Never] should be identical to Never, then just tell users to type Never instead. However, I think this is better enforced by an opinionated linter, or even a message in a type checker (something like “info: This is equivalent to Never”), and not at the grammar level if there’s a reason that type checkers might use it in a display.

It would be a good goal if all types that arise from a type checker’s diagnostic messages are valid for a user to copy. While this isn’t the case currently, and there are uphill challenges to have that be the case in more places, the fewer internal types not denotable by users the better. It’s still something I’d prefer to help with user intuition and being able to use what they get as useful diagnostic output in other places.

This one in particular is not a strong preference, if other people feel like it’s definitely better to not have this in the type system, I’ve said what I intend and won’t argue this one.

5 Likes
12

I’d like to argue in favor of allowing the user to explicitly write type[Never]. Continuing with the type[str | int] example:

t: type[str | int]
if issubclass(t, str):
    assert_type(t, type[str])
    ...
elif issubclass(t, int):
    assert_type(t, type[int])
    ...
else:
    assert... # What do I write here?

In the last line, I would personally write assert_never(t), but I guess it would be legitimate if someone preferred assert_type(t, type[Never]) for consistency.

I’d also like to argue in favor of allowing Never as a type argument for generics. I’ve used Sequence[Never] and Mapping[Any, Never] when I wanted to specify that the container is empty (e.g. a variable of type Sequence[Never] can safely be used as argument to functions that want to iterate over the sequence and do something to each element; also, a function that accepts Sequence[Never] promises not to access the elements.)

As a last note, forbidding Union[int, Never] feels completely unnecessary – type checkers should just treat it as equivalent to int, and let linters complain about the redundancy.

2 Likes