# How Pyrefly's Binding System Represents Definitions, Uses, and Phi Functions > Discover how Pyrefly's binding system represents definitions uses and phi functions using Key and Binding payloads for precise code analysis and type solving. - Repository: [Meta/pyrefly](https://github.com/facebook/pyrefly) - Tags: internals - Published: 2026-05-21 --- **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: ```rust /// I am defined in this module at this location. Definition(ShortIdentifier), ``` *Source:* [`pyrefly/lib/binding/binding.rs`](https://github.com/facebook/pyrefly/blob/main/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: ```rust pub struct NameAssign { pub name: Name, pub annotation: Option<(AnnotationStyle, Idx)>, pub expr: Box, // …other fields (first-use, receiver, …) } ``` *Source:* [`pyrefly/lib/binding/binding.rs`](https://github.com/facebook/pyrefly/blob/main/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`: ```rust /// I am a name in this module at this location, bound to the associated binding. BoundName(ShortIdentifier), ``` *Source:* [`pyrefly/lib/binding/binding.rs`](https://github.com/facebook/pyrefly/blob/main/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` 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`](https://github.com/facebook/pyrefly/blob/main/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`: ```rust /// I am the result of joining several branches. Phi(Box<(Name, TextRange)>), ``` *Source:* [`pyrefly/lib/binding/binding.rs`](https://github.com/facebook/pyrefly/blob/main/pyrefly/lib/binding/binding.rs) (lines 889–891) The corresponding binding implements the merge logic: ```rust /// A phi node, representing the union of several alternative keys. Phi(JoinStyle>, Box<[BranchInfo]>), /// A phi node for a name that was defined above a loop. LoopPhi(Idx, SmallSet>), ``` *Source:* [`pyrefly/lib/binding/binding.rs`](https://github.com/facebook/pyrefly/blob/main/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`](https://github.com/facebook/pyrefly/blob/main/pyrefly/lib/binding/scope.rs) to consolidate branch states: ```rust 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`](https://github.com/facebook/pyrefly/blob/main/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`](https://github.com/facebook/pyrefly/blob/main/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`](https://github.com/facebook/pyrefly/blob/main/pyrefly/lib/binding/scope.rs) creates these joins, while the solver in [`pyrefly/lib/alt/solve.rs`](https://github.com/facebook/pyrefly/blob/main/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`) and the set of values produced inside the loop (`SmallSet>`), 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`](https://github.com/facebook/pyrefly/blob/main/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.