If we were to go back to the drawing board on this, rather than go for incremental improvement by adding specific rules that cover cases that don’t fit in neatly, what would the transition plan be for existing typing system users?
I’m not opposed to either this or adding rules that aren’t based directly from set-theoretic typing, but are still theoretically sound, but I feel like this is something I’ve personally proposed before (back when the specification effort started) and was told that it was insurmountable to “start over” on the type system, so I’d want to know what’s changed here that you’d consider it, as well as if a transition plan here opens the door to other fixes of things we know are suboptimal and with hindsight, and might have made other choices about (runtime checkable protocols, float meaning float or int, isinstance being defined in terms of intersections without accurately describing the intersection required, ABCs that aren’t generic over a default implementation (see contextmanager ABCs))
I am not looking for a change that would lead to major user-visible changes to how the type system works in practice, but instead for a theoretical framework that can be used to explain why things work the way they work and to reason about the correct behavior when that is not clear. I think the current “Type system concepts” page is useful in those regards. For example, I’ve found that the idea of “materialization” provides a useful intuition for the way gradual types work in the type system in practice.
But as I’ve found in this thread, the current framework has some limitations that mean it doesn’t describe the actual or desired behavior of type checkers well, so we may have to look for a new framework. Ideally, that framework should be mostly compatible with how type checkers behave in practice, though I’m open to minor changes in behavior where it makes sense. (For example, above I suggested to make Any not assignable to Never.) I think this approach makes sense for the typing spec because the spec should be somewhat conservative. Perhaps there’s some totally different approach to typing that would work better for Python, but if so, that approach should first be proven useful through an implementation in some type checker before it can make it into the typing spec.
Of course, all this is my personal opinion. There are many different type checkers for Python (and more under development). Most attempt to roughly follow the typing spec and the various typing PEPs, but they differ in many ways. And if someone reading this wants to build their own type checker on a different set of rules, nobody is stopping them.
Okay, thanks for that clarity, it actually sounded to me like you were looking at bottom-up redesigning the type system. I could see value in doing that, but it would need a lot of buy-in, and a real plan on what the goals to be solved would be that extends far beyond what I’ve seen appetite for. It’s an extreme enough option at this point that even though I personally believe in the potential value, I understand that it’s unlikely to have practical value without a large driving motivation beyond any expressed so far.
I believe most of the problems with never can be explained away while retaining the set-theoretic model if we incorporate the additional concept of functions and methods having a “safe applicative domain”. Elixir gets this in a way python cannot get with the same strength due to Elixir’s guard clauses being able to turn functions into strong-arrows, but it could be expressed without the same paired runtime guards on it with the approaches in treating exception paths (where Never arises in a code path) as separate from the return type of functions and methods.
The theory behind this is compatible with set-theoretic typing, and is the foundation for some of the tricker answers to intersection-related problems; I’ve been struggling with getting the terminology correct to be compatible with the current concepts, but not for lack of theory soundness, just for wanting more out of our current definitions.
I’ve been mostly convinced in my discussions with @mikeshardmind while working on another type system that the answer that best describes python is a set-theoretic framework, but not the set-theoretic framework that we have*, augmented with additional constraints and effects.
If you’re open to discussing this either in the context of python, that other type system, or in the abstract and using that discussion to further the progress of python’s type system, I’d be happy to work on this with more people, but I think it is too soon to take any of these ideas into python without exploring what it would mean for the future of the type system more.
* (how do you do footnotes since the discourse update?) We’ve discussed a set-theoretic framework, with additional universal constraints applied to the suitability of certain types based on the requirements imposed by the implementation of the language, and constraints that separate the return path from the exception path better.