Interactions with Never leading to undesirable assignability

Typing
36

It seems to me that you are making a hidden assumption here. Let’s completely ignore gradual typing and materialization for a second. Consider the following completely statically typed program:

from typing import TypedDict, Never

class ADictWithNever(TypedDict):
    never: Never

def func(d: ADictWithNever) -> None:
    assignable_to_never: Never = d

According to your logic, this should pass type checking. Both mypy and pyright currently don’t accept this. In fact, I think that they shouldn’t be allowed to accept this (more on that later).

Your argument seems to be that Never and ADictWithNever should be structurally equivalent types, because we “know” that they both denote an empty set of runtime values. I don’t think that you can actually prove that ADictWithNever denotes an empty set only using nominal/structural information that is available to the type system.

According to the definition of TypedDict, we know that ADictWithNever is a structural type that satisfies the following structural requirements:

  1. It is a dictionary object (and not a subtype of dict or Mapping, but dict specifically).
    Or in other words, type(d) == dict is guaranteed to be True.

  2. It is required to have a key named never.
    Or in other words, "never" in d is guaranteed to be True.

  3. The value of that key is of type Never.
    Or in other words, d["never"] is guaranteed to be assignable to Never.

  4. (and a bunch of other similar structural requirements, the exact list of which is seemingly never actually explicitly specified as if it is obvious, but seems to boil down to “d quacks like a dict that has a "never" key with a value of type Never”)

Now, as a human, you know how dict is actually implemented and so you can infer that it’s impossible to construct a dict that __contains__("never") and also “never returns” from __getitem__("never"). And so you make a fairly reasonable inference that ADictWithNever must correspond to an empty set (of possible runtime values).

Type checkers on the other hand don’t have enough information about the runtime implementation details of the dict type to make such an inference. Type checkers only have access to nominal and structural type information, which is ratified in the various typing PEPs and encoded in typeshed hints (or sometimes hardcoded into the typecheckers themselves for information that can’t be directly expressed in the language).

From the perspective of the type checker, there might as well be some valid function

def create_adictwithnever_pretty_please() -> ADictWithNever: ...

that actually constructs a concrete object d, such that type(d) == dict and "never" in d is True and d["never"] raises a CantTouchThat exception or loops forever without returning or whatever. So from a type-theoretical perspective, ADictWithNever denotes some set of values, but the type system doesn’t have enough information about this set of values to prove that it is empty. And so ADictWithNever is not assignable to Never (which is provably empty by definition and thus distinct from ADictWithNever).

As an aside, I am not sure if this is actually specified anywhere, but I think that type checkers shouldn’t even be allowed to make inferences that can’t be completely derived from information that is “known” or expressed in the type system. Here’s a silly example:

def foo(v: int) -> None:
    if type(v) != int: return
    if v < 0: return
    if v > 0: return
    if v == 0: return
    # Clearly, the set of possible values of v is empty at this point, right?

    # Should type checkers be allowed to infer this fact?
    i_dont_think_so: Never = v

Unless and until a new typing PEP is accepted which formally defines the structural properties of ints, the above code ought to be rejected by type checkers, imho. The same applies to “containers that provably have at least one instance of Never”.

4 Likes