Yes, this would break the gradual guarantee. For example, in this program:
from typing import assert_never, Any
def f(x: int):
if isinstance(x, int):
pass
else:
assert_never(x)
If you remove the annotation on x (or annotate it as Any), type checkers would start showing an error for the assert_never() call under this proposal. Breaking the gradual guarantee sounds bad but I feel this is a positive change for users: if you use assert_never(), you want to be told that the code may not be unreachable.
Yes, we could say that: If B is equivalent to Never, A is assignable to B if any materialization of A is equivalent to Never. Otherwise, A is assignable to B if there exists a pair of fully static materializations Aâ and Bâ of A and B such that Aâ is not Never and Aâ is a subtype of B.
It sounds like this hack doesnât rely on assignability between Any and Never, but on assignability between types like list[Any] and list[Never]. As I wrote above, that is not the same thing; list[Never] is an inhabited type.
The union T | Any is not reducible to a simpler form. It represents an unknown static type with lower bound T . That is, it represents an unknown set of objects which may be as large as object , or as small as T , but no smaller.
Which implies that T | Any should always be assignable to T, which could be Never, and is therefore assignable to Never, yet it isnât.
Any would not be assignable to Never, but list[Any] would still be assignable to list[Never]. The proposed rule is:
For Any and Never: there is one materialization of Any that is a subtype of Never, and that is Never itself. There is no non-Never materialization of Any that is a subtype of Never, so Any is not assignable to Never.
For list[Any] and list[Never]: list[Never] is a possible materialization of list[Any], and it is not equivalent to Never but is a subtype of list[Never], so list[Any] is assignable to list[Never].
In other words, the proposed rule distinguishes between what you might call top-level and nested Any, perhaps counterintuitively.
Under the spec this should currently evaluate to Any. At step 2, no overloads are filtered out, and at step 5 none are filtered out either. The return types are not equivalent, so we return Any.
Under the proposed rule, the only change would be that the first overload would be filtered out at step 2. However, you still get non-equivalent return types on the remaining overloads, so the return type is Any.
The proposal would change the behavior for a set of overloads like this:
from typing import Any, Literal, overload, Never
@overload
def bool2int(x: Never) -> int: ...
@overload
def bool2int(x: Literal[False]) -> str: ...
a: Any
reveal_type(bool2int(a))
Currently pyright here infers int and mypy infers Any. The proposal would imply that the correct inference is str.
That language should have specified that it is not true for the top and bottom types, object and Never. object | Any is equivalent to object, and Never | Any is equivalent to Any. That follows from general principles: object is the set of all types, so unioning it with any other type doesnât leave you with a different type, and Never is the empty set, so unioning it with anything else leaves you with just the other type. We should change the wording here to clarify this.
And similarly you could also argue that Any should be assignable to Never, because the general assumption is if something is assignable to Any, then the converse well also hold. I suppose it would help for symmetry if Never wouldnât be assignable to Any, but that would break a bunch of other fundamental (implicit or explicit) assumptions, so thatâs probably not a good idea, leaving us with asymmetrical Any assignability rules.
Iâm sure thereâs a way to make this work, but doing so will complicate things a lot. As far as I can tell, this proposal lies within undiscovered type-theoretical lands, which is a risky place to be in, because of the unknown unknowns (which include(d) the Never overload workaround). So although I understand the motivation behind this, and appreciate the technical finesse of the proposed solution, Iâm worried that this might cause more problems than it solves.
I share these concerns and would prefer to take the time to explore the direction where we treat assignability differently based on better modeling and treatment of the absence of values. I believe it can be done without breaking the gradual guarantee, and I would strongly prefer that we preserve it.
Do you see issues with this formulation? At the moment it seems to me like the best option. It achieves the core aim of this proposal (avoiding problems with over-assignability), while preserving that Any is assignable to Never, which avoids both backward-compatibility issues and the gradual-guarantee problem.
I understand the argument that users might want assert_never(typed_as_Any) to fail, but I donât think this argument outweighs the gradual guarantee here. If this is important, I think it would be better implemented by changing the definition of assert_never; that is, assert_never(x) would become syntactic sugar for assert_type(x, Never) (perhaps thatâs how it should always have been defined, if not for implementation-simplicity considerations?) rather than being a simple function that accepts Never and leverages assignability.
As of right now assert_never is a function that just raises an AssertionError, which is the cleanest solution IMO. There should be no exceptions for assert_never. And if Anywould be treated special, shouldn'tobject` be treated special too then (and then, what about object instances and subclasses (basically everything in Python)), so all those cases should be special?
I think the current definition of assert_never is fine to allow Any. People can use assert_type if they need assert_type. We should tighten the language in guidance up here and emphasize that this should be seen as a tool primarily for asserting exhaustiveness and make an explicit note that exhaustive checks involving gradual types may end up falling back on the runtime error. Typecheckers could choose to offer additional warnings (not errors) that a gradual type reached an assert_never to help users be aware of this.
I think this only handles a subset of the cases I outlined above where Never is currently undesirable because itâs scoped too closely to assignability. With that said, I think this is a safe starting point and we would be able to do better with more time without a change that changes what is assignable again for the cases that this covers.
Yes, the problem with this formulation is that it would mean that any gradual type that can materialize to Never would still be assignable to Never. That includes not only Any itself, but also TypedDicts with required Any fields (as explained in my first post). If we specify that materialization also includes intersections of other materializations, as I think we must if we were to add intersections, then even more gradual types could materialize to Never.
I disagree that these cases are undesirable. It seems fine to me that it is possible to override a method with a non-Never return type with one with a Never return type. I donât see that as substantially different from something like def f() -> int: raise Exception, which is (and should be) legal.
The cases outlined above must be changed for intersections to have a sensible interpretation. This is part of why working on that has taken so long.
Beyond that, and something I wasnât directly arguing for, but I think is worth adding to the list, I wholeheartedly disagree that it should be allowed to only raise and never return from a function typed as returning.
There are very good reasons for these changes when we get to more complex issues that people want typed, like intersections or HKTs. Thereâs a reason many other newer languages differentiate between returning and erroring, and we do much the same in python already with exception handling, itâs just not modeled accurately. Iâm not pushing for a full effects system here, but we can do better for both soundness and the gradual guarantee by actually acknowledging that replacing a function expected to return a value for one that never can is clearly a substitutability issue.
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:
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.
It is required to have a key named never.
Or in other words, "never" in d is guaranteed to be True.
The value of that key is of type Never.
Or in other words, d["never"] is guaranteed to be assignable to Never.
(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
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â.