Issue with Never vs LSP

[DiscordLiz]

Never was added without a PEP as a way to directly indicate that something is uninhabited in 3.11

This brings up something from CarliJoy/intersection_examples#5 (comment) where we now have a way to express what appears to be an LSP violation that type checks (incorrectly) properly via structural subtyping by mishandling Never as a subtype of other types. Never is not a subtype of all other types. As the bottom type, it is uninhabited and does not follow subtyping rules.

from typing import Never

class A:
    def foo(self, x: int) -> None: ...
    
class B(A):
    foo: Never   # __getattr__(B, "foo") -> raise NotImplementedError
    
x: A = B()  # type checks 
reveal_type(B.foo)

https://mypy-play.net/?mypy=latest&python=3.11&flags=strict&gist=a4279b36d82c1a28d7b17be9a4bbcbdf

I believe under LSP, B is no longer a safe drop-in replacement for A. It's important to note that ongoing work to formalize the type system, including Never does not treat Never as a subtype of all other types, see the ongoing work here: http://bit.ly/python-subtyping

[JelleZijlstra]

I don't see a bug here. My understanding is that Never is compatible with any other type; if a function argument is typed as Callable[[], T] for any T, you can pass a Callable[[], Never] and type checking is correct. Do you think LSP checks should work differently?

The statement in Kevin Millikin's doc is a little imprecise, and there is discussion in the comments about exactly what it should mean, but it seems most of the confusion is about the interaction between Never and Any, which isn't at issue here.

[DiscordLiz]

Never (And all other bottom types in type systems) is not a subtype of any other type. It is the uninhabited type. I can link to formal type theory as well if you'd prefer?

I don't see a bug here. My understanding is that Never is compatible with any other type; if a function argument is typed as Callable[[], T] for any T, you can pass a Callable[[], Never] and type checking is correct. Do you think LSP checks should work differently?

Please note that you have Never in the return type there, which will never result in a type, only an exception. Inverting this makes it impossible to correctly call the function. The presence of a reliance on an uninhabited type in any code which is reachable is verifiably an error, and formalized type theories all agree on this.

This should absolutely be in error as otherwise this is just a sledgehammer that allows doing anything.

class A:
    x: int

class B:
    x: str

class C(A, B):
    x: Never

We've created a class that is impossible to ever have an attribute x, but if we are expecting A or B, we're expecting an attribute. This is unsafe replacement and the difference between an uninhabited type and a universal subtype matters

[erictraut]

@DiscordLiz, your definition of Never differs from how it is interpreted in the Python type system today by mypy, pyright and pyre.

It also differs from how the never type is treated in TypeScript, which is consistent with the current behavior in Python.

interface Parent {
    x: number;
}

interface Child extends Parent {
    x: never; // No type violation
}

I agree with Jelle that this isn't a bug, at least in terms of how the Never and NoReturn types have been treated historically in Python. If you want to redefine how they are treated, that would need to go through some standardization process, and the backward compatibility impact of such a change would need to be considered.

[DiscordLiz]

I think this is poorly considered in the face of both formal theory and obvious cases where this just allows nonsensical subclasses. It was not possible for users to create a concrete dependence on Never prior to 3.11, where this was added without a PEP and without such consideration. NoReturn was handled correctly, where it was correctly determined that there can't be a correct result relying on the (lack of) type. Additionally, typing.assert_never, which was added at the same time, correctly shows that the reliance of a type being never is equivalent to having unreachable code.

[tmke8]

The first line of the Wikipedia article on bottom types says:

In type theory, a theory within mathematical logic, the bottom type of a type system is the type that is a subtype of all other types.

I think this also makes intuitive sense: the bottom type is the type that is not inhabited, so it's kind of like the empty set, and the empty set is a subset of all other sets.

So, why does your example seemingly break LSP? It doesn't actually, because you can't actually construct an instance of B! In order to construct an instance of B you would need to have an instance of B.foo, but B.foo is of type Never and so it is not inhabited! So, it's actually all safe.

---

Incidentally, the union of any type with Never: T | Never should just be that type T because the union with the empty set is just the original set, but mypy reports a weird type for this:

from typing import Never

a: int | Never
reveal_type(a)  # N: Revealed type is "Union[builtins.int, <nothing>]"

[mikeshardmind]

Following over from where this came up as well: While I can see a definition of Never that allows this, @DiscordLiz is correct in that formal set-theoretic type systems based on subtyping relationships, including those with gradual typing, do not view the bottom type as a subtype of other types.*

Caveat on not partaking in subtyping

There is a definition of subtyping that they do partake in, but this definition of subtyping is not how type checkers currently handle subtyping, we could adopt that definition, but doing that is equivalent to saying the current behavior is wrong, so I didn't want to claim "it does participate in subtyping, python just does subtyping wrong too", when there are many ways to define subtyping and we don't have formal codified accepted definitions, we have people pointing to what implementations are doing

In such formal theories, much of which the work being done in formalization is based on, the top and bottom type are not types or even sets of types, but sets of sets of types. They exist at a higher order and are conceptually useful for indicating that something could be any possible compatible type or can't be satisfied by any type.

I don't think allowing Never as a universal subtype is useful, and it arguably completely changes expectations of what is a valid subtype to allow it, for behavior that was added without a PEP if this is the interpretation, so adding it without a PEP was breaking and now it's being suggested that changing it would require a notice period. (prior to the addition of Never, in 3.11, we only had NoReturn, which being documented as only to be used in a function return, happened to be handled correctly incidentally if people were assuming Never to be a subtype of other types because it could only indicate an exception as a return type, not actually replacing a concrete type where there was a valid expectation of one.)

---

To wit on the uselessness of this, all attribute access, even when we've specified a type that specifies an attribute exists, is now subject to it not existing if we accept this absurd premise, all because of an addition to the type system without a clear definition and without going through the process for addition where there would have been visibility on this.

---

I also don't think that "well other language allows it" means it is useful or is a good justification. All that means is that multiple people reached the same conclusion, not that the conclusion was reached correctly in either case.

The first line of the Wikipedia article on bottom types says:

Wikipedia is not correct here without a specific definition of subtyping. Some definitions of subtyping this can be shown does not hold for. I may take the time to update it with proper sourcing correcting this later, but I've got a lot of various things I'm discussing in relation to this, and that's a pretty low priority. you may want to read Abstracting Gradual Typing (AGT), (Garcia et al, 2016) for more rigorous definitions that have been proven correct.

[DiscordLiz]

@tmke8

So, why does your example seemingly break LSP? It doesn't actually, because you can't actually construct an instance of B! In order to construct an instance of B you would need to have an instance of B.foo, but B.foo is of type Never and so it is not inhabited! So, it's actually all safe.

mypy doesn't error at constructing an instance of B, so it allows it despite that that requires an instance of B.foo that is uninhabited, as shown in the mypy playground link. If mypy didn't allow constructing an instance of B, this would still be an issue however when it comes to accepting things of type[A] and receiving type[B] as an unsafe substitution. There is a reason formal theories have determined that a reliance on the bottom type indicates an error.

[mikeshardmind]

The crux of the issue here (functionally) is this:

• The ability to Remove capabilities from a class breaks the idea that subclasses are safe as a drop-in replacement for the base.
• Allowing Never as a subtype allows arbitrary removal of capabilities in subclasses without breaking compatibility.
• If this is allowed, all function parameters should be invariant as a result to prevent the issue of substitution being broken, which would of course be significantly more breaking than fixing the issue with Never here.

As for formally, papers papers galore, but python is unfortunately not so well formalized at this time.

[DiscordLiz]

Is there someone who can directly transfer this issue from python/mypy to python/typing via github's transfer feature? Thanks Jelle

If other type checkers are and have been allowing this and this may need to be discussed more as an issue for type safety overall. I don't think having a way to intentionally break compatibility and yet claim compatibility is a good thing here, and the difference between NoReturn (as a return type annotation) and Never everywhere in general changes the effects of the existance of a user specified Never which is treated as participating in subtype relationships.

[mikeshardmind]

It was pointed out to me in a discord discussion that NoReturn was being allowed by type checkers in places other than return type annotations prior to 3.11. I don't think this behavior was technically specified anywhere officially prior to 3.11, but it's worth being aware that this actually goes further back than 1 version.

I don't think this changes the need to discuss whether this should be allowed or not. My personal opinion here is that Never should be viewed as the absence of a valid type and uninhabited, not as a universal subtype that is uninhabitable, for reasons above involving replacement, as well as goals of formalization long term, but checking for impact of that (while would already be important) is much more important with the context that this has been supported for multiple versions.

[erictraut]

NoReturn was being allowed by type checkers in places other than return type annotations prior to 3.11

Yes, that's correct. Thanks for pointing that out. The NoReturn type has been allowed by type checkers in places other than return type annotations for a long time. Doing some archeological digging, it appears that this was first discussed and implemented in this mypy issue. The assert_never use case that motivated this change was quickly adopted by many code bases. Pyright, pyre, and pytype shortly thereafter followed mypy's lead and removed the limitation on NoReturn. In summary, this use of NoReturn has been in place for about five years, and I've seen it used in many code bases.

In Python 3.11, typing.Never was added as an alias for NoReturn because the NoReturn name was causing confusion for Python users. Never was considered a better name — one that many other programming languages had already adopted in their type systems. The change was discussed in the typing-sig with little or no objection raised. No PEP was deemed necessary because Never was simply an alias for NoReturn, which was an existing concept in the type system.

At the same time, typing.assert_never was added to eliminate the need for each code base to define this same function. This was also discussed on the typing-sig with little or no objection.

---

As for the broader issue being discussed here, I'm trying to get a sense for whether this is simply a nomenclature issue or whether there's a meaningful difference of opinion.

One area of contention is whether the concept called a "bottom type" participates in subtype relationships. It makes logical sense to me that it would given that it satisfies all of the set-theoretic properties of subtyping, but it's possible I'm missing something here. If we're not able to agree on whether Never is a subtype of all other types, perhaps we can at least achieve agreement about whether Never is consistent with all other types. In a gradual type system, "is-consistent-with" is the relevant test. If we can agree on that, then I think the other point is largely moot, and we can avoid further debate.

---

The terms "bottom type" and "top type" have been used pretty consistently throughout the development of the Python type system (included in PEP 483), but some of the other terms being used in the Intersection discussion have been new to me — and probably others. This includes the term "uninhabited", which is a term that does not appear anywhere in PEP 483, 484, or the searchable history of the typing-sig. I was also unable to find the term in the official TypeScript or Rust documentation. If you use the term "uninhabited type" to make a point, it may not land with your audience. If "uninhabited type" is synonymous with "bottom type" (which I gather is the case?), then it's probably best to simply stick with "bottom type" and avoid confusing folks with an alternate term. If those two terms are not synonymous, then it would be good to formally define the difference between the two.

---

It was pointed out in the thread above that mypy doesn't generate an error when a class with an attribute of type Never is constructed. Mypy is not alone here. It's consistent with the other Python type checkers. An error is reported only if and when an attempt is made to assign a value to that attribute.

class Foo:
    x: Never

f = Foo() # No type error
f.x = "" # Type violation

foo: Never # No type error
foo = "" # Type violation

This makes Never consistent with any other type. For example, if you change Never to int in the above code sample, you'd see the same behavior (same type violation errors in the same locations). Unless and until someone assigns a value to that symbol, it has no value, and no type rules have been violated.

This is in contrast to some (stricter) programming languages where it's considered a static error to declare a symbol and leave it unassigned.

[tmke8]

I agree that the fact that attributes can remain unassigned is an unrelated issue from this discussion. If you force the attribute to be assigned, then type checkers will complain in the correct way:

from dataclasses import dataclass
from typing import Never

@dataclass
class Foo:
    x: Never

f = Foo("")  # type error no matter what you try to pass in

If "uninhabited type" is synonymous with "bottom type" (which I gather is the case?)

Yes, I believe that is the case.

[mikeshardmind]

One area of contention is whether the concept called a "bottom type" participates in subtype relationships. It makes logical sense to me that it would given that it satisfies all of the set-theoretic properties of subtyping, but it's possible I'm missing something here. If we're not able to agree on whether Never is a subtype of all other types, perhaps we can at least achieve agreement about whether Never is consistent with all other types. In a gradual type system, "is-consistent-with" is the relevant test. If we can agree on that, then I think the other point is largely moot, and we can avoid further debate.

Well, I can't agree with that. The set-theoretic view as I've understood it and seen it presented formally in papers where people have actually shown formal proofs, is that the bottom and top types are not even really part of the same hierarchy as other static and gradual types. They exist at a higher order. The bottom type isn't a static type, but the absence of valid types. The top type isn't a singular static or gradual type (even though it behaves like a gradual type) but the potential for any compatible type. Neither participate in subtyping relationships [in the way python currently is treating subtyping] in this model, but it is possible to go from the top type to a more specific type when presented with evidence that the more specific gradual or static type is correct. It is also possible to go from having a type, to eliminating all possible types (such as in the case of exhaustive matching)

[mikeshardmind]

Tangential comments about process (off-topic)

Yes, that's correct. Thanks for pointing that out. The NoReturn type has been allowed by type checkers in places other than return type annotations for a long time. Doing some archeological digging, it appears that this was first discussed and implemented python/mypy#5818 (comment). The assert_never use case that motivated this change was quickly adopted by many code bases. Pyright, pyre, and pytype shortly thereafter followed mypy's lead and removed the limitation on NoReturn. In summary, this use of NoReturn has been in place for about five years, and I've seen it used in many code bases.

Which is type checkers changing the behavior via... their issue tracker instead of by specification being amended. Sigh it's years ago, little late to do much about that, but I don't think this is generally a good way for changes to happen. The specification should drive what is correct, not the implementation. If an implementation has a reason to need changes, there's a way to do that.

The change was discussed in the typing-sig with little or no objection raised.

The thing is, typing sig isn't the most noticeable place for behavioral changes to be discussed. I can sign up and follow the mailing lists I guess, but I don't really like specifications changing by just a small thing in a mailing list that may not receive attention. Specification changes have very long-term and wide-reaching impact.