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 https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1699490563 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 https://github.com/python/mypy/issues/5818#issuecomment-432616244. 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.

[mikeshardmind]

(Sorry if this is a lot, I've split my comments by concern to not have a singular wall of text)

I don't know how breaking changing the definition of Never to be more in line with what proven theory says is correct for the bottom type would be, and I'm not in a great place to implement something to that effect right now to run against mypy_primer, but I think it is worth considering.

Notably, the only actual changes behaviorally is that Never can still arise from type narrowing removing all other possible types, but any code depending on an instance of Never can't be expected to be validly reached at runtime, and Never can't be used to replace other types without it being by removing the other types. With this change, the only function which should ever receive Never as an argument, is assert_never (or any other future function intended to handle how runtime realities may diverge from static analysis due to misuse or the uncertainties of the real-world code), and only at type checking time. It would still be valid to have as a return type (indicating the lack of return)

assert_never's signature should also probably be updated too

```py @overload def assert_never(obj: object) -> Never: ... # raises at runtime if called with any real object, purpose is `unreachable` code @overload def assert_never(obj: Never) -> None: ... # the point is ensuring the type has been exhausted of all possible types def assert_never(obj): ... ```

I know there's existing work on formalization going on elsewhere, but we're running into issues with the current less formal definitions now, and with ongoing work in trying to get the Intersections PEP ready.

[DiscordLiz]

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.

I disagree that Never is consistent with other types, but it's probably useful to understand how it seems people got to a point where they have come to the conclusion that it is.

Lets start with something basic, If I specify in a function parameter annotation a singular static type, it isn't just that singular static type which is correct to give the function. Anything which can suitably stand in as a replacement for this singular type is also valid. So the parameter annotation doesn't represent one type (except in cases of invariant parameters) even though it is spelled as one type. This conceptual set of possible types which can be used in the hypothetical function exists at the same higher order @mikeshardmind referred to when describing how the top and bottom type don't exist at the same level as static and gradual types in the set-theoretic model.

In python, we have two ways that are supported by the type system for this. Inheritence (nominal typing) and Protocols (structural typing). Never can't suitably stand in for any type. It lacks the structure of every type, as it can't even exist, and it isn't a subclass of any other type either. It isn't a gradual type, it's the lack of a type all together.

So why is Never a suitable replacement in a return type? Well, it isn't. Because we aren't returning a type anymore, at least, not in a way that typing checks* and python does not have the same code path for returning values and raising exceptions, a function which unconditionally raises can have it's return value annotation used to mark the lack of return value without this being a replacement of the return type; Rather, it's specifying the lack of a type being returned.

I believe the original name of NoReturn was actually more correct for most places users could actually specify it, and some of the original insight of those who named it that may have fallen away to lack of recording anywhere important. The one case where Never is more correct as an annotation, is in the special purpose function assert_never, which the goal of is also to say that there is no longer a valid type. This is similar to unreachable in many compiled static languages. Actually reaching unreachable signals an error, as would passing an instance of something which shouldn't exist (the type system believes there are no remaining options, hence Never).**

I think it's how errors are handled in python and many other languages, and Never appearing to work as a replacement in one place (return values) that misleads people into believing it should work everywhere and be consistent with all types.

*Exceptions are really still just values with special control flow, but absent a proposal to add checked exceptions to python's type system, this distinction doesn't matter. I don't care about or want checked exceptions in python, but adding this to the type system would be an ordeal that if someone does want, they would find issues arise with Never as a replacement annotation without additional syntax.

** Never is still a good and useful name though. Never can still correctly arise in inference with elimination of possible types, and it would be weird to have NoReturn as the name in inference in that case.

[eltoder]

@tmke8

So, why does your example seemingly break LSP? It doesn't actually, because you can't actually construct an instance of B!

I think it is debatable whether constructing an instance of B should be disallowed, or if it is enough that access to foo always raises an exception for B.foo to have type Never. However, this is moot. The same issue arises for methods returning Never and NoReturn:

from typing import NoReturn

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

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

mypy allows this, but this arguably violates LSP for the same reasons as the example in OP. It introduces unreachable code into methods using A. IMHO, creating instances of this B should be allowed, but this inheritance should generate an error.

Also note that

• PEP 484 does not specify any subtyping relationships for NoReturn.
• There are several issues for mypy where people ask to disallow using NoReturn and Never as values, because this hides bugs. [1][2][3]
• mypy already disallows using functions that return None as values even if this is not a type error, because this is likely a bug. [4]

[1] https://github.com/python/mypy/issues/4116 [2] https://github.com/python/mypy/issues/13592 [3] https://github.com/python/mypy/issues/15821 [4] https://mypy-play.net/?mypy=latest&python=3.11&gist=e757839d654dd3dbc395128ec3015912

[tmke8]

from typing import NoReturn

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

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

mypy allows this, but this arguably violates LSP for the same reasons as the example in OP. It introduces unreachable code into methods using A.

I think a type theorist would reply that yes, you are allowed to construct an instance of this B class but LSP still isn't violated because you cannot get the program into an inconsistent state with this; if you call B.foo through the interface of A, the program will just crash, but it is not the case that a variable that was declared as int now has a value of a different type. So, no type guarantee is violated.

But, python's static typing obviously doesn't have to follow type theory exactly, so I won't object to potential changes on this ground.

(I just object to OP's framing of this issue as mypy violating type theory. In type theory, the bottom type is definitely a subtype of all other types. You can advocate for deviating from this, but I don't think you can say that it's more theoretically grounded that way.)

[eltoder]

@tmke8

if you call B.foo through the interface of A, the program will just crash, but it is not the case that a variable that was declared as int now has a value of a different type.

This is correct, but also not useful IMO. It is not different from passing in an object where foo is not defined at all, or has a different number of arguments. Both will result in an exception rather than a value of a different type. But preventing such exceptions is the primary reason to use a static type checker in python in the first place :-)

I agree that bottom type is by definition compatible with every other type. I think the OP's argument is that Never should be an "uninhabited type" rather than the bottom type, which are different in some theories, because making it bottom type introduces too much unsafety.

[mikeshardmind]

(I just object to OP's framing of this issue as mypy violating type theory. In type theory, the bottom type is definitely a subtype of all other types. You can advocate for deviating from this, but I don't think you can say that it's more theoretically grounded that way.)

@tmke8

In the set-theoretic model of typing which current formalization efforts are largely being built on top of, the bottom and top types don't participate in subtyping behavior. (At least in the way python type checkers are defining what a subtype is, see other posts that point out a reconciliation) Relations with these types are defined by other properties. Now, I've linked a draft that still has a lot of imprecise wording and which there is still ongoing discussion about amending several sections to be more in line with theory and deviate from it less, but there are a lot of referenced research papers and published proofs linked within that, and you may find reading through some of the more recent research here and what more recent published proofs show to be correct may broaden your perspective.

In these models, the bottom type is uninhabitable and does not participate in subtyping behavior directly with static or gradual types, instead participating with a well-defined set of behaviors (that is not equivalent to subtyping for the top and bottom types) with the relation of type specifications, which are the sets of types that can be used where a static or gradual type is requested. This distinction is subtle but important. (Note that some papers have defined this as subtyping as well, but that these definitions do not match python's current behavior)

Outside of two things:

1. Any being subclassable. This one is reconcilable with the theories python is closest to currently by not treating any as the top type as a base class, but as a gradual type that shares the same name, but having a different symbolic meaning in this context.
2. Never participating in subtyping as current typecheckers are using the term. This one changes some fundamentals of those theories, and does not appear to be easy to reconcile.

Python's type system fully follows the set-theoretic model's definitions, specifically those built up in Abstracting Gradual Typing

If that doesn't change your perspective, I'd be interested to hear how you reconcile this, as well as the effects on LSP, as it could be illuminating for how we handle this going forward.

I think the OP's argument is that Never should be an "uninhabited type" rather than the bottom type, which are different in some theories, because making it bottom type introduces too much unsafety.

@eltoder See above, but no, the argument is that python actually follows the set-theoretic definitions for nearly everything else, and that it should for Never as well. (the set-theoretic ones have the bottom type as uninhabited, as you nodded to with "some theories")) Not doing so creates inconsistency, and creates a situation where established rules for safe-replacement do not work. (Note, This still is being discussed in the formalization happening in the background as well, there isn't good agreement on which definitions should be used yet anywhere, but there are issues we can show with treating Never as a type that participates in subtyping.)

[mikeshardmind]

As for the current behavior concretely violating LSP, @randolf-scholz raised this recently in the related conversation pertaining to intersections

One possible resolution: Behavioral LSP states that

• (LSP-precondition): Preconditions cannot be strengthened in the subtype.
• (LSP-postcondition): Postconditions cannot be weakened in the subtype.

For functions, the contra-variance of arguments and co-variance of return types can be equivalently described as a set of pre-conditions and post-conditions. In particular, the covariance of the return type of Callable[..., R] is equivalent to the post-condition isinstance(return_value, R).

However, when we try to substitute Never for R there is a problem: the equivalence to a post-condition is no longer true, since Never is supposed to be uninhabited (no instances of the type can exists). Therefore, the post-condition must fail. Indeed, the prior interpretation of Never as NoReturn means that the post-condition can actually never even be reached.

This suggests one could consider a modified subtyping rule for functions, which one may refer to:

(no-substitute-never) Callable[...., R] <: Callable[..., S] if and only if either R==S==Never or Never ≨ R <: S.

I.e. if S≠Never we assume subtyping includes the post-condition and if S=Never it doesn't. This is a weak version of (LSP-exception) that forbids to substitute a function with another function that unconditionally raises if the original didn't. It would make example ① void, and, consequently, the whole https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1700892611. In particular, this would guarantee that B.getattribute("specific_key") is not allowed to raise unconditionally if the parent class didn't for "specific_key".

This makes an attempt to square the two, but notably, this creates a specific exception that reaches the same result as changing the general definition as argued here.

[eltoder]

@mikeshardmind I think it is hard to argue "python actually follows the set-theoretic definitions for nearly everything". The typing PEPs are generally not precise enough, so mypy is used as a de facto interpretation of those PEPs. But mypy has over 2000 open issues and also includes behaviors that address style or practical concerns and are far from theory. I expect that if you examine the actual behavior of mypy in enough detail, you find a lot of places where it deviates from theory.

OTOH, the current definition of Never is used in a lot of programming languages[1], so it's fair to say at a minimum that there are arguments and research supporting this position.

[1] https://en.wikipedia.org/wiki/Bottom_type#In_programming_languages

[mikeshardmind]

I think it is hard to argue "python actually follows the set-theoretic definitions for nearly everything". The typing PEPs are generally not precise enough, so mypy is used as a de facto interpretation of those PEPs. But mypy has over 2000 open issues and also includes behaviors that address style or practical concerns and are far from theory. I expect that if you examine the actual behavior of mypy in enough detail, you find a lot of places where it deviates from theory.

OTOH, the current definition of Never is used in a lot of programming languages[1], so it's fair to say at a minimum that there are arguments and research supporting this position.

@eltoder This discussion in this thread is overflowing from over a month of exploring issues with a potential addition to the type system which is based on theory. I don't lightly bandy about that python mostly follows these definitions, this has been heavily discussed and led to a lot of discussion that ultimately needed to come here due to a poor interaction between how type checkers are currently interpreting Never and other assumptions people have about type safety.

I also think we would benefit from better definitions that don't lead to relying on "well, this is what type checkers are currently doing" to define what is correct, or the end result is "type checkers, including any errors in their implementation, are the source of truth, not the specified rules."

OTOH, the current definition of Never is used in a lot of programming languages[1], so it's fair to say at a minimum that there are arguments and research supporting this position.

Funnily enough, what you linked isn't quite making the argument you seem to think it is. For example, Haskell and Rust's definitions both match more closely to what is described in this issue than what type checkers are currently doing.

Haskell:

Attempting to evaluate such an expression causes the code to abort unrecoverable.

Rust:

In Rust, the bottom type is called the never type and is denoted by !. It is present in the type signature of functions guaranteed to never return, for example by calling panic!() or looping forever. It is also the type of certain control-flow keywords, such as break and return, which do not produce a value but are nonetheless usable as expressions

Rust and Haskell do not allow the bottom type where python type checkers currently do, only allowing it where there is no value, and correctly treating reaching code that has a type of Never to be an error.

@discordliz gave a good explanation above for how easy it would be for someone without the type theory background to make the incorrect leap that many have made and why.

Additionally, When comparing TypeScript's use of Intersections, with what is being proposed for python, it was found that typescript has an arbitrary undocumented sorting algorithm that has an impact on the outcome of intersections. Should we conclude that intersections must have this feature because another language did this? Just because another language does something does not mean that that something has had the same considerations for use that would be appropriate for other use.

[DiscordLiz]

@mikeshardmind just a slight clarification for anyone confused, Haskell allows specifying such code but treats the use of it as and impossible to recover from error. This is strictly as a mathematical outcome that could arise due to composition of functions, and not as an intent to allow such code to exist or be used. You are still correct that this is not treating Never as a subtype but as the absence of a valid type.

[DiscordLiz]

@eltoder

I think it is hard to argue "python actually follows the set-theoretic definitions for nearly everything".

Hopefully mniip doesn't mind this being shared here to make the point that this is possible, but... It's possible to create a program to actually check this by encoding the rules of a specific model of working with types into a formal proof engine and comparing it to what is currently the "accepted consensus behavior" since you are arguing that the PEPs aren't precise. I similarly share the above opinion that the imprecision in PEPs meant to specify is a problem.

Coq formalization of "Gradual Typing with Union and Intersection Types" (https://www.irif.fr/~gc/papers/icfp17.pdf)

Starting from: , but modified further. ```coq Require Import Coq.Lists.List. Require Import Coq.Bool.Bool. Require Import Coq.Relations.Relations. Require Import Coq.Compat.AdmitAxiom. Import ListNotations. Infix "<$>" := map (at level 65, left associativity). Notation "k >>= f" := (flat_map f k) (at level 66, left associativity). Definition allb {A} (f : A -> bool) (xs : list A) : bool := fold_right andb true (map f xs). Definition anyb {A} (f : A -> bool) (xs : list A) : bool := fold_right orb false (map f xs). Definition apList {A B} (fs : list (A -> B)) (xs : list A) : list B := fs >>= fun f => f <$> xs. Infix "<*>" := apList (at level 65, left associativity). Definition null {A} (xs : list A) : bool := match xs with | [] => true | _ => false end. (* Subtyping decision procedure for base types. We parameterize over it here. *) Class SubtypeDecidable (BaseType : Type) : Type := { bsubDecide : list BaseType -> list BaseType -> bool (* `bsubDecide xs ys` is whether the intersection of xs lies within the union of ys *) ; BSub := fun t s => bsubDecide [t] [s] = true ; bsub_refl : reflexive _ BSub ; bsub_trans : transitive _ BSub }. Section Types. Context {BaseType : Type} `{SubtypeDecidable BaseType}. Inductive SType : Type := | SBottom : SType | STop : SType | SNot : SType -> SType | SArrow : SType -> SType -> SType | SBase : BaseType -> SType | SAnd : SType -> SType -> SType | SOr : SType -> SType -> SType. Inductive GType : Type := | GBottom : GType | GTop : GType | GAny : GType | GNot : SType -> GType | GArrow : GType -> GType -> GType | GBase : BaseType -> GType | GAnd : GType -> GType -> GType | GOr : GType -> GType -> GType. Declare Scope stype_scope. Delimit Scope stype_scope with stype. Bind Scope stype_scope with SType. Notation "𝟘" := SBottom : stype_scope. Notation "𝟙" := STop : stype_scope. Notation "¬ t" := (SNot t) (at level 75) : stype_scope. Infix "→" := SArrow (at level 99, right associativity) : stype_scope. Infix "∧" := SAnd (at level 85, right associativity) : stype_scope. Infix "∨" := SOr (at level 85, right associativity) : stype_scope. Notation "⋀ xs" := (fold_right SAnd STop xs) (at level 85) : stype_scope. Notation "⋁ xs" := (fold_right SOr SBottom xs) (at level 85) : stype_scope. Declare Scope gtype_scope. Delimit Scope gtype_scope with gtype. Bind Scope gtype_scope with GType. Notation "𝟘" := GBottom : gtype_scope. Notation "𝟙" := GTop : gtype_scope. Notation "?" := GAny : gtype_scope. Notation "¬ t" := (GNot t) (at level 75) : gtype_scope. Infix "→" := GArrow (at level 99, right associativity) : gtype_scope. Infix "∧" := GAnd (at level 85, right associativity) : gtype_scope. Infix "∨" := GOr (at level 85, right associativity) : gtype_scope. Notation "⋀ xs" := (fold_right GAnd GTop xs) (at level 85) : gtype_scope. Notation "⋁ xs" := (fold_right GOr GBottom xs) (at level 85) : gtype_scope. Reserved Infix "≤" (at level 70, no associativity). Inductive Sub : SType -> SType -> Prop := | sub_base : forall b c, BSub b c -> SBase b ≤ SBase c | sub_not_mono : forall t s, s ≤ t -> (¬t) ≤ (¬s) | sub_arrow_mono : forall t1 t2 s1 s2, s1 ≤ t1 -> t2 ≤ s2 -> (t1 → t2) ≤ (s1 → s2) | sub_bottom : forall t, 𝟘 ≤ t | sub_top : forall t, t ≤ 𝟙 | sub_and_l : forall t1 t2, (t1 ∧ t2) ≤ t1 | sub_and_r : forall t1 t2, (t1 ∧ t2) ≤ t2 | sub_and : forall t s1 s2, t ≤ s1 -> t ≤ s2 -> t ≤ (s1 ∧ s2) | sub_or_l : forall t1 t2, t1 ≤ (t1 ∨ t2) | sub_or_r : forall t1 t2, t2 ≤ (t1 ∨ t2) | sub_or : forall t1 t2 s, t1 ≤ s -> t2 ≤ s -> (t1 ∨ t2) ≤ s | sub_trans : forall t s r, t ≤ s -> s ≤ r -> t ≤ r where "t1 ≤ t2" := (Sub t1 t2). Section SubDecide. (* Either conjuncts or disjuncts depending on context, categorized by whether it's a BaseType or an arrow, and by whether it's negated *) Record Junct := mkJunct { bases : list BaseType ; arrows : list (SType * SType) ; notBases : list BaseType ; notArrows : list (SType * SType) }. Definition unitJunct : Junct := {| bases := [] ; arrows := [] ; notBases := [] ; notArrows := [] |}. Definition mergeJuncts (j1 j2 : Junct) : Junct := {| bases := bases j1 ++ bases j2 ; arrows := arrows j1 ++ arrows j2 ; notBases := notBases j1 ++ notBases j2 ; notArrows := notArrows j1 ++ notArrows j2 |}. Definition invertJunct (j : Junct) : Junct := {| bases := notBases j ; arrows := notArrows j ; notBases := bases j ; notArrows := notArrows j |}. Fixpoint udnf (t : SType) : list Junct := match t with | SBase b => [{| bases := [b]; arrows := []; notBases := []; notArrows := [] |}] | t1 → t2 => [{| bases := []; arrows := [(t1, t2)]; notBases := []; notArrows := [] |}] | 𝟘 => [] | 𝟙 => [unitJunct] | ¬t => invertJunct <$> ucnf t | t1 ∨ t2 => udnf t1 ++ udnf t2 | t1 ∧ t2 => mergeJuncts <$> udnf t1 <*> udnf t2 end%stype with ucnf (t : SType) : list Junct := match t with | SBase b => [{| bases := [b]; arrows := []; notBases := []; notArrows := [] |}] | t1 → t2 => [{| bases := []; arrows := [(t1, t2)]; notBases := []; notArrows := [] |}] | 𝟘 => [unitJunct] | 𝟙 => [] | ¬t => invertJunct <$> udnf t | t1 ∧ t2 => ucnf t1 ++ ucnf t2 | t1 ∨ t2 => mergeJuncts <$> ucnf t1 <*> ucnf t2 end%stype. Definition junctDecide (jt js : Junct) : bool := match bases jt ++ notBases js, arrows jt ++ notArrows js with | lbases, [] => bsubDecide lbases (bases js ++ notBases jt) | [], _ => match proof_admitted with (* How to decide subtyping of a bunch of arrows? Not sure. *) end | _, _ => match proof_admitted with (* How to decide whether base types intersect arrow types? This depends on the target language in some way. *) end end. Definition subDecide (t s : SType) : bool := allb id (junctDecide <$> udnf t <*> ucnf s). End SubDecide. Infix "≤!" := subDecide (at level 70, no associativity). Notation "t ∈ S" := (S t) (at level 70, only parsing). Fixpoint γ (τ : GType) : SType -> Prop := match τ with | ? => fun _ => True | 𝟘 => eq 𝟘%stype | 𝟙 => eq 𝟙%stype | GBase b => eq (SBase b) | ¬t => eq (¬t)%stype | τ1 ∧ τ2 => fun t => match t with | t1 ∧ t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2 | _ => False end%stype | τ1 ∨ τ2 => fun t => match t with | t1 ∨ t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2 | _ => False end%stype | τ1 → τ2 => fun t => match t with | t1 → t2 => t1 ∈ γ τ1 /\ t2 ∈ γ τ2 | _ => False end%stype end%gtype. Definition lift2 (P : SType -> SType -> Prop) : GType -> GType -> Prop := fun τ1 τ2 => exists t1 t2, t1 ∈ γ τ1 /\ t2 ∈ γ τ2 /\ P t1 t2. Fixpoint gradualMinimum (τ : GType) : SType := match τ with | ? => 𝟘%stype | 𝟘 => 𝟘%stype | 𝟙 => 𝟙%stype | GBase b => SBase b | ¬t => (¬t)%stype | τ1 ∧ τ2 => (gradualMinimum τ1 ∧ gradualMinimum τ2)%stype | τ1 ∨ τ2 => (gradualMinimum τ1 ∨ gradualMinimum τ2)%stype | τ1 → τ2 => (gradualMaximum τ1 → gradualMinimum τ2)%stype end%gtype with gradualMaximum (τ : GType) : SType := match τ with | ? => 𝟙%stype | 𝟘 => 𝟘%stype | 𝟙 => 𝟙%stype | GBase b => SBase b | ¬t => (¬t)%stype | τ1 ∧ τ2 => (gradualMaximum τ1 ∧ gradualMaximum τ2)%stype | τ1 ∨ τ2 => (gradualMaximum τ1 ∨ gradualMaximum τ2)%stype | τ1 → τ2 => (gradualMinimum τ1 → gradualMaximum τ2)%stype end%gtype. Notation "τ ⇓" := (gradualMinimum τ) (at level 65). Notation "τ ⇑" := (gradualMaximum τ) (at level 65). Infix "̃≤" := (lift2 Sub) (at level 70, no associativity). Definition consSubDecide (σ τ : GType) : bool := σ⇓ ≤! τ⇑. Infix "̃≤!" := consSubDecide (at level 70, no associativity). Infix "̃≰" := (lift2 (fun s t => ~(s ≤ t))) (at level 70, no associativity). Definition consNotSubDecide (σ τ : GType) : bool := negb (σ⇑ ≤! τ⇓). Infix "̃≰!" := consNotSubDecide (at level 70, no associativity). (* ??? The paper completely glances over that it treats SType as a subset of GType in the definition of γA. γA+ restricted to SType is γApos' here. *) Fixpoint stype2gtype (t : SType) : GType := match t with | 𝟘 => 𝟘%gtype | 𝟙 => 𝟙%gtype | ¬t => (¬t)%gtype | t1 → t2 => (stype2gtype t1 → stype2gtype t2)%gtype | SBase b => GBase b | t1 ∧ t2 => (stype2gtype t1 ∧ stype2gtype t2)%gtype | t1 ∨ t2 => (stype2gtype t1 ∨ stype2gtype t2)%gtype end%stype. Fixpoint γAneg (t : SType) : list (list (GType * GType)) := match t with | t1 ∨ t2 => (fun T1 T2 => T1 ++ T2) <$> γAneg t1 <*> γAneg t2 | t1 ∧ t2 => γAneg t1 ++ γAneg t2 | _ → _ => [[]] | ¬t => γApos' t | 𝟘 => [[]] | 𝟙 => [] | SBase _ => [[]] end%stype with γApos' (t : SType) : list (list (GType * GType)) := match t with | t1 ∨ t2 => γApos' t1 ++ γApos' t2 | t1 ∧ t2 => (fun T1 T2 => T1 ++ T2) <$> γApos' t1 <*> γApos' t2 | t1 → t2 => [[(stype2gtype t1, stype2gtype t2)]] | ¬t => γAneg t | 𝟘 => [] | 𝟙 => [[]] | SBase _ => [[]] end%stype. Fixpoint γApos (τ : GType) : list (list (GType * GType)) := match τ with | τ1 ∨ τ2 => γApos τ1 ++ γApos τ2 | τ1 ∧ τ2 => (fun T1 T2 => T1 ++ T2) <$> γApos τ1 <*> γApos τ2 | τ1 → τ2 => [[(τ1, τ2)]] | ¬t => γAneg t | 𝟘 => [] | 𝟙 => [[]] | GBase _ => [[]] | ? => [[(?, ?)]] end%gtype. Definition dom (τ : GType) : SType := ⋀ (fun S => ⋁ (fun '(ρ, _) => ρ⇑) <$> S)%stype <$> γApos τ. Fixpoint assignments {X : Type} (xs : list X) : list (list (X * bool)) := match xs with | [] => [[]] | (x :: xs) => cons <$> [(x, false); (x, true)] <*> assignments xs end. Definition partitions {X : Type} (xs : list X) : list (list X * list X) := (fun ys => (fst <$> filter snd ys, fst <$> filter (fun p => negb (snd p)) ys)) <$> assignments xs. Definition appResult (τ σ : GType) : GType := ⋁ (fun S => ⋁ (fun '(Q, Qbar) => ⋀ snd <$> Qbar) <$> filter (fun '(Q, Qbar) => negb (null Qbar) && (σ ̃≰! ⋁ fst <$> Q) && negb ((σ⇑ ∧ ⋁ (fun '(ρ, _) => ρ⇑) <$> Qbar) ≤! 𝟘)) (partitions S) )%gtype <$> γApos τ. Infix "∘" := appResult (at level 90, no associativity). Section SomeTheorems. Local Theorem sub_and_mono t1 t2 s1 s2 : t1 ≤ s1 -> t2 ≤ s2 -> (t1 ∧ t2) ≤ (s1 ∧ s2). Proof. intros p q. apply sub_and. - refine (sub_trans _ _ _ _ p). apply sub_and_l. - refine (sub_trans _ _ _ _ q). apply sub_and_r. Qed. Local Theorem sub_or_mono t1 t2 s1 s2 : t1 ≤ s1 -> t2 ≤ s2 -> (t1 ∨ t2) ≤ (s1 ∨ s2). Proof. intros p q. apply sub_or. - refine (sub_trans _ _ _ p _). apply sub_or_l. - refine (sub_trans _ _ _ q _). apply sub_or_r. Qed. Local Theorem sub_refl t : t ≤ t. Proof. pose proof sub_and_mono. pose proof sub_or_mono. pose proof bsub_refl. induction t; auto; now constructor. Qed. Local Theorem gradual_extrema_in_concretization τ : τ⇓ ∈ γ τ /\ τ⇑ ∈ γ τ. Proof. induction τ as [ | | | | ? [] ? [] | | ? [] ? [] | ? [] ? [] ]; simpl; auto. Qed. Local Theorem gradual_extrema_bounds τ : forall t, t ∈ γ τ -> τ⇓ ≤ t /\ t ≤ τ⇑. Proof. induction τ as [ | | | | ? IHl ? IHr | | ? IHl ? IHr | ? IHl ? IHr ]; simpl. - intros _ <-. repeat constructor. - intros _ <-. repeat constructor. - repeat constructor. - intros _ <-. repeat constructor. + apply sub_refl. + apply sub_refl. - intros [ | | | t1 t2 | | | ]; try contradiction. intros []. destruct (IHl t1); auto. destruct (IHr t2); auto. repeat constructor; auto. - intros _ <-. repeat constructor. + apply bsub_refl. + apply bsub_refl. - intros [ | | | | | t1 t2 | ]; try contradiction. intros []. destruct (IHl t1); auto. destruct (IHr t2); auto. split. + apply sub_and_mono; auto. + apply sub_and_mono; auto. - intros [ | | | | | | t1 t2 ]; try contradiction. intros []. destruct (IHl t1); auto. destruct (IHr t2); auto. split. + apply sub_or_mono; auto. + apply sub_or_mono; auto. Qed. Local Theorem cons_sub_reduction σ τ : σ ̃≤ τ <-> σ⇓ ≤ τ⇑. Proof. unfold lift2. split. - intros [s [t [? []]]]. apply (sub_trans _ s _). + now apply gradual_extrema_bounds. + apply (sub_trans _ t _). * assumption. * now apply gradual_extrema_bounds. - intros ?. exists (σ⇓), (τ⇑). split; try split. + apply gradual_extrema_in_concretization. + apply gradual_extrema_in_concretization. + assumption. Qed. Theorem sub_decide_agrees t s : t ≤ s <-> t ≤! s = true. (* Depends on the contents of junctDecide *) Admitted. Theorem cons_sub_decide_agrees σ τ : σ ̃≤ τ <-> σ ̃≤! τ = true. Proof. transitivity (σ⇓ ≤ τ⇑). - apply cons_sub_reduction. - unfold consSubDecide. apply sub_decide_agrees. Qed. Theorem cons_not_sub_reduction σ τ : σ ̃≰ τ <-> ~(σ⇑ ≤ τ⇓). Proof. unfold lift2. split. - intros [s [t [? [? p]]]] n. apply p. apply (sub_trans _ (σ⇑) _). + now apply gradual_extrema_bounds. + apply (sub_trans _ (τ⇓) _). * assumption. * now apply gradual_extrema_bounds. - intros n. exists (σ⇑), (τ⇓). split; try split. + apply gradual_extrema_in_concretization. + apply gradual_extrema_in_concretization. + assumption. Qed. Theorem cons_not_sub_decide_agrees σ τ : σ ̃≰ τ <-> σ ̃≰! τ = true. Proof. transitivity (~(σ⇑ ≤ τ⇓)). - apply cons_not_sub_reduction. - unfold consNotSubDecide. transitivity (σ⇑ ≤! τ⇓ <> true). + apply not_iff_compat. apply sub_decide_agrees. + transitivity (σ⇑ ≤! τ⇓ = false). * apply not_true_iff_false. * symmetry. apply negb_true_iff. Qed. End SomeTheorems. Section SomeContradictions. Inductive PartialEvalResult : Type := | EvBottom | EvUnknown | EvTop. Local Fixpoint partialEval (t : SType) : PartialEvalResult := match t with | 𝟘 => EvBottom | 𝟙 => EvTop | SBase _ => EvUnknown | _ → _ => EvUnknown | ¬t => match partialEval t with | EvBottom => EvTop | EvUnknown => EvUnknown | EvTop => EvBottom end | t1 ∧ t2 => match partialEval t1, partialEval t2 with | EvBottom, _ => EvBottom | _, EvBottom => EvBottom | EvUnknown, _ => EvUnknown | _, EvUnknown => EvUnknown | _, _ => EvTop end | t1 ∨ t2 => match partialEval t1, partialEval t2 with | EvTop, _ => EvTop | _, EvTop => EvTop | EvUnknown, _ => EvUnknown | _, EvUnknown => EvUnknown | _, _ => EvBottom end end%stype. Local Theorem partial_eval_mono t s : t ≤ s -> match partialEval t, partialEval s with | EvBottom, _ => True | _, EvTop => True | EvUnknown, EvBottom => False | EvUnknown, _ => True | EvTop, _ => False end. Proof. intros p. induction p. all: repeat first [ progress (simpl; auto) | destruct (partialEval _) ]. Qed. Local Theorem top_nle_bottom : ~(𝟙 ≤ 𝟘). Proof. intros n. apply (partial_eval_mono _ _ n). Qed. Theorem cons_sub_nontrans : ~(forall g h k, g ̃≤ h -> h ̃≤ k -> g ̃≤ k). Proof. intros n. enough (p : 𝟙 ̃≤ 𝟘). - apply top_nle_bottom. unfold lift2 in p. simpl in p. now destruct p as [? [? [-> [->]]]]. - apply (n _ ?%gtype _). + unfold lift2. simpl. exists 𝟙%stype, 𝟙%stype. split; auto. split; auto. constructor. + unfold lift2. simpl. exists 𝟘%stype, 𝟘%stype. split; auto. split; auto. constructor. Qed. End SomeContradictions. End Types. (* Have to redeclare all notations now that the section is closed *) Declare Scope stype_scope. Delimit Scope stype_scope with stype. Bind Scope stype_scope with SType. Notation "𝟘" := SBottom : stype_scope. Notation "𝟙" := STop : stype_scope. Notation "¬ t" := (SNot t) (at level 75) : stype_scope. Infix "→" := SArrow (at level 99, right associativity) : stype_scope. Infix "∧" := SAnd (at level 85, right associativity) : stype_scope. Infix "∨" := SOr (at level 85, right associativity) : stype_scope. Notation "⋀ xs" := (fold_right SAnd STop xs) (at level 85) : stype_scope. Notation "⋁ xs" := (fold_right SOr SBottom xs) (at level 85) : stype_scope. Declare Scope gtype_scope. Delimit Scope gtype_scope with gtype. Bind Scope gtype_scope with GType. Notation "𝟘" := GBottom : gtype_scope. Notation "𝟙" := GTop : gtype_scope. Notation "?" := GAny : gtype_scope. Notation "¬ t" := (GNot t) (at level 75) : gtype_scope. Infix "→" := GArrow (at level 99, right associativity) : gtype_scope. Infix "∧" := GAnd (at level 85, right associativity) : gtype_scope. Infix "∨" := GOr (at level 85, right associativity) : gtype_scope. Notation "⋀ xs" := (fold_right GAnd GTop xs) (at level 85) : gtype_scope. Notation "⋁ xs" := (fold_right GOr GBottom xs) (at level 85) : gtype_scope. Infix "≤" := Sub (at level 70, no associativity). Infix "≤!" := subDecide (at level 70, no associativity). Notation "τ ⇓" := (gradualMinimum τ) (at level 65). Notation "τ ⇑" := (gradualMaximum τ) (at level 65). Infix "̃≤" := (lift2 Sub) (at level 70, no associativity). Infix "̃≤!" := consSubDecide (at level 70, no associativity). Infix "̃≰" := (lift2 (fun s t => ~(s ≤ t))) (at level 70, no associativity). Infix "̃≰!" := consNotSubDecide (at level 70, no associativity). Infix "∘" := appResult (at level 90, no associativity). Section Example. Inductive BaseType := | object | int | str | bytes | float. Scheme Equality for BaseType. Definition SBase' := @SBase BaseType. Coercion SBase' : BaseType >-> SType. Definition GBase' := @GBase BaseType. Coercion GBase' : BaseType >-> GType. Definition decideSubclass (b c : BaseType) : bool := BaseType_beq b c || match b, c with | _, object => true | _, _ => false end. Program Instance subtype_decidable_basetype : SubtypeDecidable BaseType := {| bsubDecide := fun conjs disjs => anyb id (decideSubclass <$> conjs <*> disjs) || anyb (fun c => match c with object => true | _ => false end) disjs || (anyb (fun c => match c with int => true | _ => false end) conjs && anyb (fun c => match c with str => true | _ => false end) conjs) |}. Next Obligation. unfold reflexive. intros []; simpl; auto. Qed. Next Obligation. unfold transitive, anyb. intros b c d. destruct b, d; simpl; auto; destruct c; simpl; auto. Qed. Eval cbn in (int → float) ∧ (str → bytes) ∘ int. (* = (((float ∧ bytes ∧ 𝟙) ∨ (float ∧ 𝟙) ∨ 𝟘) ∨ 𝟘)%gtype : GType *) End Example. ``` Note: This doesn't contradict what was said about the set-theoretic view not allowing this despite the subtyping relation, The rules proposed in this paper and encoded in the coq program there treat the bottom type not as participating in subtyping as most people are aware of the term, but redefine subtyping more generally in such a way that it does apply.

[eltoder]

@mikeshardmind

For example, Haskell and Rust's definitions both match more closely to what is described in this issue than what type checkers are currently doing.

Not really. Haskell allows undefined to be used in place of an expression of any type. For example, this type checks and runs:

fn :: Int -> Int
fn x = 1
main = print $ fn undefined

It is considered a feature: https://wiki.haskell.org/Undefined

A similar example works in Rust:

use std::process;

fn test(x: u32) -> u32 {
    x
}

fn main() {
    #[allow(unreachable_code)]
    test(process::exit(1));
}

You have to allow unreachable code, but this is not a type error.

This example works in Scala, Kotlin, TypeScript and probably others (with respective syntax changes):

trait Trait:
  def foo: Int

class Impl extends Trait:
  override def foo: Nothing = throw Exception("test")

object Hello {
  def main(args: Array[String]) = {
    val obj: Trait = new Impl
    print(obj.foo)
  }
}

[mikeshardmind]

@mikeshardmind

For example, Haskell and Rust's definitions both match more closely to what is described in this issue than what type checkers are currently doing.

Not really. Haskell allows undefined to be used in place of an expression of any type. For example, this type checks and runs:

fn :: Int -> Int
fn x = 1
main = print $ fn undefined

It is considered a feature: https://wiki.haskell.org/Undefined

The very first line of that page: states: "You can put it anywhere and it will compile. When evaluated, it throws an exception "undefined". But thanks to laziness you can put it anywhere you've not written yet:" This is not the same as type checkers allowing this and claiming it to be safe, in fact, this is haskell specifically telling you that use of it isn't safe.

A similar example works in Rust:

use std::process;

fn test(x: u32) -> u32 {
    x
}

fn main() {
    #[allow(unreachable_code)]
    test(process::exit(1));
}

You have to allow unreachable code, but this is not a type error.

This isn't an example of it being a value, Please read again about the difference between a value and a lack of a value, it matters. On top of this, Rust correctly detects unreachable code and you are opting out of the safety it provides visibly here.

This example works in Scala, Kotlin, TypeScript and probably others (with respective syntax changes):

trait Trait:
  def foo: Int

class Impl extends Trait:
  override def foo: Nothing = throw Exception("test")

object Hello {
  def main(args: Array[String]) = {
    val obj: Trait = new Impl
    print(obj.foo)
  }
}

This is also an example of something throwing an exception and not returning a value at all, not of something having a value of the bottom type.

[DiscordLiz]

@mikeshardmind nudged me to put this comment separately rather than in a collapsible section over in discord, but what definition of "subtyping" is used matters here too. The set-theoretic model can be (see the proof above) reconciled with a general type connective which the paper it was proved in defines as their version of subtyping, but this use isn't consistent with what current type checkers are allowing. (And indeed the paper takes the time to lay out how prior definitions of subtyping are lacking)

We have a very complex issue here where there is lots of good well proven theory, and no good definitions that are commonly accepted in python to actually communicate the issue due to lack of specification in PEPs.

[mikeshardmind]

I'm gonna start with a few things here.

1. Never indicates a complete lack of a value, and is a type can't exist at runtime.
2. The example below is clearly broken. Mypy allows it full-stop, pyright actually complains about overriding foo this way.

from typing import Never, reveal_type

class A:
    @property
    def foo(self) -> int:
        return 1

class B:
    @property
    def foo(self) -> str:
        return "okay"

class AB(A, B):
    foo: Never  # mypy allows this

def takes_a(x: A) -> bytes:
    return x.foo.to_bytes(8)

def takes_b(x: B) -> bytes:
    return x.foo.encode()

if __name__ == "__main__":
    obj = AB()
    reveal_type(AB().foo)  # Revealed type is "<nothing>" (pyright "Never", both wrong) 
    print(obj.foo)
    print(takes_a(obj))  # This one works because A is first in MRO, but we can't even just isinstance check, it's an instance of A and B
    print(takes_b(obj))  # This one fails for the same reason

And the actual output:

PS C:\Users\michael> py .\t.py
Runtime type is 'int'
1
b'\x00\x00\x00\x00\x00\x00\x00\x01'
Traceback (most recent call last):
  File "C:\Users\michael\t.py", line 31, in <module>
    print(takes_b(obj))
          ^^^^^^^^^^^^
  File "C:\Users\michael\t.py", line 23, in takes_b
    return x.foo.encode()
           ^^^^^^^^^^^^
AttributeError: 'int' object has no attribute 'encode'

As described above, and clearly demonstrated with the toy example here, Never isn't consistent with other types for the purposes of safe replacement, and treating it as such not only allows nonsensical subclasses, but also breaks expectations of checked code in terms of what may be passed to it. While there are definitions of subtyping that would apply between Never and other types, they exclude this broken behavior.

Any code relying on this behavior is fundamentally broken, and I don't think this requires a "Breaking change" or transitionary period to fix as

1. All uses which would be "Broken" by fixing this already are broken and this would only highlight those issues.
2. This wasn't officially specified anywhere. This was a decision type checkers made without a corresponding specification.

Pyright's errors via pylance in VSC with strict:

Mypy's output with --strict (Showing the lack of error isn't just a settings issue) via mypy playground on latest:

main.py:28: note: Revealed type is "<nothing>"
Success: no issues found in 1 source file

A more dangerous example would involve the return types both working for takes_a and takes_b purely by implementation accident, but returning different types than expected polluting where the type issues even came from.

Now if anyone can argue that it should be allowed and keep in mind the effects on library code taking in user-provided classes with this information and impact demonstrated, I'd love to hear the argument, because as it stands it sounds like the only argument against it is "Well that's not what we've been doing it and changing it might be hard" (Appeal to tradition or status quo) or "other language does this" (Appeal to authority) even though clearly there is a detectable issue here.

My preferred resolution on this involves clearly stating that Never isn't consistent with other types (officially somewhere) and that Never remains fine for things that truly don't return a value of any type, but you can't specify a function, class, or other annotation having a dependence on Never without it specifically indicating erroneous or unreachable code of some sort.

[erictraut]

Never indicates a complete lack of a value

You state that with conviction, but that isn't how Never has been understood in the past by the Python typing community. There may or may not be good reasons to change its meaning in the Python type system. None of the reasons you've presented so far seem very compelling to me, but I'm trying to remain open-minded. Such a redefinition will likely have backward-compatibility implications, so it would need to be well motivated. Citing an academic paper on type theory will probably be insufficient to sway people. I personally enjoy geeking out about type theory, but pragmatism tends to trump theory in the Python community. There are other programming languages where "purity of theory" is valued much more highly (Haskell comes to mind), but Python tends to be further on the "pragmatism" side of that spectrum.

If you want to argue in favor of a change to the Python type system, a more effective approach is to demonstrate that such a change would solve some real problem that Python developers are facing today. What is the problem you're trying to solve? How prevalent is the problem? Do we have evidence to back this up (e.g. bug reports or feature requests in the mypy issue tracker or StackOverflow posts)?

---

pyright actually complains about overriding foo this way

Pyright is not complaining about the Never type. It's complaining about the fact that you're overriding a property with a variable. It will emit this regardless of which type you use in the override. Mypy is more lax in this case and allows properties to be overridden by variables. So this has nothing to do with Never.

---

And the actual output [shows a runtime crash]

The crash is because the variable foo was never assigned a value in class AB. This can happen with any class-scoped variable regardless of its type. This is not specific to Never.

Consider the following modified example. This also type checks without error in both mypy and pyright but crashes at runtime. There is no Never involved in this example, but it is otherwise completely analogous to your code above.

from typing import Protocol

class _SupportsToBytes(Protocol):
    def to_bytes(self, length: int) -> bytes:
        ...

class _SupportsEncode(Protocol):
    def encode(self) -> bytes:
        ...

class _SupportsEncodeAndToBytes(_SupportsToBytes, _SupportsEncode, Protocol):
    ...

class A:
    foo: _SupportsToBytes = 1

class B:
    foo: _SupportsEncode = ""

class AB(A, B):
    foo: _SupportsEncodeAndToBytes

def takes_a(x: A) -> bytes:
    return x.foo.to_bytes(8)

def takes_b(x: B) -> bytes:
    return x.foo.encode()

if __name__ == "__main__":
    obj = AB()
    print(obj.foo)
    print(takes_a(obj))
    print(takes_b(obj)) # Crash

I think your example demonstrates that there are bugs that can go uncaught by static type checking. That's something that no one would dispute. It doesn't demonstrate why Never should be treated differently from other types.

Do you have other examples?

[randolf-scholz]

@erictraut Replacing a non-Never annotated object with a Never annotated object violates certain aspects of LSP, specifically (LSP-exception)

(LSP-exception) New exceptions cannot be thrown by the methods in the subtype, except if they are subtypes of exceptions thrown by the methods of the supertype.

Also, pre- and post-conditions are in some sense violated this way (https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1700959278).

Imo, the main issue here is uncertainty. Since it is not explicitly codified, it is unclear what contract a type annotation like

class Foo:
    bar: int

really promises. Most people would probably say that it guarantees that instances of Foo are guaranteed to have an attribute bar which is an instance of int.

But clearly, if a subclass SubFoo is allowed to substitute bar with Never, then (LSP-exception) is violated, since looking up said attribute never terminates or raises an exception. Therefore, SubFoo cannot safely be used as a substitute for Foo without wrapping everything in try-except blocks.

The Python community should decide whether they want the typing system to support (LSP-exception), or a weaker version of it, like the one I proposed in https://github.com/CarliJoy/intersection_examples/issues/5#issuecomment-1700959278, and clearly communicate this decision.

[mikeshardmind]

@erictraut

The crash is because the variable foo was never assigned a value in class AB. This can happen with any class-scoped variable regardless of its type. This is not specific to Never.

No, this misunderstands the example here. Simply annotating Never without replacing the inherited methods/properties is accepted, making the annotation of Never incorrect. The crash isn't because the attribute doesn't exist, and you can see in the traceback exactly what happened.

[erictraut]

Did you look at my modified example? Try running it. My version produces exactly the same stack trace and error message but doesn't involve Never. I don't see how the two are any different, yet my version doesn't involve Never.

[mikeshardmind]

@erictraut Your modified example also involves annotating something incorrectly. This is detectable and isn't being detected.

The situation with Never matters here even if this issue of detection is resolved. You've also fundamentally sidestepped the underpinning question by turning that into a protocol. If there are two incompatible types, it shouldn't be possible to subclass both by simply placing a Never there.

[mikeshardmind]

It doesn't demonstrate why Never should be treated differently from other types.

1. Because it isn't a type in the same sense that int is. @DiscordLiz already explained how neither Any nor Never are singular types up above pretending Never is a singular type rather than the bottom type, (ie. the empty set of types or any other reasonable interpretation of what a bottom type is in a type system) is how we got here.
2. Because allowing this creates LSP violations, see the information provided by @randolf-scholz
3. Because any code relying on the existence of an object with a type of Never at runtime is already broken. Fixing this can't break anything, only inform people they are already broken.
4. The feature added at the same time, as Never, assert_never, seems to be written correctly understanding that if you reach a point where you have an expectation of a type only being Never, you have unreachable code.

If you want to argue in favor of a change to the Python type system, a more effective approach is to demonstrate that such a change would solve some real problem that Python developers are facing today. What is the problem you're trying to solve? How prevalent is the problem? Do we have evidence to back this up (e.g. bug reports or feature requests in the mypy issue tracker or StackOverflow posts)?

First of all, @eltoder already showed some relevant mypy bugs

But more to the point, where is it specified that Never is a subtype of and a suitable replacement for all other types? As far as I can ascertain, this is just a decision that type checkers made without it ever being specified and with a lack of understanding of what is correct from the point of view of theory. While it is very understandable how such a lack of understanding or misconception could occur, that's part of why these things should be specified and that the specification should happen in the open* not "oh, we implemented it this way, and we don't have a specification for it, guess you're stuck with it".

The issue it solves to have a correct specification is that future additions to the specification are building on a solid foundation not needing mountains of exceptions to rules because of an accumulation of errors.

Intersections, Not, and Stricter TypeGuards (Which use both intersections and Not in describing their resulting equivalence) are impossible to have a coherent set of rules and behaviors if Never is treated as a type, rather than an (empty) set of types. That's how this discussion came here, realizing that type checkers are allowing something that fundamentally breaks what is being worked on.

* And for the record, the typing-sig mailing list is the least visible place such a discussion could occur. Even the issue trackers of individual type checkers see more users regularly, and those do not have the barrier to entry of waiting for the mailing list administrator to manually review posts from new users which delays feedback if its even seen to begin with. Mailing lists are atrocious for modern-day collaborative discussion by comparison to other tools at the disposal of the community. (They still have a very clear place for announcements)

[erictraut]

Your modified example also involves annotating something incorrectly.

Can you elaborate? What is annotated incorrectly in my example?

I agree that there's a bug in my example, but I don't think it involves an incorrect annotation. The bug is that AB.foo is not assigned a value that conforms with its annotation, so the underlying value of A.foo is leaking through at runtime. Would it be possible for a static type checker to detect this condition? Perhaps, but such a check would also produce many false positives for correctly-written Python code. That's why Python type checkers do not currently check for this case. It would simply be too noisy and wouldn't catch many real-world bugs.

Let's assume that a type checker could reasonably enforce that a declared class variable must be assigned a value within the class' implementation. Your original example and my example would both trigger that error. In my example, I could fix that error by assigning a value to AB.foo that conforms to the _SupportsEncodeAndToBytes protocol. In your example, any attempt to address that error by assigning a value would result in a different type error because it's impossible to assign a value that conforms to Never or a value that subclasses from both int and str.

So I assert once again that your example does not demonstrate why Never should be treated differently from other types. You may be able to produce other examples that support your position, but this example does not, at least as I see it.

---

Intersections, Not, and Stricter TypeGuards ... are impossible to have a coherent set of rules and behaviors if Never is treated as a type.

I'll once again note that TypeScript is an example of a popular programming language that supports gradual typing, intersections, and strict type guards, and it treats Never the same way that Python does today. (TypeScript doesn't support negated types, but I'm not aware of any popular programming language that does.) You've said that you perceive TypeScript to be "incorrect" from a type theory perspective. I personally know the developers responsible for TypeScript, and they are both very knowledgable about type theory and very pragmatic when it comes to prioritizing usability over purity. I admit that I'm not familiar with your background or credentials, but I think I'm safe in assuming that you have less experience than Anders Hejlsberg in developing programming languages and type systems 😀. I'm not saying that your viewpoint is wrong, but I would caution you against dismissing TypeScript as an unworthy exemplar.

TypeScript isn't alone in treating Never as the subtype of (and therefore assignable to) all other types. Wikipedia and many other sources define "bottom type" as the subtype of all other types in a type system. You and @DiscordLiz have asserted that wikipedia is wrong or that it's relying a different definition of subtype. You've pointed to an academic paper on gradual typing (published several years after the Python type system was created) that indicates that the "bottom type" should be treated as though it's outside normal subtyping rules in a type system. That doesn't appear to be a universally-held opinion, yet you keep asserting it as though it's an indisputable fact.

I appreciate the perspective you bring to this discussion, but I don't think you've made a clear and convincing case that we should make a change to the type system that results in a breaking change.

---

I agree with you that there is value in formalizing the Python type specification. As you point out, this is an important foundation upon which any major new typing features should be built. Ideally, this specification should be developed in an open and collaborative manner so it has buy-in from the broader typing community, and it should employ terminology that is clearly defined and used consistently throughout the spec. (In the discussions about intersections, I've noted that new terms are being injected into the conversation with the assumption that everyone has a common understanding of terms like uninhabited type, static type, gradual type, etc., and this is leading to confusion.) I also think it's important for this formalization to be done holistically, not piecemeal. If it's done piecemeal, it likely won't hold together, and inconsistencies will creep in.

As @DiscordLiz mentioned at the top of this thread, Kevin Millikin started an effort to produce a formalization. That effort appears to have stalled. You've stated that there are some aspects of this earlier document that you disagree with, and there are other aspects that require refinement, clarification, additional review, and input from others. Perhaps you'd like to pick up the mantle and drive that effort to completion?

---

Here's some new empirical data that may help inform this discussion. I did an experiment earlier today where I changed pyright to treat Never in the manner you're suggesting. It's an easy change — just a couple of lines of code. I then ran pyright on 28 sizable typed source bases, some of them private and some of them public. Of those, the type checking results for 11 of the 28 (about 40%) were unaffected. For the remaining 17 code bases (a little over 60%), new type errors were generated, an average of about ten per code base. That's not a huge number, but if you multiply that by the total number of typed code bases, it represents a level of churn that is not insignificant.

I looked at the errors to get a sense for their causes. I didn't see any cases that represented actual bugs (unintended runtime behaviors). About a third were attributable to incorrect type annotations that would be good to fix regardless of whether the definition of Never is changed. The remainder represent uses of Never that are legitimate based on its current definition. Most of these cases would be straightforward to change, but doing so would be "busy work" for the maintainers.

Based on this information, I propose that we do not change the definition of Never at this time. Doing so would be disruptive and solve few if any problems in the short term. This doesn't preclude us from making a change later as part of a holistic effort to formalize the type system. If you or @DiscordLiz are interested in spearheading such an effort (either using Kevin Millikin's document as a starting point or starting from scratch), I'd be happy to participate. I recommend doing this before proceeding with the effort to add intersection types to the type system, since those concepts will necessarily build upon the formalized definitions.

[mikeshardmind]

@erictraut

Can you elaborate? What is annotated incorrectly in my example?

I agree that there's a bug in my example, but I don't think it involves an incorrect annotation. The bug is that AB.foo is not assigned a value that conforms with its annotation, so the underlying value of A.foo is leaking through at runtime.

This is the incorrect annotation. The MRO isn't an ignorable detail, A.foo is part of the definition of AB. If you annotate AB.foo, it needs to be correct for AB.foo, which is defined in A. If you use the types I had in my example rather than the protocols you swapped them for, the issue persists and shows up with Never for LSP as you have types that should be considered irreconcilable types that are being reconciled with Never. (See next section for the additional issues of nominal subtyping vs typescript's use)

I'll once again note that TypeScript is an example of a popular programming language that supports gradual typing, intersections, and strict type guards, and it treats Never the same way that Python does today. [...] You've said that you perceive TypeScript to be "incorrect" from a type theory perspective.

Typescript over-elevated pragmatism in a few ways which has led to it having a few subtle ways it disagrees with type theory. These aren't major issues for Typescript, and while I disagree with them, I accept their pragmatism for typescript; Applying them to Python has more issues. Typescript isn't a good exemplar for Python less because of this and more because Typescript only has structural subtyping, not nominal. Typescript therefore doesn't have the same concepts for the safe substitution of subclasses, and we have to reevaluate the decisions Typescript has made to see if they hold up for Python before just accepting them for working in a similar language. I believe there to be major issues that arise adopting the less rigorous use of the bottom type due to this in Python.

(TypeScript doesn't support negated types, but I'm not aware of any popular programming language that does.)

Most statically typed languages do so implicitly not explicitly. I've been an advocate for explicit negation in python to reduce the number of necessary runtime checks that occur via negative inference that many actually statically typed languages don't need to do at runtime that instead happens at compile time with type dispatch.

Based on this information, I propose that we do not change the definition of Never at this time. Doing so would be disruptive and solve few if any problems in the short term.

The primary motivation for this discussion being brought here was the impact on future work (Intersections) and the need for a definitive answer on this. I believe that building Intersections on the current (Type checker adopted) behavior of Never to be perilous due to the number of edge cases which simply will be self-resolving with the general rules instead should we adjust this.

I also think it's important for this formalization to be done holistically, not piecemeal. If it's done piecemeal, it likely won't hold together, and inconsistencies will creep in.

As DiscordLiz mentioned at the top of this thread, Kevin Millikin started an effort to produce a formalization. That effort appears to have stalled. You've stated that there are some aspects of this earlier document that you disagree with, and there are other aspects that require refinement, clarification, additional review, and input from others. Perhaps you'd like to pick up the mantle and drive that effort to completion?

Without full community buy-in that puts a pause on ongoing additions to the type system until this is done, I don't think such a holistic effort is pragmatically possible at this time. (edit: possible, but difficult. I'm seeing if I can expend the time necessary to expedite this in a fashion that would reduce the churn involved in reconciling with other new things)

Whoever took it up would be constantly reconciling anything new with it and having to make hard decisions on larger breakages all at once, and then all of those breakages whatever they may be, need to be accepted as a package deal, thereby causing potentially much larger churn all at once. The benefit is more clear in that case, but I don't know how pragmatic the larger churn all at once would be even with the benefit being more clear. (Edit: but as @DiscordLiz mentions below, there aren't many things in total that would change for most users of typing, so even as a package deal, maybe this isn't insurmountably large an ask)

There have also been a few recent changes that have very ambiguous meanings, such as intentionally subclassing from Any, and the difference between directly subclassing the top type vs having an Unknown base. (instead of implementing support for __getattr__ despite that PEP 484 suggests a very similar method for modules with the need to inform type checkers of not typed members existing that should not be assumed an error)

I don't fully agree that it is necessary to do this holistically rather than piecemeal, but I think that very few people would be able to meaningfully participate if it wasn't done holistically because it would require unquestionably correct definitions done in order of most fundamental parts of the type system and building upon them in order. I think this is extremely hard to ask of most people, especially given the interactions with gradual typing.

You've pointed to an academic paper on gradual typing (published several years after the Python type system was created) that indicates that the "bottom type" should be treated as though it's outside normal subtyping rules in a type system. That doesn't appear to be a universally-held opinion, yet you keep asserting it as though it's an indisputable fact.

The paper linked includes proof that treating it the other way is insufficient, and there's a translation of the paper's proofs to a formal proof engine with some basic examples included in it for how the paper prescribes interactions with python's types up above as well. so yes, I'm treating it as an indisputable fact because there is proof that it is not merely an opinion, but a provable fact of the interactions between these.

Many of the original decisions in pythons type system have had issues of specification. (Here's one for unions having slightly incorrect specifications: https://github.com/CarliJoy/intersection_examples/issues/22 which formally shows something that has led to minor divergence between type checker behavior, which was brought up at the typing summit in 2022.)

Python was pushing forward with gradual typing well before many of the stronger proofs of what is correct had been proven, and that should be applauded, but I would hope that we can look at things that are actually proven to improve the type system going forward and have fewer special cases needed by making small adjustments that fix the few places where formal theory is in disagreement. This gives us a stronger foundation, still allows gradual typing and allows future features to build more fearlessly as they can defer either entirely to what is proven already for the correct interpretation in many cases or use what is provable already to check for consistency.

Those who did the initial work on Python's type system were exceptionally close to being entirely correct with regard to now proven theory, and that is no small feat.

I think I'm safe in assuming that you have less experience than Anders Hejlsberg in developing programming languages and type systems

Not everyone lives such that their knowledge and experience is a matter of public record. I would caution from such appeals to credentials when we can discuss a matter plainly on the facts. (though doing this is undeniably difficult, as we have to distinguish from what is specified, what is conventionally accepted even if not specified, and what definitions of terms we are using where there isn't a singular definition adopted by the type system already)

I don't think it was your intention to use this in a discrediting manner and I personally have not taken it this way, but there have been multiple expressions in both public and less public places that contributing to Python's type system has barriers to entry that are artificial, or that certain things are only discussed with people already in "the club". While this may not be strictly true, even the appearance of such impacts some people's willingness to even try to participate. While this does not seem to have been your intent, I would advise that such statements could contribute to the existing sentiment that it is hard to meaningfully contribute to this without already being involved. I've been a bit loud on this more process-issue bit in particular because I've seen an impact of it on someone I consider a friend not wanting to even bother on this despite finding it to be something important.

[DiscordLiz]

Based on this information, I propose that we do not change the definition of Never at this time. Doing so would be disruptive and solve few if any problems in the short term. This doesn't preclude us from making a change later as part of a holistic effort to formalize the type system. If you or @DiscordLiz are interested in spearheading such an effort (either using Kevin Millikin's document as a starting point or starting from scratch), I'd be happy to participate. I recommend doing this before proceeding with the effort to add intersection types to the type system, since those concepts will necessarily build upon the formalized definitions.

@erictraut I would not be willing to spearhead that effort. I am willing to work with anyone (cough @mikeshardmind you are pretty invested in this) doing so if and only if there is a clear intent from the community that

1. The formalization is to be based on what is provable while remaining pragmatic.
2. Whatever the conclusions of it are should be kept up to date in a living specification document.
3. Implementations should follow the specification.
4. Implementations should not check things which are type issues that do not have specified behavior without it being clearly marked as outside of specification.
5. Any such checks outside of specification should lead to exploring if the specification should be expanded, and should be removed or adjusted if they become conflicting with the living specification.
6. Static analysis tools may continue to check for non-type based issues without specification, but should be encouraged to collaborate on specification of what may be correctly detected here as well. I believe there should be a section in the living specification of the type system for non-type issues which are correctly detectable in the presence of type information. Two existing examples of this are exhaustive type matching at runtime and unreachable code detection.

numbers 2, 4, 5, and 6 are of particular importance to me as they result in a source of truth that is not subject to bugs in implementation becoming the behavior without consideration, while allowing type checkers some freedom to check more than just what is fully agreed upon already, allowing room for heuristic checks which may not be proven or accepted yet, but still valuable to developers.

Being based on what is provable does not preclude any existing use case for gradual typing, but my observations lead me to think that code that directly uses Never or Any would be the code most likely to need more than only minor changes. It appears to me that outside of the top and bottom type, people are already either at the theory-correct conclusions for how types should behave or are correct by special case that applies to their use. I think there are two changes to the top type that would happen here as well if we go with theory-correct definitions, but that most users would not experience any meaningful difference on these changes as they are subtle.

I do think that the changes formalization based on theory would lead to would actually improve the usability for gradual typing users as well, not just current users of strict modes of type checkers. Having well defined specification here could allow implicit Any on untyped code as opt-in behavior be more safe than it currently is, though I'd prefer not to get too far into that hypothetical at this point in time.

I've been a bit loud on this more process-issue bit in particular because I've seen an impact of it on someone I consider a friend not wanting to even bother on this despite finding it to be something important.

@mikeshardmind I've made my displeasure in certain interactions with this known, but I hope you aren't doing this only because of that and I hope you're aware that you are also coming across a bit more confrontational as a result of taking that on.

[mikeshardmind]

I'll see if I can get some time approved to work on this as part of my actual day job. If so, I'm willing to attempt to not just pick up formalization efforts where they have stalled, but spearhead it. If not, I need to think about this a bit more to see if I'm willing to put in the time required.

I have a feeling that numbers 2 and 3 on your list of conditions @DiscordLiz would be a requirement for my employer to even consider me spending work hours on this. However, we heavily make use of static analysis and have fully typed code, so there is a case for my employer to be invested in such an outcome and I do think I can present this in a way that they may truly consider it. To be clear though, my employer's involvement in allowing me time to work on this would (on my end) be predicated on them not interfering in the process. My decisions on this would need to remain independent of their goals (though I believe the general case being correct aligns with my employer's use of static analysis anyhow) and something that I can evaluate only on the merits that are generally applicable or I'd not work on it on company time.

I'm also not being loud strictly because of what you've said. I've always held that good ideas can come from anywhere and that we should evaluate ideas and arguments on their own merits. I hadn't noticed that I was being that much more argumentative, so my apologies if anyone else has perceived me as being hostile as a result, the intent has been to reduce the barriers to entry on this and get the focus to be on the facts.

[mikeshardmind]

class A:
    a: int

class B(A):
    a: bool

def foo(a: A) -> None:
    a.a = 2

B().a = 2 # not ok

foo(B()) # ok

Something from the Python Discord's typing channel that shows that even though Never is in question in the issue here, there are ways to demonstrate other issues with what type checkers currently allow in the same place that don't require protocols or Never.

The problem here is still the LSP violation described above. Something that can be both used and assigned to is only being checked for variance as if it is only being used, not as if it also needs to be suitable to assign to in replacement. There's an open mypy issue going back to 2017 for this one.

Fixing this may implicitly solve most of the perceived issues with Never, though I believe the issues with Never are fundamental enough to still require their own attention and more concrete specification.

[diabolo-dan]

The following scenario demonstrates the problem. Consider the following program fragment: let q : [x : Int] = [x = 5, y = true] in 〈body〉 According to standard subtype-based reasoning, the body cannot access the y field of the record. Such modular reasoning is a hallmark of static typing, and programmers who mix static and dy- namic typing want to reason about their code using static types where available [Tunnell Wilson et al. 2018]. Unfortunately, the following completed GTFL. program compiles and runs successfully: let q : [x : Int] = [x = 5, y = true] in (q :: ? :: [x : Int, y : Bool]).y In essence, casting q to the unknown type and then back to a record type exposes the extra field

From the referenced paper https://arxiv.org/pdf/2010.14094.pdf for some context.

This is listed as one of the two motivating example (the other is about runtime performance for tail recursion), but the behaviour seems correct to me: assuming ? as Any, then "upcasting" to Any and then "upcasting" to a different type seems perfectly reasonable. (if ? is object, then the example would require an explicit cast, which could skip the ? part entirely).

You may disagree, but to present the paper to make the strong claim:

I'm treating it as an indisputable fact because there is proof that it is not merely an opinion, but a provable fact of the interactions between these

Without any acknowledgement that the assumptions of the proof may not be universally accepted in the python typing community (or referencing what the assumptions are directly), seems a bit misleading.

[DiscordLiz]

This is listed as one of the two motivating example (the other is about runtime performance for tail recursion), but the behaviour seems correct to me: assuming ? as Any, then "upcasting" to Any and then "upcasting" to a different type seems perfectly reasonable. (if ? is object, then the example would require an explicit cast, which could skip the ? part entirely).

Casting incorrectly doesn't make a type system's being incorrect correct it makes a programmer who does this without concern for the underlying behavior incorrect. The paper is calling out the issue with the existing definition here, the extra field that materializes and that the program works does not mean that this behavior is well defined by type systems.

Without any acknowledgement that the assumptions of the proof may not be universally accepted in the python typing community (or referencing what the assumptions are directly), seems a bit misleading

The assumptions of that paper are pretty bland, but it's safe to say that if someone is linking a paper to justify something, they are expecting that people read it and evaluate it for themselves. If I or anyone else was going to argue from base principles without leaning on existing research, the assumptions need to be included. If someone links a paper to claim something, it's safe to assume they are claiming the assumptions hold and if you have a problem with that, challenge those assumptions rather than just try and win a gotcha for them not writing word for word how the paper translates to this context.

seems a bit misleading

speaking of misleading, you didn't link the referenced paper where you wrote "From the referenced paper https://arxiv.org/pdf/2010.14094.pdf for some context.", this is a different paper that happens to agree with what was referenced above.

[mikeshardmind]

When I said

I'm treating it as an indisputable fact because there is proof that it is not merely an opinion, but a provable fact of the interactions between these

I was quite clear that I believe the assumptions are sound. If you don't believe that they are or think that rather general assumptions that hold across multiple type systems should not be used for python for some reason, please do explain yourself.

There are also direct examples in this thread that show an issue with current type checker behavior in this context both with and without the presence of Never, so it might do to defer to theory instead of to implementations that have clear and demonstrable errors.

[diabolo-dan]

Casting incorrectly doesn't make a type system's being incorrect correct it makes a programmer who does this without concern for the underlying behavior incorrect.

That's my point.

the extra field that materializes and that the program works does not mean that this behavior is well defined by type systems.

The behaviour can be well defined. I.e. you've gone through Any, so the behaviour is defined as not protected by the type system.

In this case the code works, but that's incidental from the type perspective, the logic would be the same as for:

let q : [x : Int] = [x = 5] in (q :: ? :: [x : Int, y : Bool]).y

which obviously crashes, but I wouldn't expect to raise a type error.

The paper is calling out the issue with the existing definition here,

I disagree that it's a problem with the definition, it's a problem with the programmer.

[diabolo-dan]

please do explain yourself.

I guess you missed the earlier part of the post you're quoting:

This is listed as one of the two motivating example (the other is about runtime performance for tail recursion), but the behaviour seems correct to me: assuming ? as Any, then "upcasting" to Any and then "upcasting" to a different type seems perfectly reasonable. (if ? is object, then the example would require an explicit cast, which could skip the ? part entirely).

Technically, this is not an assumption of the proof, but it's presumably an outcome of the proof, so it proves by counterexample that there is an assumption I don't agree with.

[diabolo-dan]

speaking of misleading, you didn't link the referenced paper where you wrote "From the referenced paper https://arxiv.org/pdf/2010.14094.pdf for some context.", this is a different paper that happens to agree with what was referenced above.

My apologies, there was a paper referenced above, I couldn't find a link for it, so searched, and that paper came up. I see it was later linked, but didn't find that when I was trying to find the paper that was referenced.

I'll take a look. So I don't make the same mistake again, can you confirm that it's this one: https://www.irif.fr/~gc/papers/icfp17.pdf

[mikeshardmind]

I guess you missed the earlier part of the post you're quoting:

I didn't miss it, but it wasn't sensical for me to address it as it wasn't one of the assumptions of the proof.

Technically, this is not an assumption of the proof, but it's presumably an outcome of the proof, so it proves by counterexample that there is an assumption I don't agree with.

If you can't disagree with the assumptions but you disagree with the outcome, you need to show that the proof is incorrect or it is your model of thought which is wrong about the outcome.

My apologies, there was a paper referenced above, I couldn't find a link for it

This is one of the two papers referenced specifically, and the one that has a link in thread, as well as a machine-proof version of it that shows how these definitions interact with Python's types Paper: https://www.irif.fr/~gc/papers/icfp17.pdf

The other is Titled "Abstracting General Typing" and is a 2016 paper attributable to Garcia. I don't have a link to it on hand, and I'm on mobile right now.

[diabolo-dan]

The other is Titled "Abstracting General Typing" and is a 2016 paper attributable to Garcia. I don't have a link to it on hand, and I'm on mobile right now.

this one: https://www.cs.ubc.ca/~rxg/agt.pdf ?

[mikeshardmind]

@diabolo-dan yes, though the one linked in thread previously is the one which specific claims where made based on, that paper is referenced and built upon in the other.

All of that said, I think the part about "but this is proven correct" is only tangentially important right now. That can all be addressed in any formalization effort, The real issue here most relevant to what started all of this, is that mutable instance variables are not treated as invariant. This has a relevant open issue since 2017 linked above.

We can't compare directly to the decisions of other languages that don't have nominal subtyping (typescript) or that don't have the same concerns on mutability (Haskell) without addressing how things those languages don't have to consider interact.

[kmillikin]

I think there are some things not quite right here. (I only found out about this issue this morning).

A bottom type does participate in subtyping, by definition of what "bottom" means. It is a bottom type with respect to subtyping. What I intended to write in the draft spec was that Never was just such a static type.

An uninhabited type is one that, when intepreted as a set of values, is empty. In semantic subtyping where subtyping is subset inclusion, then an uninhabited type is a subtype of every type. (Trivially, every element of the empty set is an element of every other set.). Python's Never is an uninhabited static type (there are no values of type Never).

AGT ("abstracting gradual typing") represents ("concretizes") gradual types (possibly involving Any) as sets of static types. Any is the set of all static types. A static type (not involving Any) is concretized as the singleton set consisting of just that static type. So crucially, the bottom type Never is concretized as a singleton set containing the static type Never and this is definitely completely distinct from a gradual type that was concretized as an empty set (if such a thing existed).

This is definition 2 on page 9 in the paper (https://www.irif.fr/~gc/papers/icfp17.pdf). Notice that concretization here can not produce an empty set of static types. To my knowledge, nobody has worried about what would be the gradual type that would be concretized as an empty set of static types (the original AGT paper just says that abstracting such a set is undefined).

What I intended to write in the spec was that Never was most certainly a static type. If there were a hypothetical "fully statically typed" Python language, it would have Never as a static type (unlike Any). I was wishy washy about whether Never was a static subtype of Any, as an open question. (I think it could be, and I'm not aware of any problem with that.)