This is a very interesting discussion, it’s useful to see everyone’s perspectives. Personally I’m in the group of people who don’t really use typing because it seems like too much trouble. I do have to read code that uses types, though, so it still winds up affecting me. I also answer Python questions in various chat rooms and forums and in the past few years I notice a trend of more and more questions that boil down to “I have some working code but how can I get the type checks to pass?” This is largely what gives me the perception that people are starting to take on additional labor that is wholly devoted to pleasing the type checker, and I don’t see that as a positive thing.
There’s one thought I keep having as I read through this thread: it seems to me that static typing as applied in Python is going to be fundamentally different from in a language that has had it from an early stage (even if it was optional). A big reason for this is that if the language was designed with static typing, then the language’s runtime type system (hopefully) was designed in tandem with the type checking. This means that things that there will usually be some commonality between things that are hard to specify correctly for type checking and things that are actually hard to do in the language.
But in Python, the type checking is grafted on to the actual types post hoc. There are all sorts of things that people want to do and do do in Python that have developed with nor regard for strict type correctness. This means there are many cases where it’s easy to get the code to work right but harder to get the type checker to realize it is right. And this results in all sorts of awkwardness, such as having parallel nomenclature (dict vs Dict, etc.).
None of that is news to anyone here (and it’s similar to some of what’s said in the typing explanation linked earlier). My gut feeling, though, is that this friction between the runtime type system and the static type system means that there is not going to be a way to please type theory purists without unacceptable levels of disruption to runtime behavior or code readability. We already see the trend in this direction:
I agree entirely, and in my view, things like this should be viewed as red flags telling us to halt and go no further in that direction.
I assume here you mean “harder for the tool/IDE”. But the irony is that it’s much easier to use an interpret the help() output — for a human. And, as you note, that’s precisely the problem. This kind of thing is making programming harder for humans in order to make it easier for IDEs, and I see that as a bad trade. More generally, I’d say there’s a lot of value in keeping Python the language “clean” enough for humans to be able to read and interact with Python code without an IDE being required. And as type annotations become longer and more elaborate, they reduce readability for humans looking directly at the source code (as opposed to hitting some IDE button to give them a summary of the arguments).
I agree with this. I might push it even a bit more: the point of adding features to Python should be to make Python better, not to align with some abstract external system like type theory. So I see arguments that originate as some form of “well, there’s this type theory notion…” as nonstarters.
From the perspective I just mentioned, the question becomes: “Okay, so why do we need anything that you would call a type-checker?” 
I tend to be leery of discussions of “soundness”. In my interactions with type theory fans, my impression has been that they tend to see soundness similarly to how you characterized it, in terms of guarantees. Or, in terms of false positives vs. false negatives, the approach coming from type theory is to minimize false negatives — in the ideal case, to ensure that if the code passes the type checker, a runtime type error is literally impossible.
I don’t think that that is a good road to go down for Python.[1] Like I said above, I see the benefit to users as of immeasurably greater importance than conformance with type theory. So from this perspective, the goal is not to minimize false negatives but to minimize false positives and get some useful level of true positives. That is, I don’t really care how many bugs the type checker doesn’t catch, I just care how many it does help me find, and I definitely care how much it makes me do extra work to get it to find a useful number of bugs.
This may be just another way of saying what you said above: you would consider such things to be just linters, rather than type checkers. Which is fine. But in that case what I’m saying amounts to a hypothesis that there is no possible “real” type checker for Python whose benefits outweigh its costs (e.g., in code readability).
That’s a reasonable position, but I have doubt about whether it’s feasible. The reason is that, as I see it, there is a certain minimum level of “easiness” that is acceptable. If we start from a position of type correctness, and then try to polish things up, even if things get easier and easier, there’s no guarantee they will ever get “easy enough” to justify the effort. And my suspicion is that they won’t.
It’s still possible to take the safety-first approach and work on smoothing out the pain points of a “correct” type system. But I don’t think that is anything that should be presented to the general public as “a good thing to do” until it actually reaches the point where it is easy enough to be a net win (which I don’t think it will).
This is exactly how I feel, and it kind of sums up my point about the friction between Python’s runtime and static type systems. As your example shows, the two systems, although tantalizingly close, always maddeningly remind us of how different they are. But I fear the gulf between the two systems cannot be bridged. The “right” level of annotation for a human reader is something like “list[int]”, but Python’s runtime behavior is too flexible to be adequately characterized by such hints. The result is that you either have to give “incorrect” type hints (which are useful as documentation but not for strict checking), or go the route of the SupportsDivMod example from above. I know which one I’d choose.
I share that sentiment to some extent. I don’t think I ever used 1.5.2; I can’t remember whether I started with 2.1 or 2.2. There have been many good developments since then. But I do have a sense that there have been diminishing returns with some of the changes over time, and the typing-related changes are perhaps the most prominent example. As a simple metric, by my count there are 24 typing PEPs in the accepted or finished states. I do wonder whether we really needed (or still need) that level of elaboration for an entirely optional language feature with no effect on runtime behavior.
I actually question whether it’s good road for any language, but that’s neither here nor there. ↩︎