Interactions with Never leading to undesirable assignability

Typing
1

This topic grew out of a ty issue, where it was argued that the current spec implies that tuple[Any] is assignable to Never. There was some discussion about whether this is true for tuples, but that discussion is orthogonal to the issue I’m raising here. The same problem appears less arguably with TypedDicts.

Consider two typeddicts:

from typing import Any, TypedDict

class TD1(TypedDict):
    a: int
    b: Any

class TD2(TypedDict):
    c: str
    d: Any

To check whether TD1 is assignable to TD2 (or vice versa), we check whether there is any pair of materializations of both such that one is a subtype of the other. And even though the two TypedDicts have different sets
of keys, there is such a pair of materializations: the materializations where the two instances of Any are substituted with Never. In both cases, a required key becomes of type Never. But a TypedDict must be an instance of dict (not a subclass) with those exact keys, and there cannot be a dict with a key b and no value. Therefore, TD1 with b materialized to Never and TD2 with d materialized to Never are both empty types, i.e., Never.

This means that strictly speaking, type checkers should accept code like this:

x: list[TD1] = list[TD2]()
y: TD1 = TD2()

This is obviously undesirable: these types appear clearly distinct, and users won’t expect an inner Any to expand out like this. Indeed, current type checkers won’t actually allow this.

Other places where this problem can arguably appear include:

  • Fixed-length tuples like tuple[Any], though there is an argument that because of the existence of tuple subclasses, tuple[Never] is an inhabited type and not equivalent to Never.
  • Classes with an attribute like x: Any, though here there’s room for discussion around whether attributes need to be necessarily set, and around descriptors.
  • Intersections like A & Any and B & Any become consistent with each other even if A and B are nonoverlapping types, because both can materialize to Never. But of course intersections are not a standardized part of the current type system.

I believe this is a problem because actual type checker behavior diverges from the rules implied by the spec, and the behavior of the type checkers is clearly the more useful choice. To make the theoretical framework in the spec useful, we have to change something in the spec.

Suggested solutions

(1) Guillaume Duboc via @carljm (link): Modifying assignability

But they also use an additional restriction on assignability (beyond just “consistent subtyping”). Any type which can materialize to Never is a consistent subtype of any other type which can materialize to Never, per the definition of consistent subtyping. But assignability is meant to establish that an inhabitant of one type can substitute for an inhabitant of another type – this is not meaningful in the absence of inhabitants. So for A to be assignable to B, they require both that A is a consistent subtype of B, and that, if the bottom or lower bound materialization of A is Never, that the upper bound or top materializations of A and B be non-disjoint. Another way to describe this is that there must be some object that can inhabit some possible materialization of both A and B, in order for A to be assignable to B.

This refers to the implementation of gradual typing in Elixir. Guillaume also shared a more formal definition of this relationship, which adds back the property that Never is a subtype of itself.

I think this is a promising approach but the formulation has a few problems:

  • The “top” and “bottom” materializations of a type are interesting concepts, but they’re not currently part of the spec for the Python type system, and there are technical reasons why the definitions used in Elixir may not work well in Python. I think in the future we may come up with a formalization that adds these concepts to Python, but I don’t think a suitable formalization exists yet.
  • The definition would lead to some undesirable results. Consider whether, given a class SubList[T](list[T]): pass, list[Any] is assignable to SubList[Any]. The bottom materialization of SubList[Any] is Never (since the class is invariant, so its specializations do not have any other common subtype), and Never is a subtype of some (in fact, all) materializations of list[Any], so SubList[Any] is a consistent subtype of list[Any]. And list[Any] and SubList[Any] are not disjoint types, since instances of say SubList[int]() are members of both the types list[int] and SubList[int] (because SubList is a subclass of list). Therefore, we find that list[Any] is assignable to SubList[Any].

I would propose the following formulation instead:

Given two gradual types A and B, A is assignable to B if either (a) both A and B are equivalent to Never or (b) there exists a pair of fully static materializations A’ and B’ of A and B such that A’ is a subtype of B’ and A’ is not equivalent to Never.

Corollaries:

  • Any is not assignable to Never. This would be the main user-visible change to type checker behavior resulting from this definition, but I think it’s a positive change: assignability to Never mostly comes up in the context of assert_never(), and if you use that, you probably don’t want it to succeed if the argument is of type Any.
  • However, this does not translate to “deeper” levels of types: Sequence[Any] is still assignable to Sequence[Never]. That is because Sequence[Never] is a possible materialization of Sequence[Any], and it is an inhabited type (it contains e.g. the empty tuple).
  • Assignability is no longer a synonym of consistent subtyping, as consistent subtyping lacks the special provision for Never.

(2) @mikeshardmind (link): Different understanding of Never

“Consistent subtyping requires that if the super type is inhabited, that the subtype can be as well” (not is, but can be. it doesnt require a proof that some type can exist, only that there is no knowledge that prohibits such a type from existing)

This requires a slight change in the understanding of Never, from a consistent subtype of all types, to a representation of the absence of the possibility of a value consistent with the available type information (which happens to be more accurate)

I may not fully understand this but I think it comes down to saying that Never is not a subtype of other inhabited types, only of itself. @mikeshardmind gives an example where Callable[[], Never] is no longer a subtype of Callable[[], int]. I think this would break a significant amount of code and make the type system less consistent. For example, a function may take an onerror callback typed as Callable[[something], object]; it should be allowed to pass a Callable[[something], Never] to let errors bubble up.

(3) My suggestion (link): No materialization to Never

A gradual type that is not Never cannot materialize to Never, or to any type equivalent to Never.

This means that a type like TypedDict[{"x": Any}] cannot materialize to TypedDict[{"x": Never}] (because that type is equivalent to Never), but a type like Callable[[], Any] can materialize to Callable[[], Never] (because this is an inhabited type).

I think this leads to similar results as (1) but creates a bigger hole in the foundational concepts of the type system, because Never in general is a meaningful type, and the definition of materialization is more useful when it remains included.

(4) Another suggestion: Distinct Nevers

This is another new idea (I hinted at it here): what if we just pretend that when Never comes up out of tuple[Never], it’s a different type than the Never that comes out of TypedDict[{"x": Never}], even though both types contain the same (empty) set of runtime values. I think this approach has some promise as an implementation technique within a type checker, but it’s very much inconsistent with a set-theoretic type system: after all, the empty set is the empty set. I list it here in case there is some way I missed to turn this idea into something that makes sense.

Recommendation

I believe the best fix is a modified definition of assignability (suggestion 1). Unless a better solution comes up, I’ll prepare a PR to the spec to make that change.

2 Likes
2

The docs for Never mention the bottom type

Never and NoReturn represent the bottom type, a type that has no members.

So it’s at least referred in the docs. Edit: my mistake, this is something different.

But my two cents, I’d lean towards the distinct nevers. From a set theoretic point of view, a tuple is a sequence of sets of types and the python type system allows merging of positional elements in the sequence so for a monadic style builder example:

type Builder[T1=Never, T2=Never, T3=Never] = Callable[[], tuple[T1, T2, T3]]

def insert_int[T1, T2, T3](builder: Builder[T1, T2, T3]) -> Builder[T1 | int, T2, T3]:
    ...

It’s been 10 years since I’ve studied set theory but from a typing theory tuple[Never] is a sequence of empty sets, which is a set containing a single member (as the empty set is unique, there is only one sequence of length 1 of empty sets). And this set does not intersect the set of empty sets of length 2, so tuple[Never] is distinct from tuple[Never, Never]. If those two are distinct and have a single member each, I’d say they’re logically distinct from Never which is the empty set.

Mappings would have a similar argument.

I think people have assumed that because there is no value that can materialize as a tuple of Never, the set is empty, but I think that assumption is incorrect. But, as I said, it’s been 10 years since I’ve done this stuff in detail.

Imaginary numbers really melted my brain though.

3

This isn’t quite what I meant, but I don’t think I expressed the ideas clearly enough in that issue. This is still an area I’m exploring independently of python’s type system currently, and trying to pull in only the “we must do this for sensible interpretations” portions of that back to python’s type system.

Multiple issues with Never have poor current implications, so it’s worth actually breaking them down into independent cases.

  1. Local narrowing from a conditional resulting in no valid runtime type. This one isn’t as trivial as it appears, but it means if we got here, one of two things is true. Either this is actually unreachable code, or some amount of type information isn’t accurate. Because python’s type system is both gradual and “open world assuming”, the function can be typed correctly, but the type information be “wrong” when called from an untyped caller. There’s better that can be done than what current type checkers do in this case to preserve the gradual guarantee but I don’t think this particular one is a pressing issue.

  2. User replacement of an annotation with Never to satisfy an otherwise unsatisfiable requirement. This one should be forbidden, but isn’t due to an incomplete set of definitions about callable types. For example:

class A:
    def foo(self, x: int, /) -> int:  ...

class B:
    def foo(self, x: int, /) -> str:  ...

class C(B, A):
    def foo(self, x: int, /) -> Never:  ...

This stems from an incorrect assessment of function types that doesn’t fully align with theory, but is difficult to reconcile appropriately without modeling effects that interrupt control flow separately from function types. The problem here is that this changes the domain of the method in subclassing, something only very loosely modeled in python currently. Replacing a function that can return for one that can’t clearly breaks ideas of substitution, but the way we’ve defined raising to be equivalent to a lack of a type is less than helpful in this case.

We can remedy this by disallowing user replacement of an inhabitable type annotation with an uninhabitable one without having to add an effects system, but the explanation of this may not be satisfying for many users without deeper explanations.

  1. Generics that require a value (pretty much anything that isn’t an empty container type) (edit: see below, edit too late for mailing list, return parameterization…), shouldn’t be possible to parameterize with Never in General, and Never should not be a valid materialization within those generics. Places where we know a value exists can’t be Never. If a type checker comes across this at any point while determining it is reachable code, something has gone wrong.

None of these directly rule out Sequence[Never]. I believe that we could rule it out intentionally for most parameterizations(see below, edit too late for mailing list, return parameterization) without negative consequences. If we went with this route, most generics that has exhausted all possible parameterizations would collapse to Never itself.

4

I missed a case in summarizing other work in the above, due to generic protocols with __call__ and Callable: with the interpretations above, Never would still be valid in the parameterization of generic return types.

5

Just to clarify, bottom materializations are a different concept than the bottom type already in Python’s type system. Jelle explains the concept in more detail here: Gradual negation types and the Python type system | Jelle Zijlstra

3 Likes
6

Thanks, sorry for any confusion!

7

Both pyright and mypy currently do not conform to typing spec in the following spec conformance test (Added a few more overload evaluation tests. by erictraut · Pull Request #1957 · python/typing · GitHub):

from typing import Any, assert_type, overload

@overload
def example5(obj: list[int]) -> list[int]: ...
@overload
def example5(obj: list[str]) -> list[str]: ...
def example5(obj: Any) -> list[Any]:
    return []

def check_example5(b: list[Any]) -> None:
    assert_type(example5(b), Any)  # ❌ expected "Any" but received "list[int]"

In NumPy, this non-conformance often causes incorrect result types to be inferred. For example, the widely used NDArray[T] type alias is roughly defined as ndarray[tuple[Any, ...], dtype[T]]. But because it uses a gradual tuple type to describe its shape, we’ll get incorrect results when overloaded:

# --snip--
@overload
def tolist(self: ndarray[tuple[()], dtype[generic[_T]]], /) -> _T: ...
@overload
def tolist(self: ndarray[tuple[int], dtype[generic[_T]]], /) -> list[_T]: ...
# --snip--
@overload
def tolist(self, /) -> Any: ...

With this, calling a.tolist() on some a: NDArray[T] will be inferred as T instead of Any.

As far as I’m aware, the only way to work around this, is by (mis)using Never:

@overload
def tolist(self: ndarray[tuple[Never], dtype[generic[_T]]], /) -> Any: ...
@overload
def tolist(self: ndarray[tuple[()], dtype[generic[_T]]], /) -> _T: ...
# --snip--

This works because Any is the only “type” that’s assignable to Never, causing greedy overload evaluation implementations to select that first overload. The result is that a.tolist() will now be inferred as Any, as desired.

If Any would not be assignable to Never anymore (pun intended) before mypy and pyright conform to the typing spec for overload evaluation, then this will workaround won’t work anymore.

Just to be clear: I’m not saying that using Never like this is a good idea or anything. I would much rather have mypy and pyright conform to the spec here, so that we can get rid of those overloads.

And although I have my doubts about Any not being assignable to Never is theoretically sound, I’m not against this per se. Apart from this sketchy overload workaround, I’m not aware of any other situations where this could lead to problems. And the hope is that those Never overload workarounds will be needed nevermore ;).

1 Like
8

To elaborate a bit on this: if Any is not assignable to Never, then Any and Never must be disjoint, thus Any | Never cannot be reduced to a simpler form. But by definition, T | Never reduces to T for all types T, which leads to a logical contradiction when T: Any.

It’s not impossible to work around this, but doing so will require adding even more special cases for Any to the spec. So I’m just not sure if that additional complexity will be worth it.

9

This doesn’t require special casing to accomplish. It would mean changing the definition of assignability such that consistent subtyping is not the only requirement for assignability.

In that framing, Never is still an empty set of types, which leaves T | Never = T for all T, Any or otherwise, it’s just simply disallowed to assign an uninhabitable value to an inhabited type, or to treat an uninhabited type as a valid replacement for an inhabited one.

1 Like
10

I think Eric made the point, the presence of Never may not mean an uninhabitable value, eg user defined class, I’ve used Never as a “not set”, so what would be the rules for inferring habitability?

11

I clearly don’t understand how this type algebra works. With sets if A and B are disjoint then A | B cannot be simplified but A & B would be the empty set ∅.

How do you get that Any | Never must be Never here?

1 Like
12

Oh yea woops; brainfart. Any | Never will then instead be not reducible to a simpler form, which still leads to a contradiction. I’ll update it.

13

This is (wrongly) assuming that assignability must be equivalent to (consistent) subtyping. The point of this proposal is to place additional constraints on assignability (so as to avoid undesirable assignability of many gradual types that can materialize to Never), without changing the definition of materialization or consistent subtyping at all. So the proposal has zero implications for the disjointness or simplification of Any | Never.

2 Likes
14

I don’t think this is true. It is true that people sometimes try to use Never to indicate something like “not set”, but these are mis-uses and (AFAIK) not supported by the typing spec. (And if there is language in the typing spec that implies this, it should be removed.) Never is the bottom or uninhabited type, full stop.

1 Like
15

But what it is doesn’t constrain how it’s used. See the monad builder esque example I gave above. I’m using “not set” here to mean “empty set of types”.

16

I don’t think this is right. I’m not sure what it means to say the tuple[Never] is “a sequence of empty sets.” It is the set of all length-one tuples whose single element is uninhabited. This type isn’t inhabited by one object, it is uninhabited. No such object can exist. That is, tuple[Never] is equivalent to Never. So is tuple[Never, Never]. All of these are the uninhabited type.

1 Like
17

I guess I’m thinking set theory more than type theory

18

Thanks @Jelle for writing this up! I like your formulation of option 1.

I am a bit concerned about the backward compatibility implications (one case of which was highlighted by @jorenham) of changing things such that Any is no longer assignable to Never.

Is there an alternative formulation where if B is exactly Never, then A’ is allowed to materialize to Never, otherwise it is not? It seems like this would solve the same cases of undesirable assignability, without the result that Any becomes not-assignable to Never.

19

“simply” is doing some very heavy lifting here in terms of current implementations vs what would be required of implementations to make this rule work, but the simple expression of the rule doesn’t require involving a directly disallowing of a materialization of Never. it implicitly disallows it in some places where we would be going from an inhabitable type to Never. A specific instance of Any might be uninhabited, even though some instances of Any are inhabited. This is where the implementation details would get complex (and overlaps with a discussion we had about negating Any and needing to track gradual types differently), but interestingly, overloads (the case we want to preserve) would not be one of those. Neither would generic callable return types without a non-Any, non-Never bound

20

Sorry, I haven’t had the time to fully read the background and discussion here, but specifically on to topic of assignability of Any to Never, does forbidding this introduce a scenario where adding an Any annotation makes a program fail to type check? Assuming that Never is assignable to Never, and Never is assignable to Any, I can replace a Never annotation with Any and make a passing program start to fail, no?