Van Antwerpen et al. (2016) — A Constraint Language for Static Semantic Analysis Based on Scope Graphs

The paper

H. van Antwerpen, P. Néron, A. Tolmach, E. Visser, and G. Wachsmuth, “A constraint language for static semantic analysis based on scope graphs,” PEPM’16: Workshop on Partial Evaluation and Program Manipulation, pp. 49–60, 2016.

doi:10.1145/2847538.2847543 · read the paper

A summary of the paper and how gen uses it.

Paper Summary

Van Antwerpen, Neron, Tolmach, Visser, and Wachsmuth address a fundamental tension in language tooling: name resolution and type checking are conceptually separate concerns but practically interdependent. In languages with record field projection (r.x) or module imports, resolving a name requires knowing a type, which itself requires resolving other names. The paper’s contribution is a constraint language that unifies name binding and typing into a single declarative framework built on the scope graph formalism of Neron et al. (2015).

The architecture follows a clean two-phase design (Fig. 1): a language-specific extractor produces constraints from the AST, and a language-independent solver resolves them. Three constraint categories partition the problem: scope graph constraints (CG) define binding structure, resolution constraints (CRes) express name resolution requirements and uniqueness/completeness properties, and typing constraints (CTy) express type consistency via term equality and type assignment.

The key technical innovation is support for incomplete scope graphs — scope graph constraints may contain variables (particularly scope variables as targets of direct edges), allowing the solver to incrementally resolve constraints even when the full graph structure is not yet known. This is critical for type-dependent name resolution: when resolving e.x, the scope to search for x depends on the type of e, which may not yet be determined. The paper models this with scope variables (varsigma) that act as placeholders in import edges, resolved as type information becomes available.

The resolution calculus (Section 3.3, Fig. 9) extends Neron 2015 with two significant generalizations. First, edge labels are generalized beyond the fixed P (parent) and I (import) labels, with a parameterizable label set L. Second, the well-formedness predicate WF and visibility ordering < are now parameters rather than fixed: WF is defined by a regular expression E over label sequences (tested via Brzozowski derivatives), and < defines a lexicographic ordering on paths. Section 3.4 and Figure 10 demonstrate several instantiations: lexical scope alone (P*, D < P), non-transitive imports (P*.I?, D < P, D < I, I < P), transitive imports (P*.TI*, D < P, D < TI, TI < P), and combinations thereof.

The resolution algorithm (Section 4, Fig. 11) operates on incomplete scope graphs, returning either a set of declarations or U (unknown) when insufficient information exists. Environment functions return pairs of (result flag, declarations) where the flag is T (total — all visible declarations computed) or P (partial — scope variables still unresolved). The constraint solver (Fig. 12) is a non-deterministic rewrite system over tuples (C, G, psi), applying six rules: S-RESOLVE (name resolution via the algorithm), S-ASSOC (scope association lookup), S-EQUAL (unification), S-UNIQUE (uniqueness checking), S-SUBNAME (name collection subset), and S-TYPEOF (type assignment).

The paper proves three formal results. Lemma 1 establishes soundness and completeness of the resolution algorithm on ground scope graphs. Lemma 2 extends soundness to incomplete scope graphs: any resolution returned on an incomplete graph is valid in all ground instances. The stability property (G down-arrow o) ensures that if a resolution is found, it is the same across all ground completions. Lemma 4 proves the constraint solver sound: any solution it produces satisfies the constraint semantics. Completeness of the solver is explicitly left as future work.

The model language LMR (Language with Modules and Records) demonstrates the framework’s expressiveness across declarations, lexical scoping, module imports (transitive and non-transitive), associated scopes, record field declarations, field access with type-dependent name resolution, record initialization completeness checking, and Pascal-style with expressions.

Key Concepts

• Constraint-based scope graph specification: Scope graphs are defined declaratively via constraints (CG) rather than constructed imperatively. The graph emerges from constraint satisfaction, enabling incomplete graphs during solving.

• Three-category constraint taxonomy: CG (scope graph structure), CRes (resolution and collection properties), CTy (typing) — cleanly separating concerns while allowing interdependence through shared variables.

• Incomplete scope graphs with scope variables: Direct edge constraints may target scope variables (S —l—> varsigma), enabling incremental resolution as type information fills in placeholders. The algorithm signals U (unknown) when resolution depends on unresolved variables.

• Parameterized resolution calculus: The well-formedness predicate (regular expression E over label sequences) and visibility ordering (< on labels) are parameters, not hardcoded. This enables the same calculus to express lexical scope, non-transitive imports, transitive imports, includes, and arbitrary combinations (Fig. 10).

• Brzozowski derivative for path well-formedness: The algorithm uses Brzozowski derivatives (l^{-1} re) to incrementally check whether a path prefix remains in the language of the well-formedness regular expression, avoiding repeated full-path checks.

• Shadowing operator on declaration sets: The operator D1 triangle-right D2 keeps declarations from D1, plus declarations from D2 whose name does not appear in D1. Extended to pairs with result flags for the incomplete case.

• Stability on incomplete graphs: A resolution on an incomplete graph G is stable (G down-arrow o) when all ground instances yield the same resolution set. The algorithm guarantees stability for any resolution it returns (Lemma 2).

• Name collections with uniqueness and completeness: D(S) (declarations in scope), R(S) (references in scope), V(S) (visible declarations from scope). Constraints !N (uniqueness) and N1 subset N2 (subset) express properties like “no duplicate field names” and “all record fields initialized.”

• Type-dependent name resolution via association constraints: D —assoc—> S links a declaration to its associated scope. For field access, a chain of constraints connects the expression type to a declaration variable to an associated scope variable, threading name resolution through type resolution.

• Non-deterministic constraint solver: The solver (Fig. 12) branches when a reference resolves to multiple declarations, exploring all possibilities. Each branch maintains its own substitution state.

How gen uses this

gen-scope

gen-scope’s resolution is traversal-based (Neron 2015), not constraint-solving, so the paper’s core algorithm (Fig. 11) and solver (Fig. 12) are not implemented. Several of its patterns appear:

• Parameterized visibility policies (Section 3.4, Fig. 10): gen-scope’s query accepts localShadowsImport, importShadowsParent and transitiveImports, which correspond to instantiations of the paper’s label ordering and well-formedness regex. The default (D < I < P, transitiveImports = false) matches the paper’s “non-transitive imports” row. followEdge (from van Antwerpen 2018, prefigured here in the generalized label set L) follows custom edge labels beyond P and I.

• Well-formedness as a structural constraint: the _seen tracking in query (preventing import self-resolution) corresponds to the seen-imports set I in rule (N) and the seen-scopes set S in rule (T) of the resolution calculus. The paper formalizes what gen-scope implements operationally.

• Structural subtyping queries: subtypeOf checks that every declaration of scope A is also declared in scope B (with an optional per-key eq), the subset constraint N1 ⊆ N2 of Section 2.4. If one scope’s declarations are a subset of another’s, structural subtyping holds.

Further directions

Unexploited Ideas

Non-deterministic branching in resolution (Section 4.5, Fig. 12, S-RESOLVE): The solver branches when multiple declarations match. gen-scope’s query returns a single result (most specific), and queryAll returns all results, but there is no branching exploration of alternatives. For rules that need to reason about ambiguity (e.g., “if this reference is ambiguous, apply a tiebreaker”), a structured branching mechanism could be useful.

Uniqueness and completeness constraints (Section 2.1, 2.4): The !D(S) uniqueness constraint and V(S) approximately-equal R(S) completeness constraint have no direct gen-scope analogue. gen-scope can detect ambiguity via ambiguous, but cannot declaratively assert “no duplicate declarations in this scope” or “all expected references are present.” These would be useful for configuration validation.

Scope graph constraints as a specification language (Section 2, Fig. 6): The full constraint extraction framework — where an AST walk produces constraints rather than directly building a graph — is not implemented. gen-scope builds graphs directly via buildNodes and algebraic constructors. A constraint-based specification layer would make graph construction more declarative.

Brzozowski derivatives for path validation (Section 4, algorithm): The technique of using regular expression derivatives to incrementally validate resolution paths during traversal is not implemented. gen-scope’s query uses hardcoded path logic (local -> imports -> parent). A derivative-based approach would enable arbitrary path well-formedness policies without per-policy code.

Association constraints for type-scope bridging (Section 2.4): The D —assoc—> S mechanism for connecting declarations to associated scopes via type resolution is not directly used. gen-scope has followEdge for explicit custom edges, but not the type-driven dynamic edge discovery that association constraints enable.

Research Directions

Incremental constraint resolution: The paper notes incremental evaluation as an open problem (Section 5, “many applications for semantic analysis require efficient incremental computation”). In the Nix context, where evaluation is batch (not interactive), the question becomes: can Nix’s lazy evaluation be leveraged as a form of incremental computation, where only demanded constraints are solved? gen-scope’s _eval memoization already achieves this for attributes; extending it to constraint satisfaction would require tracking which constraints contributed to which resolutions.

Constraint-based configuration validation: The paper’s constraint framework could inform a declarative validation language for configurations. Rather than imperative assertions (“throw if X”), users would declare constraints (”!D(S) for scope S” meaning “no duplicate declarations”), and the framework would check satisfiability and produce targeted error messages. This aligns with the paper’s vision of constraint-based analysis producing partial solutions with residual unsolvable constraints translatable to error messages (Section 5, “Prototype Implementation”).

Completeness guarantees for scope graph resolution: The paper proves soundness but not completeness of the constraint solver. For gen, the analogous question is: does gen-scope’s traversal-based resolution find all resolutions that a constraint-based approach would? Since gen-scope implements the Neron 2015 calculus directly, and this paper proves the calculus sound and complete on ground graphs (Lemma 1), the answer is yes for fully-evaluated graphs. The open question is whether Nix’s lazy evaluation introduces incompleteness by not forcing all edges — a formal treatment would require characterizing which evaluations are “sufficiently forced” for resolution completeness.