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

A summary of the paper and how gen uses 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.

How gen uses this

gen-bind

gen-bind is the main implementation site.

Signatures as lightweight linksets (Section 5, Definition 5-1). buildSignature computes { requires, bound, unsatisfied, declaredMergeStrategies } for a wrapped module.

• bound corresponds to exp(L), the names this fragment provides (the injected bindings).
• requires corresponds to imp(L), the names still needed (formal arguments not satisfied by bindings, expected from evalModules).
• unsatisfied corresponds to fragments missing from the linkset: arguments in the declared vocabulary that were neither injected nor optional.

wrap is the analogue of compilation. It takes a module and returns it with explicit import and export metadata (the signature). buildSignature can run without wrapping, which is interface extraction without compilation.

Identity wrapping as fragment naming (Sections 5, 6). wrapIdentity stamps a stable key of the form "${class}@${identity}" onto a wrapped module. This is Cardelli’s fragment naming: each fragment in a linkset has a unique label that determines how it connects to other fragments. evalModules uses key for deduplication, so two modules with the same key are included once. This parallels Cardelli’s requirement that export names in a linkset are distinct (Definition 5-2). When the same module is reached along several scope-graph paths, identity wrapping makes it appear once in the final evalModules call.

Layered composition as linkset merge (Section 5, Definition 5-7). compose and composeWith merge binding layers across their fields (bindings, provenance, contracts, merge strategies). Each layer provides some names and may still need others, as two linksets reduce each other’s external interfaces. Later layers shadow earlier ones, which matches Cardelli’s left-biased environment merge E1 + E2 = E1, (E2 \ dom(E1)).

The argument environment as a linkset. adaptArgs and crossEval treat the argument environment a module resolves its free names against (_module.args and specialArgs) as the linkset. adaptArgs extends it where a slice of configuration enters evalModules. crossEval evaluates an opaque fragment separately against a sub-linkset and lifts its resolved config, which is Cardelli’s separate compilation.

Crossings and the fleet linkset. bind.crossing models each import of a value across an evaluation boundary as a node, and mkLinkset builds the fleet’s linkset over those crossings. Its coherence condition is a containment: the set of target identities a unit’s crossings reach, minus the unit itself, must lie within the linkset’s members. A unit whose set is empty is linked and can be evaluated alone. The two disjointness clauses of Definition 5-2 (imp(L) ∩ exp(L) = ∅) and Definition 5-7’s precondition (exp(L) ∩ exp(L') = ∅) are enforced when crossings are declared and merged. Theorem 7-6 is not claimed, because its hypotheses are F1 typing derivations this setting cannot supply.

gen-schema

emitModule translates record-algebra records into NixOS modules, a one-way step from a typed internal representation to an external module format. It is informed by Cardelli’s compilation function [[E |- d : S]], which translates binding judgments into linksets. gen-schema does not implement the linking calculus: it has no merge on emitted modules, no inter-checking between separately emitted modules and no linking by substitution. emitModule strips refinement metadata from types, so source-level typing is simplified for the target after type safety has been established, as in Cardelli’s compilation.

Acyclicity

Cardelli excludes cyclic dependencies: his Link algorithm fails on a cycle without diverging. gen’s staged minting has the same property for crossings. A crossing relates only nodes minted in strictly earlier passes, so a cycle among them cannot be written, and a crossing whose binding is itself the output of another crossing takes two passes. gen-scope evaluates circular attributes by fixpoint iteration (Sloane 2010), a separate mechanism from linking.

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) and notes that subtyping should refine it. gen-bind matches by name through builtins.functionArgs: a module declares an argument or it does not. A binding that provides { name, addr, role } to a module that needs { name, addr } is covered by the module system’s ... pattern, and gen-bind’s contracts could check this structural subtyping on binding values.

Explicit substitutions (Section 9, citing Abadi et al. 1990). Linking by substitution copies the provider’s term into each consumer. In Nix this appears as per-module closures when one binding is injected into many modules. wrapAll shares contract computation, and wrapping still creates a closure per module. Keeping a reference to the binding, as explicit substitution does, could reduce memory use for large fleets.

Dynamic linking (Section 9). Late-bound values, known only when a particular scope is evaluated, correspond to dynamic linking. gen-bind’s mkThunk (deferred, config-dependent values) is a step in this direction. A full model would link modules at different evaluation stages and preserve type safety across stages.

The inference system for build processes (Section 8). The five rules for validating compilation and linking sequences are not implemented in gen. They could verify that a sequence of operations (wrap aspects, merge binding layers, link into evalModules) preserves type safety at each step.

Potential New Libraries or Features

A linking step for module lists. A linkset algebra over NixOS modules: build linksets from wrapped modules, merge them with compatibility checks, resolve dependencies in topological order and inter-check types across module boundaries before evalModules runs. The core algorithm is iterative substitution. The NixOS module merge is a fixpoint, which needs care to reconcile with substitution. It would consume gen-bind signatures as fragments.

Signature compatibility. A compatible predicate over two buildSignature results, implementing Definition 7-4, would check whether two fragments’ binding requirements are mutually satisfiable before evalModules runs.

Structural subtyping for binding contracts. gen-bind’s contract.hasFields checks that a value carries given fields. A subtypeOf contract taking a reference signature would generalise it, and would compose with gen-schema’s refinement types for nested validation.

Research Directions

Linking semantics for module merge. Cardelli’s linking is substitution-based, and evalModules merges by fixpoint (mkMerge, option priority, deferred modules). Under what conditions does the fixpoint merge of separately compiled modules keep the properties Cardelli proves for substitution (subject reduction, confluence)? Modules reach evalModules from different scope paths, so the answer bears on whether merge behaviour is predictable.

Incremental relinking. Cardelli’s Day 6-7 scenario, library evolution and relinking, is fleet management: when one aspect changes, which hosts need reconfiguration? Compatibility and linking compatibility suggest that when an aspect’s signature is unchanged, downstream modules need not be relinked. gen-bind’s linked predicate already licenses evaluating and caching a unit alone, which is a starting point.

Mutual recursion through fixpoints. Cardelli defers mutual recursion (Section 2.2): “the circumstances under which cyclic dependencies are acceptable depend strongly on specific languages”. Lazy evaluation makes some mutual references safe in Nix, such as two modules reading each other’s config through the evalModules fixpoint. Characterising which cyclic linking patterns are safe in a lazy language would extend the theory to module patterns that staged minting excludes.