typing
typing copied to clipboard
python
Issue with Never vs LSP
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
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.
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 aCallable[[], 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
@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.
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.
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>]"
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.
@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.
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.
~~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.
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.
NoReturnwas 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.
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.
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)
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.
(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
@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.
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.
@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
NoReturnandNeveras values, because this hides bugs. [1][2][3] - mypy already disallows using functions that return
Noneas 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
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.)
@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.
(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:
- 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.
- 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.)
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-conditionisinstance(return_value, R).However, when we try to substitute
NeverforRthere is a problem: the equivalence to a post-condition is no longer true, sinceNeveris supposed to be uninhabited (no instances of the type can exists). Therefore, the post-condition must fail. Indeed, the prior interpretation ofNeverasNoReturnmeans 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 eitherR==S==NeverorNever ≨ 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.
@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
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.
@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.
@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: https://gist.github.com/mniip/0bfb52f35da3ad6c96878082e6af37e6, but modified further.
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.
@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
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
undefinedto 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 undefinedIt 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.
@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.
I'm gonna start with a few things here.
- Never indicates a complete lack of a value, and is a type can't exist at runtime.
- 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
- All uses which would be "Broken" by fixing this already are broken and this would only highlight those issues.
- 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.
Neverindicates 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?