A more useful and less divisive future for typing?

[mikeshardmind (Michael H)]

@BrenBarn

Perhaps I’m demonstrating my ignorance here, but my understanding is that typing as provided by Python (not mypy or other third-party tools) is essentially nothing but those two things: the typing stdlib module and documentation (in which I include standards such as those promulgated as PEPs). What I’m not understanding is where what you describe fits into that. Are you envisioning a PEP that says something like “we hereby adopt the set-theoretic model of subtyping”?

Specification (language level, currently just a collection of PEPs) describes the type system, type checkers (various) then choose what to do with them. There’s a bit more on how the standards haven’t actually spelled out everything that’s important or relevant to a type system, and good reasons to not have diverging behavior here, at least not largely diverging.

@BrenBarn

So would the same amount of effort be needed if your desiderata above were realized? Would the 640 person-hours of work you describe be in effect a “down payment” on the work required to bring the system to full fruition (as opposed to being “wasted” on a proof of concept that can’t be fleshed out into a full-featured tool)? That sounds like a good deal of work! And if that amount of work is required just for a proof of concept, it seems like the benefits of the changes would need to be quite large in order to make it worth it to implement the full system.

No, Anything I wrote here wouldn’t necessarily translate into the codebases of existing type-checkers.

@BrenBarn

Plus, personally, I think I’d be a little leery about a proposed change to Python itself at a stage where things are still 640 person-hours away from even being able to demonstrate the benefits. That sounds to me, again, like a case where the normal “put something on PyPI first” approach is more warranted — which is slow, but thereby allows things to proceed on a parallel track without impacting core Python functionality (or docs) until the gains are clearly established. Are there any existing Python typing tools that give us a glimpse of what you’re saying would be this better future?

Well, the changes I’d need are small and non-breaking, and only describe the type system, not runtime behavior. There’s no change to CPython needed, only to the specification of typing behavior. These changes are only to make one behavior specifically better defined, and specifically allow more from the type system.

1. Define subtyping for Python using the set-theoretic model. This model is 1:1 compatible with how type checkers currently treat subtyping but also covers cases the type system does not yet consider, such as Intersections. (Non-breaking, but gives a stronger foundation for future work)

2. State that type checkers are allowed (not required) to make complex type inferences based on consistency of usage even in untyped code and narrow Any based on observed use.

3. Type checkers may (not must) detect incompatible use of Any due to inconsistent use.

For people not using a type checker, nothing changes. For people using a type-checker, they may get more errors detected if the type-checker they use can suddenly detect more issues. It would be on type checkers to continue finding the balance spoken about with useful errors vs false positives spoken about above

Those are the only changes needed here for this, and I think that these two being specified is a good thing even if this never materialized fully. It’s one possible benefit from actually having definitions that are stronger and enable more.

Having an agreed-upon definition for subtyping is pretty important for a type system (we don’t have one of these currently)

The second one opens the door for type checkers to do more with untyped code for users without it violating if not the letter of specification, the original spirit that did not seem to envision there to be a good case to.

I think people overestimate what the required changes are for this, and it’s not even my primary goal in this discussion. It is to point out potential benefits we can gain over time by having better definitions and consistency in those definitions, and that stronger definitions do not inherently conflict with the other end of the spectrum on the usage of typing.