Neil Mitchell: How Pyrefly Checks Python at Scale

Neil Mitchell, a programmer at Meta who previously worked on Buck2, introduces Pyrefly, an open-source Python type checker and language server. Python annotations can specify, for example, an integer parameter and a string return value, but the interpreter does not generally enforce them as static guarantees.

Once annotations exist, runtime tools can check values as the program executes, while static checkers examine code before execution. Python has several tools in both categories. Its type language has grown rich, with generics, literal types, narrowing, higher-order functions, and other features supported by a specification and conformance tests.

Pyrefly is written in Rust for speed, parallelism, and cross-platform support. The team previously built Pyre. A key goal for Pyrefly is inference: programmers provide useful hints, and the checker infers much of the rest so Python code can retain its ordinary style.

In a sandbox example, Pyrefly displays inferred types in the editor, infers a list's element type, reports a string passed where an integer is annotated, and supplies completion for a known string result. Mitchell notes that a type error can be stricter than a Python runtime error: the particular string argument in his example would actually run.

The scale motivating this work is substantial. Mitchell says Instagram's server contains over 20 million lines of Python and about 3,300 Meta developers work on Python on a given day. At this scale, type checking helps people change code without breaking unrelated behavior.

Meta started Pyre in 2017 after encountering scale and performance problems with the available checker, mypy. Pyre was written in OCaml and shared ideas with the company's previous work adding types to PHP and JavaScript. It became important to Meta's development workflow.

Mitchell says OCaml was not an ideal fit for Meta's environment at the time, citing Windows support, a difficult multiprocessing and shared-memory approach to parallelism, and barriers for outside contributors. He emphasizes that some issues reflected Meta's own investment choices and that OCaml was not the sole reason for Pyre's problems.

Pyre also had structural constraints: its abstract-interpreter design extensively desugared code, lacked a conventional symbol table and scope resolution, began as a command-line tool, and did not initially focus on open-source users. Retrofitting those facilities after adoption was difficult.

Two developers began prototyping a successor around August 2024, exploring constraint solving, more traditional subtyping approaches, and abstract interpretation. They chose Rust as a practical combination of speed, memory safety, portability, and growing adoption in the Python tooling community.

The prototype became a project in October 2024. The team chose the name Pyrefly after discovering a collision with an existing Python binding named pyre2. An alpha was released at PyCon; Mitchell describes the checker as still under development but ready to try.

Python's type system was grafted onto a huge amount of existing code, rather than designed alongside the language from the beginning. It keeps growing to describe previously untyped patterns. Types can catch problems in rarely exercised exception handlers and provide a useful check on generated code.

A standard and conformance tests provide common ground, but implementations still choose how much to infer. More inference can actually reject more programs, Mitchell observes, because a checker that infers less may approximate unknown information more broadly.

Python supports class types and literal types, such as a particular file-mode string or the integer 42. Annotations may be evaluated at runtime, and imports needed only for types can have a cost. Quoted annotations and explicit type-alias syntax address some complications, though older forms can make it hard to distinguish a value from a type alias.

The gradual type Any represents an unknown static type and is assignable in either direction. Mitchell points out that unions involving Any can behave less intuitively than simply collapsing everything to Any. Never and NoReturn describe unreachable or uninhabited results.

For unannotated variables, Pyrefly generally tries to infer something more informative than Any; unannotated function parameters, in the approach he describes, default to Any. Python generics support type variables, constraints, bounds, and variance, including newer syntax that can infer variance.

Protocols support structural subtyping: an object with the required close method can satisfy a closing protocol without explicitly inheriting from it. Overloads give different signatures for different inputs; the implementation must be compatible with those signatures, but the checker does not prove that each declared behavioral relationship is true.

Higher-order typing must handle Python's positional and keyword arguments. Parameter specifications can describe a generic bundle of those arguments. Flow-sensitive narrowing also refines types: after testing a string-or-None value for truth, a branch can treat it as a string.

Typing existing built-ins is another challenge. Typeshed supplies descriptions, but some runtime APIs do not fit a perfectly tidy type model. Mitchell mentions dictionary and mutable-mapping compatibility as an example where pragmatic treatment helps existing programs work.

Pyrefly's design goals include time and memory efficiency at Instagram scale, command-line and IDE support, integration with build systems, and a codebase open-source contributors can modify. Circular imports are a required case, not an exceptional one, because large Python codebases commonly contain them.

Drawing on his build-system experience, Mitchell chose file-level dependencies and invalidation. Finer granularity would add complexity, while a large codebase already has plenty of files. A keystroke invalidates a whole file, so rechecking that file must typically take only a few milliseconds; unused data must also be evicted.

A build-system layer manages dependencies, invalidation and concurrency while each file passes through six stages: code, AST, exports, bindings, answers, and interface. It obtains source from disk or an editor buffer and parses it using Ruff's error-correcting Python parser, which can return an AST even for incomplete code.

The exports stage determines what names each module provides, including names reached through star imports. Circular star imports can require a least fixed point. These results also establish dependencies between modules for the build graph.

The bindings stage turns statements into key-value relationships describing how to compute the type of each identified occurrence. It resolves sequencing, flow control and name uses before the later type calculations. A use can point to a definition or to an import in another module.

At a branch join, a phi operation combines the possible definitions, often as a union. A test such as isinstance supplies narrowing on a branch. The result is a compact intermediate language for Python type checking rather than repeated reasoning over the original control-flow structure.

An audience question raises the walrus assignment expression. Mitchell calls it a complication because it can define names inside expressions, but explains that the binding pass handles it by linearizing relevant boolean expressions and creating appropriate bindings. Loops and assignment expressions make this part of the implementation more intricate.

The answers stage evaluates the binding relationships and computes larger expression types from subexpression types. Cycles can arise in imports and return-type inference. Deferred computations, or thunks, and fresh variables help represent answers that are not yet known.

The interface retains the types of exported names, a smaller subset of the answers. To save memory, Pyrefly can discard ASTs, bindings, and answers after producing an interface, while retaining more information for files open in an IDE so navigation and other editor features work well.

Mitchell illustrates inference with lists. A list containing literal 1 is generally inferred as list[int], not list[Literal[1]], because mutable lists are invariant and a literal-only list could prevent later useful operations. A mixed list can be inferred with a union; contextual annotations can tell the checker to retain a literal type instead.

For an empty list followed by a generic add operation, Pyrefly starts with a fresh unknown element type. The generic function is instantiated with another fresh variable; constraints from the list and the value 1 connect the variables and determine an integer element type. The checker looks to the next use to constrain the list, otherwise falling back to Any.

Cross-module queries can use a compact interface once available or force an answer when a cycle means the interface has not yet been completed. Only exported answers are visible to other modules. This separation permits lazy computation during cycles without making private answers part of the interface.

Incremental checking with cycles is tricky: collapsing a large import cycle into one node could force tens of thousands of modules to be rechecked. If A changes, Pyrefly first checks it assuming B and C's old interfaces. If A's exported interface is unchanged, the other files need not be invalidated.

If the interface changes, the checker propagates to the affected modules and may revisit A. To avoid endless iteration, it falls back to invalidating the entire cycle after revisiting work or reaching a depth limit. The common case can be much faster, at the cost of occasional repeated work or less parallelism.

Mitchell describes exports, bindings, and answers as increasingly expensive stages, each roughly an order of magnitude more costly than the previous one in his profile. Threads and thread pools matter, but parallelism had not yet been the most important optimization. Transaction-like coordination allows editor queries and updates to proceed concurrently.

Instead of immediately offering an external plugin API for a rapidly evolving type system, Pyrefly incorporates extensions directly. Mitchell cites built-in Pydantic support, ongoing Django work, and native Buck integration; other build-system support was also being explored.

For recursion, the checker can place a thunk where a cycle may occur. If evaluation encounters the same computation again on its call stack, it inserts a fresh variable and later constrains that variable to the computed result. The approach does not solve every case, but the same variable mechanism is useful for generics, inference and recursion.

Pyrefly is MIT-licensed, accepts contributions, and has an issue tracker and Discord. Mitchell says the team deliberately prioritizes open-source users because the wider Python ecosystem benefits Meta too. At the time of the talk, he describes the project as alpha software with bugs and more than 100 contributors.

In questions, an audience member suggests retaining a bounded variable as the most general type for a list rather than immediately choosing list[int]. Mitchell agrees this might defer a choice between, for example, a union and a shared supertype until later use, and says the team could explore it; multiple inheritance complicates the lattice.

Another question probes whether using answers during a cyclic calculation conflicts with interface-based invalidation. Mitchell explains that cross-module queries can only access exported answers, and completed interfaces contain the same exported information. Deferred answers are needed while the interfaces are still being computed.

Asked about constraint solving, Mitchell says most constraints are subtype relationships, such as requiring an argument's type to be a subtype of a parameter's type. Unions make those relationships more complicated, and adding intersection types can make subset checks resemble satisfiability solving.

On compatibility, Mitchell describes work moving PyTorch from mypy to Pyrefly: a few hundred type ignores were added and a comparable number removed. He says the checkers are broadly comparable but may accept different programs, including cases Pyrefly flags that another checker misses. Large projects can require more migration effort.