How do we continue on from this point?
Is the next step a Pre-PEP and if so where could I find the resources to get started with writing a PEP?
1 Like
PEP 12 should be what you want.
1 Like
PEP 1 – PEP Purpose and Guidelines explains the process.
Maybe the rule of thumb would be that any access to a variable having this type attributed would error. It might be called Invalid and possibly be used in other cases…
Maybe in the case of a function requiring to have a given signature where one of the inputs is invalidated and should not be used or assigned, but I am not proficient in typing so I won’t try to write the ideal syntax for this.
I think the confusion may come from the python documentation saying they can be used in this way and giving an example of Never being used as return type for a function that always raises an exception.
“They can be used to indicate that a function never returns, such as sys.exit():
from typing import Never # or NoReturn
def stop() -> Never:
raise RuntimeError('no way')
Perhaps the typing documentation needs to be updated?
That is their intended purpose, I don’t know what you mean.
Never and NoReturn are supposed to be interchangeable.
Never was just misused for the purpose to show that access to an element is invalid. That is not its intended purpose and therefore some type checkers (pyright) special cased this behavior, while others didn’t.
My proposal is to add another similar construct to NoReturn and Never that specifically gives the type checker an error when an expression results in it.
So when, for example, a field or function result in Wrong (or however it will be called), it will explicitly be an error for the type checker, instead of misusing the other two existing constructs.
4 Likes
I will make a PEP write-up of this soon, when/if I manage to. Currently I don’t quite have the time.
Until then, I would like to open another final poll about the name of the special form, because the old one resulted in “something else”. I combined all suggested names that would not cause confusion with already existing language features.
- Forbidden
- Illegal
- Invalid
- Wrong
- I don’t care / Results
0
voters
1 Like
I still don’t really like any of the suggested names. I would personally prefer the decorator approach with @type_error, the way this feature has previously been suggested[1]. I think there’s also a potential missed opportunity for generalizing this feature along with @deprecated into something more widely useful like typing.dataclass_transform for defining custom decorators that emit some category of user-facing warning or error. Since it’s quite common for libraries to define something like that. It would also open up the possibility for user-defined type error categories that can be ignored in a more granular fashion, like giving libraries the opportunity to have some pedantic errors that are off by default, but can be enabled by changing the type checker configuration, similar to how deprecated errors are off by default in mypy.
That being said, having a special form in addition to a decorator could potentially be useful[2], the same goes for @deprecated, since right now you need something like @property to make deprecated attributes work. On the other hand, you can only easily get the benefit of a runtime warning with a decorator, so maybe restricting this feature to decorators is fine, even if it’s less ergonomic[3].
It gives the additional benefit/flexibility of being able to specify what return type is used for that function ↩︎
in which case the objections for
TypeErrorwould be valid, at which point my preference would probably shift towardsTypeViolationorViolation↩︎Although it might be interesting to think about a class level decorator which accepts a mapping for deprecated attributes, which inserts a hook into
__getattribute__for those attributes ↩︎
4 Likes
I want to throw Uninhabited in the ring.
To expand on this, I believe we have a problem due to NoReturn and Never being introduced as identical, when they are really two different concepts. If anything, NoReturn should actually have been the decorator, because conceptually NoReturn is not a type. It was introduced to annotate functions that never terminate (for example, event loops). On the other hand, the python docs state that
Never and NoReturn represent the bottom type, a type that has no members.
But this is a lie, not a single type checker truly honors the implications of Never being a type without members. If Never truly had no members, then the type checkers should throw an error whenever they witnessed an instance of that type (being created).
To me, it would make much more sense if we annotated these functions with a decorator
@typing.no_return # <- tells the type checker this function never returns
def event_loop() -> AnyTypeWeWantButProbablyJustNoneByConvention:
while True:
...
@typing.no_return
def raises_unconditionally() -> AnyTypeWeWant:
raise ValueError
Because again, conceptually, they never return anything, so we actually should be allowed to put any return type annotation we want there.
On the other hand, a typing.Uninhabited should really be that. Uninhabited and not fake uninhabited like typing.Never or typing.NoReturn. Witnessing an instance of Uninhabited is an error, always. The exception being of course a typing.no_return decorated function that returns Uninhabted, because there is no witness in this case.
1 Like
I don’t think it is clear that witnessing an instance of the uninhabited type should be an error.
Is dead code always an error? What if it’s only dead under the current type-checking environment, not all possible environments?
import sys
from typing import final
@final
class A: ...
@final
class B: ...
if sys.version_info >= (3, 14):
type MyAlias = A | B
else:
type MyAlias = A
def f(x: MyAlias):
if isinstance(x, B):
reveal_type(x)
If that code is checked under Python 3.13, reveal_type(x) should certainly reveal the uninhabited type. Should that be an error?
2 Likes
You are incorrect. I understand that this might seem counterintuitive, but this is how uninhabited / bottom types are supposed to work.
Never is a type without members. And yet, you can have a piece of code that tries to do stuff with a Never value and that code will not be a type error.
In some cases it might be a linter error, but it’s not the responsibility of type checkers to detect suspicious, smelly or unidiomatic code (and in general, detecting such code and automatically deciding if it is valid is not even possible, since it depends on semantics and might not even be decidable).
Type checkers only detect operations that are unsafe from the perspective of the type system. And code that does stuff with Never values is not unsafe. You might think that this is not intuitive, or you might not like it, but this is how the mathematical framework of type theory (and other related fields) works.
Unless you are planning to propose a completely separate mathematical theory in which uninhabited types are forbidden or invalid, the current type theoretical framework is here to stay.
In the meantime, this proposal suggests adding an extra helper type that would be able to carry extra information (represented outside of the type-theoretical framework) that would signal linters (and yes, maybe even some type checkers) to warn the user about using a uninhabited type that was explicitly marked as Invalid / Forbidden.
This is quite similar to Annotated - a type which carries more information than what would be allowed by the type-theoretical framework. Namely, the Invalid / Forbidden type isn’t just uninhabited, but also not intended to be used in any concrete code (you just can’t express “not intended to be used in any concrete code” as a concept in the mathematical framework underlying modern type theory).
3 Likes
For code like this, checked with 3.13, I’d expect a type checker to warn that a subclass of A and B can’t exist and mark the branch content as unreachable, so yes. And both mypy and pyright do this with strict settings pyright playground, mypy-playground
Theoretically, the intersection A & B would be, even if itself impossible, be more appropriate than Never here. Using methods on x inside that branch that neither belong to A nor to B is always wrong, but a Never type would incorrectly allow that.
The type error is not when using a value of Never, it is when allowing a member of Never to be created in the first place. This is the place when a type error should happen. Allowing this is self-contradictory. When you have code that calls a function def fn() -> Never, then a type checker should error on any fn() expression, because, from a type theory POV, this proves the creation of a member of the empty set, an obvious contradiction.
I agree that the current typechecker behavior is not quite right, but I disagree about the idea that function can’t have a return type of Never and still be valid to call.
If you want to actually differentiate the reasons for an error, you need an algebraic effects system or special forms per reason, while all of them would still be an uninhabited type, as raised exceptions are not returned values (they are the absence of such)
1 Like
This might be what you would intuitively expect, but that is not how type theory works.
-
sys.exitis a valid function with an uninhabited return type. -
handle_http_requests_in_a_loop_and_never_returnis a valid function with an uninhabited return type. -
This is also fine
def run_task_and_print_result[T]( task: Callable[[], T], ) -> None: result = task() # ^ result: T can be Never and that's not an error print("The task finished with result:", result) def get_str_task() -> str: return "wow" def do_stuff_forever_task() -> Never: # this function has an uninhabitable return type and that's not an error while True: stuff = get_more_stuff() stuff.do_some_things() print("I sure am busy!") run_task_and_print_result(get_str_task) run_task_and_print_result(do_stuff_forever_task) # this is totally okay
Yes, creating an instance of an uninhabitable type is a contradiction. No, a contradiction is not a type error. Encountering a “concrete” instantiation of an uninhabitable type just means that the code is unreachable.
Unreachable code is not unsafe. In fact, unreachable code is the most “type safe” code you can have since you are guaranteed that no type errors may occur in unreachable code (you know… since it will never ever be actually run).
Once again, please understand that this is not a matter of opinion. This is just how bottom types in type theory (the mathematical discipline) are supposed to work. Trying to argue otherwise is like trying to “solve” the Halting problem or claiming that you found a way to trisect an arbitrary angle with an unmarked straightedge and a compass.
Unless you are ready to propose a completely different mathematical theory in which bottom types are invalid, you’ll just have to accept the facts and move on.
3 Likes
I’ll disagree with this, but only because we don’t have a closed type system, we have an open gradual one. Unreachable code via the type system doesn’t indicate that the code is solely unreachable, it indicates that it is unreachable if the entrypoint obeys the annotations. We have stronger indications in the case of some runtime local narrowing, but not all.
I’ve laid out thoughts about improving this here but if we ignore the gradual and open nature, we can end up breaking the gradual guarantee without needing to.
1 Like
Yes, yes. Of course. If we are being pedantic, what I said only applies when you haven’t already lost type safety due to some other type unsafe operation in your code.
However, arguing about the semantics of programs that are unsound or type unsafe is pointless, IMHO. If you have already violated type safety (either by writing code that doesn’t pass a type checker, or by lying to the type checker using gradual typing or by performing an invalid cast or whatever), then you have already summoned the nose demons and at that point even a get_str() -> str might return an int.
I suppose, I should have said something like
Unreachable code is not type unsafe. In fact, unreachable code is the most “type safe” code you can have since you are guaranteed that no extra type errors may occur in unreachable code (unless, you have already violated type safety rules making this unreachable code actually reachable, at which point all bets are off).
But that still doesn’t change my main point. Unreachable code is at least as safe as any reachable type safe code.
2 Likes
Sorry if it came across as pedantic, I know of some actual deficiencies in current type checker behavior that are a result of this one (As well as other tangentially related issues of assuming more than the type system actually promises)
The classic example is that a type checker should easily be able to warn on the below, but instead treats it as dead code:
def foo(x: int) -> int:
if not isinstance(x, int):
return TypeError(f"Got {type(x):!r}, expected an int") # should be raised not returned.
...
This case allows a type error to propogate into type checked code where the user expects that they checked it both statically and at runtime.
You’re right that the blast radius on such issues is limited to where there’s already an error though.
1 Like
This also does give cases where it is legal to have a runtime value the type system believes has a type of Never though.
Locally, in that branch where there is runtime type enforcement, according to the type system, such a value can’t exist.
But in reality, an untyped caller could have called, and (at least fixing the above example to raise) is perfectly valid code even in the case of runtime narrowing to Never, not just a function that returns Never.
In python’s type system, Having a value with a type of Never only indicates that either the code is unreachable or one of our assumptions is wrong. Some of those assumptions are unavoidable in an open type system from the perspective of a type checker. A type checker can’t know that all users of your code also use a typechecker.