A more useful and less divisive future for typing?

[mikeshardmind (Michael H)]

@BrenBarn

So. . . is there anything that Python needs to do here? What you said here sounds to me like “someone could write a different type checker and/or a different set of types (to be used in annotations) that would work better”. Is there some kind of support needed from the Python-language side that isn’t currently there?

Formalizing the parts of the type system that aren’t, explicitly choosing the set-theoretic model of subtyping (notably, this is entirely compatible with the current subtyping behavior that type checkers use, but is not specified, but there are other definitions which could be chosen that would have different outcomes), clarification on the definition of “Any” in python typing, as the ability to subclass it that was added recently isn’t well defined, and possibly either an explicit auto or Unknown if we don’t want the behavior of untyped code to change for existing type checkers, or something accepting that type checkers may rely on inference for more than they do. If auto/Unknown are wanted, this would make the kind of inference I’m describing opt-in, but still relatively easy.

@flyinghyrax

This future sounds like a much better correspondence between Python-the-language and Python-the-type-system. If I am understanding you correctly, intersection inference like this reflects Python’s actual runtime duck typing by identifying what attributes are actually used (the “quack”). So with no annotations at all, a verifier’s default behavior could be to check for compatible usage of these inferred protocols. It would be possible to only add annotations for API documentation (like giving a protocol a more meaningful name), to resolve ambiguity, or to restrict a type to something narrower than what is inferred.

This sounds excellent and makes me optimistic.

I’m optimistic that it’s possible and can describe a path that could get us to it, but I don’t think it’s an easy path, and it would require existing type-checker buy-in to not fragment the typing ecosystem. If more is “just detected” and some type-checkers aren’t buying into this, it’s going to lead to conflict between libraries that would prefer to use a type-checker that does this and the ones that would stick with the status quo. Maybe that’s okay long term and the ecosystem would self-resolve to what is more ergonomic and useful, but I don’t think it would be good for end users of the libraries on differing type-checkers in the short term without this actually being an intent to be supported by the type system.

Both of these points also feed into the desire for formalization that’s been expressed here, and for end-user stability in typing here, that is, even if this is something that would be a large improvement for most users, we can’t just up and do it either.