Growing pains for typing in Python

Python's static-typing feature has come a long way since it was introduced in 2014. Adding type information to functions has always been—and will remain—optional, but typing still remains somewhat contentious. There are multiple kinds of consumers of the information, each with their own needs and wishes, as well as users of the feature with expectations of their own. That has led to the formation of a Python typing council to govern the type system for the language, though, as might be guessed, there are still grumblings from various quarters.

Divisive

A long, recently rekindled, thread about typing and its future was kicked off back in September on the Python Discourse forum with a lengthy post from Michael Hall. He noted that the topic is "more than a little divisive in Python" because there are people pulling in different directions. There are some, like himself, who want the type system to be more strict, others who are concerned that the tools and community are making the feature less optional than advertised, and there are also discussions on putting extra non-type information into the type system. Part of the problem is that there is "no clear answer to the question 'Who is this for?'".

Hall suggested a series of steps, starting with formalizing the type system, making a reference document for it, and specifying what the type system's purpose and goals are. Jelle Zijlstra, who has been doing a lot of work on Python typing, replied that he would have a proposal soon "that will address some (though not all) of your points, creating a path towards a specification". He noted that Hall is focused on "soundness" for the type system, but that is not necessarily a goal—in fact, it may be difficult to achieve with the current tools:

You clearly care deeply about making the type system sound, but for many type checkers full soundness has not historically been a goal. And for type checkers like mypy and pyright that are used by numerous projects, any changes now can have backward compatibility considerations, so even if the maintainers of these type checkers agree with soundness as a goal (they may not!), it will take them a long time to get there.

What followed was some further discussion, also at length, about what was meant by "soundness"—rigor and consistency to a first approximation—which Hall thinks is essential, while others see it differently. Pyright developer Eric Traut noted that Python is a "big tent" programming language with diverse needs from its users and that the same is true for static typing in the language. In addition, the notions of type safety and soundness are not so black-and-white—there is a lot of gray. He thought that it would be difficult to find a single answer to the question of "purpose", but had a suggestion on how to approach it:

If we're going to attempt to codify the purpose of the type system, I suggest that do so in terms of user value. An answer like "the purpose of a type system is to allow a type checker to enforce type safety" is hard to evaluate because it begs the question "what exactly does that mean?" and "why should a user care?". If we frame the answer in terms of user value, I think it will help us find common ground.

David Foster, who is a contributor to Python typing, gave his thoughts on the question of the feature's targets, noting that long-lived, large, and collaborative projects are likely to benefit most. In his view, the goal should be to catch common error types and to provide "reliable machine-verified documentation that cannot get out of date"; that all should be driven by patterns in real-world Python programs. He agreed with Traut that soundness is not clear-cut, but also pointed out that he believes unsound typing is still useful.

Longtime Python developer Skip Montanaro is getting increasingly worried about what he sees going on with typing. It looks complex and the benefits marginal, he said, but typing is creeping in everywhere:

My understanding was that type annotations were always supposed to be optional. Technically, I suppose they still are. However, as tooling shifts to demand more and more metadata be specified through annotations or open source projects require type annotations in all submissions, I fear it has become optional in name only. I think at some point a fence will need to be built around type annotations to prevent them from infecting the entire ecosystem.

While there is no fence, there is typeshed, mypy maintainer Shantanu Jain said, which contains stubs for libraries that do not have their own type annotations; it should help reduce pressure on library developers coming from users who want them to add type information. Another problem is that it is difficult for developers to write annotations that work with all of the different type checkers that are available, as Foster, Hall, and others mentioned; type documentation that is type-checker-independent is largely non-existent.

Montanaro said that he is not only concerned about library authors being badgered about adding type information; the existing documentation mechanism, docstrings, is being ignored in favor of type information. "My understanding is that Visual Studio no longer uses that info, but relies only on type annotations when prompting for completions." Python packaging developer Paul Moore had an example of that:

As a user of VS Code, the autocompletion and informational pop-ups are often very nice. But they can be utterly terrible when type annotations are complicated. As an example, the popup for divmod says:

    (__x: SupportsDivMod[_T_contra@divmod, _T_co@divmod], \
     __y: _T_contra@divmod, /) -> _T_co@divmod

While that information may be easy to get (from type annotations) it's frankly worse than useless as actual documentation. In contrast, help(divmod) gives:

    divmod(x, y, /)
    Return the tuple (x//y, x%y). Invariant: div*y + mod == x.

I'm not entirely sure what conclusions to draw from this. But it very much feels like the pressure to "use type annotations" has resulted in a badly degraded user experience.

He agreed with Montanaro that a fence was needed, but thought it should be "a social one, rather than a technical one"; Moore would like to see it become more acceptable for libraries not to include type annotations and for the tools to treat that code as perfectly valid. In addition, as his example showed, annotations are not necessarily human-readable so tools should "promote non-typing solutions that are readable". To that end, Jain created a document with an "anti-pitch" for type annotations, which was eventually added to the typing repository (and documentation) as "Reasons to avoid static type checking".

In yet another lengthy message, Brendan Barnwell agreed with Moore and Montanaro about the path of typing in Python; the focus should be on user experience and not "making programming harder for humans in order to make it easier for IDEs". He concluded by noting that there are a large number of typing PEPs that have been accepted; "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."

After that, there was a fair amount of back-and-forth discussion, largely between Moore and Hall, on soundness, correctness, and what is possible (and not) within typing theory. Guido van Rossum popped in on the conversation late; once he mostly got up to speed, he observed that the goal of Hall's original post, as described in the subject ("A more useful and less divisive future for typing?"), may not be in the cards:

Going back to the subject line of this thread, it feels like whatever the benefits of a set-theoretic type system, "less divisive" does not appear particularly likely at this point. :(

Typing council

As that conversation was mostly winding down, Zijlstra announced the first draft of PEP 729 ("Typing governance process"), which proposes the formation of a typing council "that would help shepherd the Python type system by creating a conformance test suite and specification". It was co-authored by Jain and came out of a September discussion on typing governance that was proceeding in parallel with the thread started by Hall.

The PEP was favorably received in the thread and feedback was provided, some of which got reflected in the PEP. Zijlstra added the initial members to it at the end of October; it proposed a five-member council with Zijlstra, Van Rossum, Jain, Traut, and pytype maintainer Rebecca Chen. It was submitted to the steering council, which accepted it on November 20.

There have been lots of discussions in the Python typing forum of various aspects of typing from before and since the formation of the council. Beyond that, GitHub issues are being used to propose changes, which are being reflected in the specifications, conformance tests, and documentation in the typing repository.

User experience

Hall returned to the original thread in January with an "example of tools being placed above users". His argument was that the removal of a feature from PEP 646 ("Variadic Generics") was done because implementation would be difficult in the Pyre type checker, which might mean it would also be hard for others. To an outside observer, the description of the feature removed ("support for type variable tuples in `Union`") would seem to bolster the case about complexities in the type system that others (e.g. Moore) were pointing out; that description is not particularly clear to those not deeply immersed in the typing world. Hall said that there was evidence (from the mypy_primer regression tester) that projects had actually shown interest in using the feature.

Traut disagreed, saying that the PEP authors did not have a use case in mind for the feature when it was added; it does not make sense to add functionality without a use case. Beyond that, implementation complexity is something that needs to be taken into account:

From the time that the first draft PEP 646 was presented for general review, it took almost three years for mypy to add support for it. Pyre still hasn't added full support, and pytype hasn't even started to add support for it. New type system features that are too complex to implement in type checkers do not help the community. If you are involved in drafting a typing PEP, please take that into consideration.

But Hall said that the use cases for the feature were apparent. While it is understandable that type-checker developers need to consider the implementation difficulty, that puts users in a bind. "Things go from being typed as Any or untyped because the type system can't handle it yet, to people rewriting perfectly good code when it turns into 'and it never will be supported'." Elizabeth King had a similar complaint:

You incrementally support more and that's supposed to be a good thing right? In reality, that doesn't work for specifications. You get ossification as implementations block each other on [compatibility]. How many things are in the typeshed with a comment about a specific type checker not handling something correctly? Special casing that turns into a bigger problem down the road. This becomes self-fulfilling if even one implementation does this if implementations are allowed to be a blocker for the specification of something that makes sense.

At some point if typing is going to keep up with demands from users, it needs to stop being implementations that dictate what the type system supports, and only a matter of if a type checker is compliant with a specification made to support real use.

Moore said that a missing piece is a commitment to "prioritise user experience over implementation convenience" as an explicit goal of the typing council. Zijlstra thought that a blanket statement about priorities was not reasonable, "because a spec that is never implemented cannot help users". Meanwhile, he believes that the process worked in this case, since there were "no known use cases at the time"; he suggested that now that there are use cases, anyone who wants to re-add that feature should "go through the process for updating the typing spec".

There is a clear disagreement about the question of use cases and when they were known—or should have been known—with regard to this feature. Hall strongly disagreed with Zijlstra; in fact, he thinks the lack of recognition of the need for the feature is the biggest part of the problem, in general, for typing. There is a chicken-and-egg problem of sorts with typing features: without support, things that need the feature are not given types, so there are no clear use cases. That calls for careful consideration:

The type system is being bolted onto the language, and the gradual nature means people need to look at not only the things they are making now, but how this may interact with other things and things that haven't been typable so far.

Tensions

That is where things were left, but the thread clearly highlights the tension within the typing community. There are various things contributing to that, but the crux of the matter was summed up in that first message: there are too many constituencies, pulling in too many different directions. There is an enormous amount of Python code out there in the world without a single type annotation—and that is not likely to change substantially, probably for a long time. Meanwhile, there is a loud and likely growing group of Python developers who believe that "all code must have typing information"—to the extent that there have been proposals that would make typing implicitly, or even explicitly, required. Those were quickly shot down, and always will be, given that PEP 484 ("Type Hints"), which is the starting point for Python typing clearly states:

It should also be emphasized that Python will remain a dynamically typed language, and the authors have no desire to ever make type hints mandatory, even by convention.

It is into this mini-maelstrom that the typing council steps; it has a big job ahead of it. Bolting on (or, more politely, gradually adopting) a typing system was always going to be difficult, but the existence of the current set of tools may actually be making it harder. Those type checkers and integrated development environments (IDEs) have to ensure that they continue to function and to report the same kinds of problems and results, even as the specification changes out from under them. Choices made nearly ten years ago may not have aged well, but those tools are somewhat stuck at this point. Whether the council can help cut through this Gordian Knot remains to be seen.

The discussion highlighted another thing that is something of a hallmark of the Python world: cordiality even in the face of strong disagreement. Though public conversations have generally improved over the last decade or so, one does not have to look too far to find rancor and flames on the internet. But Python conversations are almost always collegial—and have been for decades. For example, several took the opportunity of the thread to thank the typing developers and to recognize that the feature does have uses (and users), even if they were not particularly inclined toward using typing themselves. It all helps reinforce Brett Cannon's adage that he came for the language, but stayed for the community. It also bodes well for finding reasonable solutions and compromises for typing—and more.