1 of 17

Pyrefly

a Python typechecker

​

pyrefly.org

​

2 of 17

Why Pyrefly?

Meta’s type checker Pyre did not meet all our needs

  • Slow for IDE use cases
  • Bugs in the language logic
  • Challenges using OCaml

Existing type checkers might not meet our needs

  • Deep integration with buck2 builds
  • Fast CI and IDE on very large codebases (>10K modules to analyze)
  • Support for downstream tools (Pysa, Glean, etc)

3 of 17

Why Pyrefly?

Our goals for the project

  • Fast for both bulk type checking and for use in an IDE
  • Correctness, conformance, good type inference tradeoffs
  • Support for downstream tools

Written in Rust

  • Good single-threaded speed, good support for parallelism
  • Built using the Ruff AST
  • Incrementality through a custom library (rather than salsa or dice)

4 of 17

A Couple New Ideas

The Pyrefly sandbox includes a Python interpreter

  • Easily cross-referencing static vs runtime behavior

​

Attribute access uses an API designed around the descriptor API

  • First look up the base, then model get vs set actions
    • General descriptor access is easy to support
    • Built-in descriptors (method, classmethod) fit nicely
    • Tricky edge cases (e.g. narrowing descriptors) are obvious

5 of 17

Multi-Pass Architecture

Pyrefly has three phases:

  • Definitions phase finds names defined per-module
  • Binding phase turns control flow into a table of “bindings”
  • Solving phase calculates binding results, handles types and expressions

​

Each phase is about 10x more expensive than the previous one

  • The first two phases are embarrassingly parallel
  • The last runs as parallel as possible

6 of 17

Multi-Pass Architecture

The Binding phase produces a table of Bindings, forming a graph of computations of various kinds (most of them resolve to a TypeInfo, which is a Type with possible attribute narrows).

​

I like to think of this in two ways:

  • A graph of deferred calculations, or “lazy types”
  • An IR that flattens control flow in statements

7 of 17

Binding Example

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

​

​

8 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

​

9 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

10 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

​

​

11 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

​

12 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

Def(y@line3) => Expr(x)

​

13 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

Def(y@line3) => Expr(x)

Def(y@line5) => Expr(“y”)

​

14 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

Def(y@line3) => Expr(x)

Def(y@line5) => Expr(“y”)

Phi(y@line6) => Phi(Def(y@line3), Def(y@line5))

15 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

​

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

Def(y@line3) => Expr(x)

Def(y@line5) => Expr(“y”)

Phi(y@line6) => Phi(Def(y@line3), Def(y@line5))

Use(y@line7) => Forward(Phi(y@line6))

​

16 of 17

Binding Example

​

​

1: x = f()

2: if isinstance(x, int):

3: y = x

4: else:

5: y = “y”

6: #

7: y

​

Use(f@line1) => Forward(...)

Def(x@line1) => Expr(x, f())

Use(x@line2) => Forward(Def(x@line1))

Use(int@line2) => Forward(...)

N(x@line2, line3) => N(Use(x@line2), IsInstance(int))

N(x@line2, line4) => N(Use(x@line2), NotInstance(int))

Use(x@line3) => Forward(N(x@line2, line3))

Def(y@line3) => Expr(x)

Def(y@line5) => Expr(“y”)

Phi(y@line6) => Phi(Def(y@line3), Def(y@line5))

Use(y@line7) => Forward(Phi(y@line6))

17 of 17

Pyrefly.org

​

Open Space Tomorrow:�321 4-5pm

​

​