🥇The Road to Type Checking 4 Million Lines of Python Code. Part 1

Today we present to you the first part of the translation of the material on how type checking of Python code is handled at Dropbox.

A lot of writing at Dropbox is done in Python. This is a language we use extensively—for both backend services and desktop client applications. We also utilize Go, TypeScript, and Rust in large volumes, but Python remains our primary language. Considering our scale, with millions of lines of Python code, it became clear that dynamic typing unnecessarily complicated understanding and began to seriously impact productivity. To alleviate this problem, we started gradually converting our code to use static type checking with mypy. This is probably the most popular standalone type checker for Python. Mypy is an open-source project, with its main developers working at Dropbox.

Dropbox turned out to be one of the first companies to implement static type checking in Python code on such a scale. Nowadays, mypy is used in thousands of projects. This tool has been tried and tested countless times in real-world scenarios. To get to where we are today, we have had to travel a long road filled with many unsuccessful attempts and failed experiments. This material narrates the history of static type checking in Python—from its challenging beginnings, which were part of my scientific research project, to the present day, when type checks and type hints have become commonplace for countless developers writing in Python. These mechanisms are now supported by various tools such as IDEs and code analyzers.

→ Read the second part

Why is type checking needed?

If you've ever used Python, which is dynamically typed, you may be confused about the recent buzz surrounding static typing and mypy. Perhaps you even appreciate Python precisely because of its dynamic typing, and all of this is simply frustrating. The key to the value of static typing lies in project scale: the larger your project, the more you lean towards static typing, and ultimately, the more you genuinely need it.

Imagine a project has grown to tens of thousands of lines of code, and several developers are working on it. Based on our experience, understanding the code will be crucial in maintaining developer productivity. Without type annotations, it can be challenging to discern, for example, what arguments to pass to a function, or what types of values a particular function might return. Here are typical questions that are often difficult to answer without type annotations:

Can this function return None?
What type should this argument be items?
What is the type of the attribute id: int is it str, or maybe some custom type?
Should this argument be a list? Can a tuple be passed to it?

If we look at the following code snippet with type annotations and attempt to answer such questions, it turns out to be a straightforward task:

class Resource:
    id: bytes
    ...
    def read_metadata(self, 
                      items: Sequence[str]) -> Dict[str, MetadataItem]:
        ...

read_metadata does not return None, as the return type is not Optional[…].
Argument items — this is a sequence of strings. It cannot be iterated in arbitrary order.
The attribute id — this is a bytes string.

In an ideal world, one would expect that all such nuances would be described in the built-in documentation (docstring). However, experience provides numerous examples of the fact that such documentation is often absent in the code one has to work with. Even if such documentation is present in the code, one cannot rely on its absolute accuracy. This documentation may be unclear, inaccurate, leaving many opportunities for misinterpretation. In large teams or big projects, this issue can become particularly acute.

Although Python excels in the early or intermediate stages of projects, at a certain point, successful projects and companies using Python may face a crucial question: "Do we need to rewrite everything in a statically typed language?"

Type-checking systems like mypy address the aforementioned problem by providing developers with a formal language for describing types and by checking that type descriptions correspond to the program implementations (and, optionally, verifying their existence). Overall, one could say that these systems provide something akin to thoroughly validated documentation.

The use of such systems has other advantages that are already quite nontrivial:

The type-checking system can detect some minor (and not so minor) errors. A typical example is forgetting to handle a value None or some other exceptional condition.
Refactoring code becomes significantly easier, as the type-checking system often very accurately indicates which code needs to be changed. Additionally, we do not need to rely on 100% code coverage with tests, which is usually impractical anyway. We do not need to delve into the depths of stack trace reports to figure out the cause of a bug.
Even in large projects, mypy can often perform a full type check in mere seconds. Running tests usually takes tens of seconds or even minutes. The type-checking system provides instant feedback to the programmer, allowing them to work faster. They no longer need to write fragile and hard-to-maintain unit tests that replace real entities with mocks and patches just to get quicker results from code testing.

IDEs and editors, such as PyCharm or Visual Studio Code, leverage type annotation features to provide developers with code completion, error highlighting, and support for common language constructs. These are just some of the advantages that typing offers. For some programmers, this is the main argument in favor of typing. It brings immediate benefits right after implementation. This use of types does not require a separate type checking system like mypy, although it's worth noting that mypy helps maintain the consistency between type annotations and code.

The Background of mypy

The story of mypy began in the UK, in Cambridge, several years before I joined Dropbox. I was working on a PhD research project concerning the unification of statically typed and dynamically typed languages. I was inspired by an article on gradual typing by Jeremy Siek and Philip Wadler, as well as the Typed Racket project. I was trying to find ways to use the same programming language for various projects—from small scripts to codebases containing millions of lines. My goal was to avoid making too many compromises on projects of any scale. A key part of this was the idea of a gradual transition from an untyped project prototype to a fully tested, statically typed final product. These ideas are largely taken for granted today, but in 2010, it was a problem still being actively researched.

My initial work in type checking was not aimed at Python. Instead, I used a small 'homemade' language. AloreHere's an example that will help you understand what this is about (type annotations are optional here):

def Fib(n as Int) as Int
  if n <= 1
    return n
  else
    return Fib(n - 1) + Fib(n - 2)
  end
end

Using a simplified language of one's own design is a common approach in scientific research. This is largely because such an approach allows for quick experimentation, as well as the fact that anything unrelated to the research can be easily ignored. Real programming languages typically represent large-scale phenomena with complex implementations, which slows down experimentation. However, any results based on a simplified language can seem somewhat suspect, as in obtaining those results the researcher may have sacrificed considerations important for the practical use of languages.

My type checker for Alore looked quite promising, but I wanted to test it by running experiments on real code, of which there wasn’t much available in Alore. Fortunately, the Alore language was largely based on the same ideas as Python. It was fairly straightforward to adapt the type checker to work with Python's syntax and semantics. This allowed me to attempt type checking on open-source Python code. Additionally, I wrote a transpiler to convert code written in Alore to Python code and used it to translate the code of my type checker. Now I had a type checking system written in Python that supported a subset of Python, a kind of variant of this language! (Certain architectural decisions that made sense for Alore didn’t fit well with Python, which is still noticeable in some parts of the mypy codebase.)

In reality, the language supported by my type system at that moment couldn’t quite be called Python: it was a variant of Python due to some constraints of Python 3's type annotation syntax.

It looked like a mix of Java and Python:

int fib(int n):
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

One of my ideas at the time was to use type annotations to improve performance by compiling this variant of Python into C, or perhaps into JVM bytecode. I progressed to the stage of writing a compiler prototype, but I abandoned the venture as type checking itself seemed quite useful.

In the end, I presented my project at the PyCon 2013 conference in Santa Clara. I also discussed it with Guido van Rossum, the benevolent dictator for life of Python. He convinced me to abandon my own syntax and stick to the standard Python 3 syntax. Python 3 supports function annotations, allowing my example to be rewritten as shown below, resulting in a standard Python program:

def fib(n: int) -> int:
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

I had to make some compromises (first and foremost, I want to note that I invented my own syntax for this reason). In particular, Python 3.3, the latest version of the language at the time, did not support variable annotations. I discussed various formatting possibilities for such annotations with Guido via email. We decided to use comments with type hints for variables. This achieved the desired goal but looked somewhat clunky (Python 3.6 gave us a more pleasant syntax):

products = []  # type: List[str]  # Eww

Type comments also came in handy for supporting Python 2, which lacks built-in support for type annotations:

def fib(n):
    # type: (int) -> int
    if n <= 1:
        return n
    else:
        return fib(n - 1) + fib(n - 2)

It turned out that these (and other) compromises didn't really matter — the advantages of static typing led users to quickly forget about the not-quite-perfect syntax. Since no special syntactic constructs were employed in Python code where types were checked, existing Python tools and code processing methods continued to work normally, greatly easing developers' adaption to the new tool.

Guido also convinced me to join Dropbox after I defended my thesis. This is where the most interesting part of the mypy story begins.

To be continued…

Dear readers! If you use Python, we invite you to share what scale of projects you are developing in this language.

Source: habr.com