Lessons from Pyre that Shaped Pyrefly

Overview

Pyrefly is Facebook's next-generation Python type checker and language server, successor to Pyre. This article shares key lessons from Pyre's development that influenced Pyrefly's design.

Key Lessons

1. Language-Server-First Architecture

Pyre was originally designed as a CLI tool prioritizing throughput (parallel CPU usage). Adapting it for IDE use caused problems:

• Excessive machine resource consumption
• Editor interface freezes during computations
• High latency unacceptable for interactive use

Solution: Pyrefly built for flexibility from the start, plus uses Ruff parser for better error recovery during parsing.

2. OCaml vs Rust: Ecosystem as a Ceiling

Pyre was implemented in OCaml. While it bootstrapped quickly, limitations emerged:

• IPC model forced data into string-to-string hashtables
• Heavy serialization/deserialization overhead
• OCaml struggled with Windows support historically

Solution: Rust treats Windows, macOS, and Linux as true equals. Cross-platform reliability is foundational. Also enabled faster community growth.

3. Irreversible AST Lowering

Pyre used AST transformation passes to accelerate development (e.g., lowering Union[X,Y] to X | Y). However, this caused problems:

# Original code
from foo import x
def test():
    y = x
    x = "bar"
    z = x

# Transformed (lost critical info)
from foo import x
def test():
    y = foo.x  # lost: test() never references module foo!
    _local_test_x = "bar"
    z = _local_test_x

Solution: Pyrefly minimizes AST fabrication/transformation to preserve source location info for language server features.

4. Attribute Narrowing: Soundness vs Usability

Pyre's strict security focus led to strict type narrowing rules:

# Pyre complained even after isinstance check
class C:
    x: int | str = ...

def narrowing_test(c: C) -> int:
    if isinstance(c.x, int):
        some_other_function(c)
        return c.x  # Pyre: might still be str!

Users had to manually assign to local variables. Solution: Pyrefly allows this narrowing, prioritizing usability over strict soundness.

Significance

This article provides rare insight into how major tech companies evolve their developer tools. The lessons about language server architecture, ecosystem limitations, and usability tradeoffs are applicable beyond Python type checking.

Original Article