Cardelli (1997) — Program Fragments, Linking, and Modularization

The paper

L. Cardelli, “Program fragments, linking, and modularization,” the 24th ACM SIGPLAN-SIGACT symposium, pp. 266–277, 1997.

doi:10.1145/263699.263735

This page is our reading of it, not a substitute for it.

Paper Summary

Cardelli addresses a gap in programming language theory: while module mechanisms had received extensive formal treatment, the associated processes of separate compilation and linking remained largely unformalized. The paper observes that increasingly sophisticated module systems — particularly in functional and object-oriented languages — had drifted from the original purpose of modularization (separate compilation), producing systems where components could not be independently typechecked and compiled. The motivating example is a nine-day software development lifecycle (Days 1-9) that catalogs obstacles at each stage: interface publication, user program description, compilation, library compilation, linking, implementation evolution, relinking, interface evolution, and user adaptation. These obstacles span language design, implementation technology, and environment engineering.

The core contribution is a formal framework called linksets. A linkset is a collection of named typing judgments plus an external interface: E0 | x1 -> E1 |- t1 ... xn -> En |- tn. Each component xi -> Ei |- ti is a linkset fragment — a separately compiled unit with its own typing environment. The external interface E0 describes what the entire linkset still needs from outside. Fragment names (xi) match free variables of other fragments, determining how pieces connect. This naming-as-wiring strategy makes the linking topology explicit and checkable.

Cardelli builds the formalism over F1, a simply typed lambda-calculus, and defines a hierarchy of well-formedness predicates with increasing strength:

1. linkset(L) — names are coherent: environments use distinct variables, every assumption in a fragment’s environment is matched by a named fragment or declared in E0, and imports/exports are disjoint (Definition 5-2).
2. intra-checked(L) — each fragment is individually well-typed in F1, and all judgments share the common prefix E0 (Definition 5-3).
3. inter-checked(L) — fragment types agree across boundaries: if fragment k imports name xj with type A, then fragment j exports type Aj = A (Definition 5-4).

Linking is formalized as repeated substitution. A linking step L -> L' substitutes a fully-resolved fragment (one with empty environment) into another fragment’s free variable (Definition 6-1). The paper proves three central results about this process:

• Subject reduction for linking (Proposition 6-3): if inter-checked(L) and L ->* L', then inter-checked(L'). Linking preserves type safety.
• Confluence (Proposition 6-4): linking steps can be performed in any order; all reduction sequences converge to the same result. The proof uses a diamond argument on pairs of linking steps, extended to the reflexive-transitive closure by standard tiling.
• Algorithm Link (Algorithm 6-5, Proposition 6-6): a simple iterative algorithm that applies linking steps until no more are possible. Proved to terminate (environments strictly shrink), to be sound and complete with respect to linking reductions, and to preserve inter-checked on its output.

The paper then introduces a simple module system for F1 with import/export lists, signatures (tuple of declarations), and bindings (tuple of definitions). The compilation function [[E |- d : S]] translates binding judgments to linksets, and the two main theorems follow:

• Separate compilation (Theorem 7-3): a well-typed binding compiles to an inter-checked linkset.
• Separate compilation and merge (Theorem 7-6): two well-typed bindings with compatible interfaces compile to linksets whose merge is inter-checked.

Section 8 recasts these results as an inference system for reasoning about sequences of compilation and linking steps, showing that complex build pipelines (compile, partially link, merge with another compilation, link again) preserve type safety at every stage.

The paper explicitly excludes recursive/mutually-recursive modules (cyclic dependencies cause linking failure, not divergence) and notes future directions including alternative linking reductions, mutual dependencies via fixpoints, explicit substitutions to avoid code expansion, flexible signature matching with subtyping, and dynamic linking.

Key Concepts

• Program fragment: any syntactically well-formed term with free variables; a judgment E |- a : A represents a fragment compilable in isolation given environment E.
• Linkset: E0 | x1 -> E1 |- t1 ... xn -> En |- tn — a configuration language for collections of named fragments with a shared external interface. The “simple configuration language” of the paper.
• Fragment naming: each fragment’s label matches free variables of other fragments, creating an implicit needs/provides dependency graph. This is the linking topology.
• Three-level checking: linkset (name coherence) < intra-checked (per-fragment typing) < inter-checked (cross-fragment type agreement). Each level is preserved by its appropriate operations.
• Linking as substitution: a linking step replaces a free variable reference with the corresponding fragment’s term. Requires the provider fragment to have an empty environment (fully resolved).
• Linkset merge (L + L'): combines two linksets, reducing each other’s external interfaces by the fragments the other provides. Import environments are enriched; export environments are concatenated.
• Environment compatibility (E1 ~ E2): shared names must have identical types. Extended to linkset compatibility which also requires disjoint export sets.
• Confluence of linking: linking order does not matter — all paths reach the same normal form. Critical for build system correctness.
• Compilation function ([[_]]): translates module-level binding judgments into linksets, preserving typing properties. Compilation compatibility (Lemma 7-5) ensures compatible modules compile to compatible linksets.
• Inference system for build processes: Section 8’s five rules (Compilation, Compilation compatibility, Linking, Linking compatibility, Merge) form a reasoning framework for validating complex build sequences.

Implementation Mapping

Current Usage in Gen Ecosystem

gen-bind (Major)

gen-bind is the primary implementation site. Three features trace directly to Cardelli:

1. Signatures as lightweight linksets (Section 5, Definition 5-1)

signature.nix: buildSignature computes { requires, bound, unsatisfied, mergeStrategies } for each wrapped module. This is a direct analog of Cardelli’s linkset structure:

• bound corresponds to exp(L) — the names this fragment provides (bindings injected).
• requires corresponds to imp(L) — the names still needed (formal args not satisfied by bindings, expected from evalModules).
• unsatisfied corresponds to fragments missing from the linkset — args in the vocabulary but not injected and not optional.

The wrap function performs the analog of compilation: it takes a module (binding judgment) and produces a result with explicit import/export metadata (the signature). buildSignature can be called without performing wrapping, analogous to interface extraction without compilation.

2. Identity wrapping as fragment naming (Section 5, Section 6)

identity.nix: wrapIdentity stamps a stable key onto wrapped modules: "${class}@${identity}". This implements Cardelli’s fragment naming — each linkset fragment has a unique label (xi) that determines how it hooks into other fragments. In the NixOS module system, evalModules uses key for deduplication: two modules with the same key are merged once, not duplicated. This directly parallels Cardelli’s requirement that fragment names in a linkset are distinct (env(exports(L)) in Definition 5-2), and his observation that fragment identity determines the linking topology.

When the same module is reached via multiple scope graph paths in den, identity wrapping ensures it appears once in the final evalModules call — the same problem Cardelli’s fragment naming solves for compilation units reached via multiple dependency paths.

3. Layered composition as linkset merge (Section 5, Definition 5-7)

compose.nix: compose and composeWith merge binding layers. composeWith merges across all four binding fields (bindings, provenance, contracts, mergeStrategies) — each layer provides some names and may still need others. This parallels linkset merge where two linksets mutually reduce each other’s external interfaces. Later layers shadow earlier ones (// semantics), which corresponds to Cardelli’s left-biased environment merge (E1 + E2 = E1, (E2 \ dom(E1))).

gen-schema (Minor)

bridge.nix: emitModule translates record-algebra records into NixOS modules. This is a one-directional compilation step — from typed internal representation to external module format — informed by Cardelli’s compilation function ([[E |- d : S]]) that translates binding judgments to linksets. However, gen-schema does not implement the full linking calculus: there is no merge operation on emitted modules, no inter-checking between separately emitted modules, and no linking-as-substitution. The influence is architectural (the idea that typed internal records compile to external module fragments) rather than formal.

The emitModule function strips refinement metadata from types and extracts collections, producing a clean NixOS module. This corresponds to the information loss Cardelli notes in compilation — the source-level typing information is simplified for the target representation, with the type-safety guarantees established before compilation.

Relevance to Den v2 HOAG Pipeline

Den v2’s demand-driven HOAG (Higher-Order Attribute Grammar) over scope graphs creates a context where Cardelli’s linking model structures the boundary between scope-computed values and NixOS evalModules.

Fragment identity for scope-path dedup. In the HOAG pipeline, the same aspect can be reached via multiple scope graph paths (e.g., an aspect included by two different hosts that share a user). Each path computes attribute values independently, but the resulting NixOS module must appear once in the output. gen-bind’s wrapIdentity — implementing Cardelli’s fragment naming — stamps a key derived from the scope identity ("nixos@host=igloo") so that evalModules deduplicates. Without this, identical modules reached via different resolution paths would be duplicated, violating the expectation that linking produces a coherent whole.

Binding signatures as scope-boundary contracts. When scope-computed values cross from the gen world into NixOS evalModules — held today under a declared interim — the boundary is a wrap call. The signature (requires/bound) makes this boundary explicit and inspectable — the scope graph knows what it provided, and what evalModules must still supply. This is Cardelli’s separation of concerns: the fragment (wrapped module) is compiled (wrapped) with explicit knowledge of what it needs and what it provides, and the linker (evalModules) resolves the remaining dependencies.

Merge as scope-graph edge resolution. Den v2’s edge effect adds import edges between scope nodes. When aspects compose, their binding layers merge via composeWith. The scope graph’s resolution order (D < I < P specificity from Neron 2015) determines which bindings win — but the merge mechanics are Cardelli’s: two independently compiled units combine, mutually satisfying each other’s imports.

Acyclicity and the linking algorithm. Cardelli explicitly excludes cyclic dependencies — his Link algorithm fails (but does not diverge) on cycles. Den v2’s scope graph similarly requires acyclic resolution for class content: circular aspect dependencies are detected and rejected. The HOAG evaluator (gen-scope) handles circular attributes via fixpoint iteration (Sloane 2010), but circular linking — where module A needs module B’s output and vice versa — is structurally prevented, matching Cardelli’s design decision.

Appendix: Follow-up Work

Unexploited Ideas

Flexible signature matching and subtyping (Section 9). Cardelli’s inter-checked predicate requires exact type agreement (A = Aj in Definition 5-4). He notes this should be refined for subtyping. gen-bind currently uses exact name matching via builtins.functionArgs — a module either declares an arg or it doesn’t. There is no notion of a binding being “compatible but not identical” (e.g., a binding providing { name, addr, role } satisfying a module that only needs { name, addr }). The NixOS module system’s ... pattern partially addresses this, but gen-bind’s contract system could enforce structural subtyping on binding values.

Explicit substitutions to avoid code expansion (Section 9, citing Abadi et al. 1990). Cardelli notes that his linking-as-substitution causes code expansion — each linking step copies the provider fragment’s term into the consumer. In the Nix context, this manifests as duplicated module closures when the same binding is injected into many modules. gen-bind’s wrapAll partially addresses this by sharing contract computation, but the underlying wrapping still creates per-module closures. Explicit substitution — where a reference to the binding is maintained rather than a copy — could reduce memory pressure for large fleets.

Dynamic linking (Section 9). The paper mentions dynamic linking as future work. In den’s context, this corresponds to late-bound aspects — aspects whose binding values aren’t known until a specific scope context is evaluated. gen-bind’s mkThunk (config-dependent deferred values) is a step in this direction, but a full dynamic linking model would allow modules to be linked at different evaluation stages, with type safety preserved across stages.

The full inference system for build processes (Section 8). The five-rule inference system for validating compilation and linking sequences is not implemented anywhere in the gen ecosystem. It could serve as a formal verification framework for den’s pipeline: given a sequence of scope graph operations (compile aspects, merge binding layers, link into evalModules), verify that type safety is preserved at each step.

Potential New Libraries or Features

gen-link: A formal linking layer. A dedicated library implementing Cardelli’s linkset algebra over NixOS modules. Scope: linkset construction from wrapped modules, linkset merge with compatibility checking, a Link algorithm that resolves dependencies in topological order, and formal inter-checking that validates type compatibility across module boundaries before evalModules runs. This would sit between gen-bind (which handles individual module wrapping) and the consumer’s output assembly (which currently uses ad-hoc list concatenation). Complexity: moderate — the core algorithm is simple (iterative substitution), but adapting it to NixOS’s module merge semantics (which is not substitution-based but fixpoint-based) requires careful design. Interactions: consumes gen-bind signatures as linkset fragments, produces module lists for evalModules.

Signature compatibility checking on gen-bind. Extend buildSignature to support a compatible predicate between two signatures, implementing Cardelli’s Definition 7-4 (signature compatibility). This would allow den v2 to check at scope-graph construction time whether two aspects’ binding requirements are mutually satisfiable, catching configuration errors before evalModules evaluation. Scope: small — a pure function over two signature records. Interactions: feeds into gen-derive rules for early error detection.

Structural subtyping for binding contracts. Extend gen-bind’s contract system to support subtyping assertions — “this binding provides at least these fields” rather than exact field matching. This implements Cardelli’s Section 9 suggestion of flexible signature matching. Scope: small to moderate — contract.hasFields already does structural checking, but a contract.subtypeOf that takes a reference signature and checks structural compatibility would be more general. Interactions: composes with gen-schema’s refinement types for nested structural validation.

Research Directions

Linking semantics for NixOS module merge. Cardelli’s linking is substitution-based, but NixOS evalModules uses fixpoint-based module merge (lib.mkMerge, option priority, deferred modules). The formal relationship between these two models is unexplored. A key question: under what conditions does the fixpoint merge of separately compiled NixOS modules preserve the same properties (subject reduction, confluence) that Cardelli proves for substitution-based linking? This matters for den because scope-computed modules enter evalModules from different scope paths, and the merge behavior must be predictable.

Incremental linking for fleet-scale configuration. Cardelli’s Day 6-7 scenario (library evolution and relinking) maps directly to den’s fleet management: when one aspect changes, which hosts need reconfiguration? The paper’s compatibility and linking-compatibility properties suggest that if an aspect’s interface (signature) hasn’t changed, downstream modules need not be relinked. Formalizing this for scope graphs could enable incremental evaluation — only recompute scope subtrees whose input signatures changed.

Linking with mutual recursion via fixpoints. Cardelli explicitly defers mutual recursion (Section 2.2), noting that “the circumstances under which cyclic dependencies are acceptable depend strongly on specific languages.” In Nix, lazy evaluation makes certain mutual dependencies safe (e.g., two modules that reference each other’s config through the evalModules fixpoint). Characterizing which cyclic linking patterns are safe in a lazy language — and integrating this with Cardelli’s framework — would generalize the theory to cover real NixOS module patterns that the current acyclic restriction in den prohibits.