How Pyrefly's Binding System Represents Definitions, Uses, and Phi Functions

Pyrefly encodes definitions as Key::Definition paired with binding payloads like Binding::NameAssign, captures uses through Key::BoundName and specialized placeholders such as Key::UsageLink, and represents control-flow merges via Key::Phi paired with Binding::Phi or Binding::LoopPhi for the type solver to resolve.

Pyrefly, Facebook's Rust-based Python type checker, constructs a binding graph during AST traversal to track value flow through a program. This system represents every variable definition, use, and phi function—the join points of control-flow branches—as distinct Key and Binding entities that the type solver later resolves to concrete types. Understanding these representations is essential for navigating the Pyrefly codebase or analyzing its inference behavior.

Definitions: Key::Definition and Binding Payloads

Definitions in Pyrefly introduce named values into the scope and are represented by the Key::Definition variant linked to concrete binding implementations.

The Definition Key

When the binder encounters a name assignment, it creates a Key::Definition that uniquely identifies the source location:

/// I am defined in this module at this location.
Definition(ShortIdentifier),

Source: pyrefly/lib/binding/binding.rs (lines 859–866)

The ShortIdentifier records both the name and its precise TextRange in the source file, allowing the solver to map binding graph nodes back to concrete syntax.

Assignment Bindings

Variable assignments are stored as Binding::NameAssign structures containing the assignment context:

pub struct NameAssign {
    pub name: Name,
    pub annotation: Option<(AnnotationStyle, Idx<KeyAnnotation>)>,
    pub expr: Box<Expr>,
    // …other fields (first-use, receiver, …)
}

Source: pyrefly/lib/binding/binding.rs (lines 2053–2062)

This binding is linked to the Key::Definition via the scopes table maintained by BindingsBuilder. Beyond simple assignments, Pyrefly uses specialized variants such as Binding::Import, Binding::ClassDef, and Binding::FunctionDef to capture module imports and class or function declarations.

Tracking Variable Uses

Uses represent reads of defined names and require distinct key types depending on the complexity of the reference.

Standard Name Resolution

For direct reads of bound names, Pyrefly emits a Key::BoundName:

/// I am a name in this module at this location, bound to the associated binding.
BoundName(ShortIdentifier),

Source: pyrefly/lib/binding/binding.rs (lines 879–882)

When the resolver encounters a name read, it creates this key pointing back to the definition’s Idx<Key> through the bindings table, establishing the data dependency for the solver.

Specialized Use Placeholders

Pyrefly handles complex inference scenarios through specialized use keys:

• UsageLink(TextRange): Creates a placeholder allowing a later expression to pin the type of a partially-typed definition during first-use inference.
• YieldLink(TextRange) / YieldFromLink(TextRange): Provides links for the solver to connect the first use of a generator value back to its yield site.
• Delete(TextRange): Guarantees a key exists even when a variable is only deleted via del, ensuring the binding graph remains complete.

Sources: pyrefly/lib/binding/binding.rs (lines 891–894, 896–898, 904–907)

These correspond to Binding::UsageLink(LinkedKey) entries where LinkedKey points to the eventual definition key that will be resolved by the solver.

Phi Functions and Control-Flow Merging

Phi functions represent the union of values from different control-flow branches, implemented through dedicated key and binding pairs.

The Phi Key and Binding Structure

Control-flow joins are marked by Key::Phi:

/// I am the result of joining several branches.
Phi(Box<(Name, TextRange)>),

Source: pyrefly/lib/binding/binding.rs (lines 889–891)

The corresponding binding implements the merge logic:

/// A phi node, representing the union of several alternative keys.
Phi(JoinStyle<Idx<Key>>, Box<[BranchInfo]>),

/// A phi node for a name that was defined above a loop.
LoopPhi(Idx<Key>, SmallSet<Idx<Key>>),

Source: pyrefly/lib/binding/binding.rs (lines 276–283)

The JoinStyle parameter determines the type-union policy—such as Strict or Widen—while BranchInfo records each incoming branch’s value key and an optional termination key (the last StmtExpr in that branch, useful for detecting Never or NoReturn types).

LoopPhi for Carried Dependencies

Binding::LoopPhi handles the specific case where a name is defined before a loop but reassigned inside it. This captures the circular dependency between loop iterations where the variable's value depends on its previous iteration's value.

Creating Phi Nodes During Scope Merging

When the binder finishes processing a control-flow construct, it invokes merge_idxs in pyrefly/lib/binding/scope.rs to consolidate branch states:

if branch_idxs.len() == 1 {
    // no phi – just forward the single value
    self.insert_binding_idx(phi_idx, Binding::Forward(idx));
    idx
} else if let Some(loop_prior) = loop_prior {
    self.insert_binding_idx(phi_idx, Binding::LoopPhi(loop_prior, branch_idxs));
    phi_idx
} else {
    self.insert_binding_idx(
        phi_idx,
        Binding::Phi(join_style, branch_infos.into_boxed_slice()),
    );
    phi_idx
}

Source: pyrefly/lib/binding/scope.rs (lines 3220–3229)

The phi_idx generated by idx_for_promise(Key::Phi(...)) becomes the canonical key that downstream statements reference after the control-flow merge.

From Binding Graph to Type Resolution

The binding graph serves as the intermediate representation for Pyrefly's type solver (pyrefly/lib/alt/solve.rs). During the AST walk:

1. Assignments create Key::Definition nodes with Binding::NameAssign payloads.
2. Reads create Key::BoundName or specialized use keys pointing to their definitions.
3. Control-flow joins trigger merge_idxs to create Binding::Phi or Binding::LoopPhi nodes, with all subsequent reads resolving to the Key::Phi.

The solver traverses this graph, computing TypeInfo for each binding. For phi nodes, it joins the types of all incoming branches according to the specified JoinStyle, enabling precise type inference across complex control flow.

Summary

• Pyrefly uses Key as a type-erased identifier for source locations and Binding as the payload describing the operation.
• Definitions use Key::Definition paired with variants like Binding::NameAssign to capture assignment metadata including annotations and expressions.
• Uses are captured as Key::BoundName for direct reads or specialized keys like Key::UsageLink and Key::YieldLink for complex inference scenarios.
• Phi functions merge control-flow paths using Key::Phi and Binding::Phi, with LoopPhi handling variables defined before but assigned inside loops.
• The merge_idxs function in pyrefly/lib/binding/scope.rs creates these joins, while the solver in pyrefly/lib/alt/solve.rs resolves them to union types according to JoinStyle policies.

Frequently Asked Questions

What is the difference between Key and Binding in Pyrefly?

Key is a type-erased identifier that carries the source range of a definition, use, or phi node, while Binding is the concrete payload attached to that key describing what operation occurred. For example, Key::Definition identifies where a variable is defined, while Binding::NameAssign contains the actual assignment details like the expression and type annotation.

How does Pyrefly handle variable assignments inside loops?

Pyrefly uses Binding::LoopPhi specifically for variables defined before a loop but reassigned inside it. Unlike standard Binding::Phi, LoopPhi tracks the initial value before the loop (Idx<Key>) and the set of values produced inside the loop (SmallSet<Idx<Key>>), allowing the solver to compute the fixed-point type across iterations.

What is a UsageLink and when is it used?

Key::UsageLink and its corresponding Binding::UsageLink serve as placeholders for first-use inference scenarios. When a variable is partially typed or when its type depends on how it is first used in the program, this link creates a connection point that allows the solver to "pin" the definition's type based on the observed usage site rather than the declaration site.

How does the type solver resolve Phi functions to concrete types?

The solver in pyrefly/lib/alt/solve.rs traverses the binding graph and computes a TypeInfo for each Binding::Phi by joining the types of all incoming branches specified in the BranchInfo array. The JoinStyle parameter determines the union policy—such as strict union or type widening—ensuring sound type propagation across if-statements, loops, and other control-flow constructs.

{
  "mcpServers": {
    "instagit": {
      "command": "npx",
      "args": ["-y", "instagit@latest"]
    }
  }
}