ML Modules: Abstraction, Functors, and Sharing

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

The existential packages of chapter 10 can hide one representation. Reusing that chapter’s counter, for example, gives the interface $$\mathrm{\exists }t::\mathsf{Ty}.t\times ((t\to t)\times (t\to \mathbb{N})).$$ After unpacking, a client receives a fresh type name, an initial state, a step, and an observation. This is the right lexical account of one abstract value. It does not yet describe $$\begin{array}{l}\mathsf{structure}\mathsf{NatOrder}:\mathsf{ORDERED},\\ \mathsf{functor}\mathsf{SetFn}(X:\mathsf{ORDERED}):\mathsf{SET}\mathsf{sharing}\mathsf{type}\mathsf{elem}=X.s,\\ \mathsf{structure}\mathsf{NatSet}=\mathsf{SetFn}(\mathsf{NatOrder}).\end{array}$$ The sharing clause requires the result’s element type to be the very constructor selected by the argument’s component s, not merely a constructor of the same kind. An ML functor takes one statically classified module to another, and its result signature may mention the argument’s type component. A signature is a module’s static classifier; a module is the packaged implementation. The result interface must remember that its element type is the very type selected by the argument. Packing the argument and result independently creates unrelated existential witnesses. Unpacking the argument inside the functor body makes its witness lexical: the name cannot occur in the result type after that unpacking ends. Adding an equation outside the packages merely asserts the sharing that the encoding failed to transport.

The failure can be displayed before adding module signatures. If $O$ and $S$ are independently packed order and set implementations, the attempt does not type: its second component has type $\mathsf{Set}(u)$, not $\mathsf{Set}(t)$. Choosing witness $u$ makes the order component fail instead. The two lexical witnesses provide no equation between $t$ and $u$.

A projectible path is a module path whose static projections carry a stable type identity. Signature matching propagates that identity into later components before any dynamic code runs. In the reduced calculus, opaque sealing is generative and functor application is nonprojectible.

One reduced module calculus

The constructor and pure-term core is the $F_{\omega }$ calculus of chapter 9, restricted to $\mathsf{Ty}$, singleton kinds, arrows, products, and the pure terms appearing in module components. The only new constructor feature is a singleton kind $\mathsf{Sing}(c)$. A mixed context $\mathrm{\Gamma }$ contains constructor assumptions $u::\kappa$, expression assumptions $x:\tau$, and module assumptions $X:\sigma$. Its exact singleton delta is $$\frac{\mathrm{\Gamma }⊢c::\mathsf{Ty}}{\mathrm{\Gamma }⊢\mathsf{Sing}(c)\mathsf{kind}}\mathrm{Sing}-\mathrm{Kind},\frac{\mathrm{\Gamma }⊢c::\mathsf{Ty}}{\mathrm{\Gamma }⊢c::\mathsf{Sing}(c)}\mathrm{Sing}-\mathrm{I},$$ $$\frac{\mathrm{\Gamma }⊢c::\mathsf{Ty}}{\mathrm{\Gamma }⊢\mathsf{Sing}(c){⪯}_{\mathsf{k}}\mathsf{Ty}}\mathrm{Sing}-\mathrm{Sub},\frac{\mathrm{\Gamma }⊢d::\mathsf{Sing}(c)}{\mathrm{\Gamma }⊢d\equiv c::\mathsf{Ty}}\mathrm{Sing}-\mathrm{E}.$$ Thus $d::\mathsf{Sing}(c)$ entails $d\equiv c::\mathsf{Ty}$: a singleton kind records a static constructor equation. Subkinding is the least reflexive and transitive relation containing Sing-Sub and closed under kind equivalence; constructor kinding admits subsumption along it. Dynamic-type subtyping in this reduced calculus is conversion: exactly when $\mathrm{\Gamma }⊢{\tau }_1\equiv {\tau }_2\mathsf{type}$. Constructor equivalence and pure-term typing otherwise use the inherited $F_{\omega }$ rules, but Sing-E adds the directed conclusion $\mathrm{\Gamma }⊢d\equiv c::\mathsf{Ty}$ from $\mathrm{\Gamma }⊢d::\mathsf{Sing}(c)$. A singleton kind is therefore a static equation, not a runtime test.

The selected fragment uses an acyclic manifest environment. Read the context from left to right. A manifest atom is either a declaration $u::\mathsf{Sing}(c)$ or a projectible component $Q.s$ whose signature carries that singleton kind; its manifest equation is $u\mapsto c$ or $Q.s\mapsto c$. The right-hand side $c$ must be well kinded in the earlier context. Constructor variables and projectible static projections are the only atoms. Define ${\mathsf{expand}}_{\mathrm{\Gamma }}(d)$ by replacing each manifest atom by its earlier right-hand side, recursively, and then taking the inherited $F_{\omega }$ beta-eta normal form. The declaration index strictly decreases at every manifest replacement.

Algorithmic constructor conversion first synthesizes the inherited kind of both inputs, erasing $\mathsf{Sing}(c)$ to $\mathsf{Ty}$, and then compares ${\mathsf{expand}}_{\mathrm{\Gamma }}(d_1)$ and ${\mathsf{expand}}_{\mathrm{\Gamma }}(d_2)$ up to alpha-equivalence. Algorithmic subkinding accepts equal normalized kinds and the one strict shape $\mathsf{Sing}(c){⪯}_{\mathsf{k}}\mathsf{Ty}$. Checking $d$ at $\mathsf{Sing}(c)$ synthesizes $d::\mathsf{Ty}$ and applies the conversion test to $d$ and $c$; checking at any other kind uses inherited $F_{\omega }$ kinding.

Proof of Proposition 14.1 — Decision for the singleton constructor fragment

Proof. Manifest expansion terminates because every replacement decreases the declaration index. The inherited normalization and comparison terminate by the $F_{\omega }$ normalization and conversion result of corollary 7.26; the subkinding test is a finite shape comparison.

For soundness, induction on expansion replaces $q$ by $c$ using the singleton equation recorded when $q$ entered the context. Inherited beta-eta normalization preserves constructor equality, so equal normal forms give declarative conversion. The strict subkind case is Sing-Sub, and singleton checking ends with Sing-I followed by conversion.

For completeness, induct on a declarative derivation. The inherited cases are complete by the $F_{\omega }$ procedure. In the new Sing-E case, the manifest atom and its recorded right-hand side expand to the same normal form. Reflexivity, symmetry, and transitivity preserve equality of normal forms, and congruence follows because expansion is homomorphic before normalization. The only strict generated subkind is Sing-Sub. After equality steps are contracted, a subkinding derivation contains at most one strict step: no rule derives $\mathsf{Ty}{⪯}_{\mathsf{k}}\mathsf{Sing}(c)$. The finite test therefore covers every derivation. ◻

The formation rules state each dependency explicitly: the dynamic type $\tau$ in B-Sig is formed under its static component $u$, while the codomain signature ${\sigma }_2$ in Sigma-Sig and Pi-Sig is formed under the module path $X$: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\kappa \mathsf{kind}\\ \mathrm{\Gamma },u::\kappa ⊢\tau \mathsf{type}\end{array}}{\mathrm{\Gamma }⊢\mathsf{B}(u::\kappa ;\tau )\mathsf{sig}}\mathrm{B}-\mathrm{Sig},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1\mathsf{sig}\\ \mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\mathsf{sig}\end{array}}{\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\mathsf{sig}}\mathrm{Sigma}-\mathrm{Sig}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1\mathsf{sig}\\ \mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\mathsf{sig}\end{array}}{\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2\mathsf{sig}}\mathrm{Pi}-\mathrm{Sig}.$$ Signature equivalence contains alpha-equivalence and the inherited kind, constructor, and type equivalences. It is closed under the congruence rules below. In B-Eq, write $${\beta }_i:=\mathsf{B}(u::{\kappa }_i;{\tau }_i).$$ Its new congruence rules are $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\kappa }_1\equiv {\kappa }_2\mathsf{kind}\\ \mathrm{\Gamma },u::{\kappa }_1⊢{\tau }_1\equiv {\tau }_2\mathsf{type}\end{array}}{\mathrm{\Gamma }⊢{\beta }_1\equiv {\beta }_2\mathsf{sig}}\mathrm{B}-\mathrm{Eq},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1\equiv {\sigma }_1^{\prime }\mathsf{sig}\\ \mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\equiv {\sigma }_2^{\prime }\mathsf{sig}\end{array}}{\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\equiv \mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }\mathsf{sig}}\mathrm{Sigma}-\mathrm{Eq}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1\equiv {\sigma }_1^{\prime }\mathsf{sig}\\ \mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\equiv {\sigma }_2^{\prime }\mathsf{sig}\end{array}}{\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2\equiv \mathsf{Pi}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }\mathsf{sig}}\mathrm{Pi}-\mathrm{Eq}.$$

Surface records with several type and value fields are right-associated hierarchies of basic signatures. This convention is structural, not an equation identifying differently associated hierarchies.

The judgment $\mathrm{\Gamma }⊢M:\sigma$ is generated by the following module rules. Basic structures expose singleton kinds; sealing checks a match and exports only the sealed signature: $$\frac{X:\sigma \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢X:\sigma }\mathrm{Var},\frac{\begin{array}{c}\mathrm{\Gamma }⊢c::\kappa \\ \mathrm{\Gamma }⊢e:\tau [c/u]\end{array}}{\mathrm{\Gamma }⊢⟨c;e⟩:\mathsf{B}(u::\mathsf{Sing}(c);\tau )}\mathrm{Basic},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢M:{\sigma }_0\\ \mathcal{D}::\mathrm{\Gamma }⊢{\sigma }_0{⪯}_{\mathsf{s}}\sigma \end{array}}{\mathrm{\Gamma }⊢M\upharpoonright \sigma :\sigma }\mathrm{Seal}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢\sigma \mathsf{sig}\\ \mathrm{\Gamma }⊢M_1:{\sigma }_1\\ \mathrm{\Gamma },X:{\sigma }_1⊢M_2:\sigma \end{array}}{\mathrm{\Gamma }⊢(\mathsf{let}X=M_1\mathsf{in}{M}_2):\sigma }\mathrm{Let},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢M:{\sigma }_1\\ \mathcal{D}::\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2\end{array}}{\mathrm{\Gamma }⊢M:{\sigma }_2}\mathrm{Sub}.$$ Hierarchy introduction is intentionally nondependent. Dependency is added by matching and self-recognition, not guessed by the introduction rule: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢M_1:{\sigma }_1\\ \mathrm{\Gamma }⊢M_2:{\sigma }_2\end{array}}{\mathrm{\Gamma }⊢⟨M_1;M_2⟩:\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2}\mathrm{Hierarchy}.$$ $$\frac{\mathrm{\Gamma }⊢M:\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2}{\mathrm{\Gamma }⊢M.1:{\sigma }_1}\mathrm{First},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢M:\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\\ X\notin \mathrm{FV}({\sigma }_2)\end{array}}{\mathrm{\Gamma }⊢M.2:{\sigma }_2}\mathrm{Second}.$$ Direct second projection is therefore forbidden while the range mentions the first path. The abbreviation $\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2$ records this displayed freshness premise; it does not encode an additional rule.

The two-sorted basic projections have distinct judgments: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢Q\mathsf{projectible}\\ \mathrm{\Gamma }⊢Q:\mathsf{B}(u::\kappa ;\tau )\end{array}}{\mathrm{\Gamma }⊢Q.s::\kappa }\mathrm{Static}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢M:\mathsf{B}(u::\kappa ;\tau )\\ u\notin \mathrm{FV}(\tau )\end{array}}{\mathrm{\Gamma }⊢M.d:\tau }\mathrm{Dynamic}.$$ Thus Static requires a stable path, and Dynamic requires a nondependent basic signature. A dependent dynamic type is first made nondependent by self-recognition and signature equivalence: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢Q:\mathsf{B}(u::\kappa ;\tau )\\ \mathrm{\Gamma }⊢Q\mathsf{projectible}\end{array}}{\mathrm{\Gamma }⊢Q:\mathsf{B}(u::\mathsf{Sing}(Q.s);\tau )}\mathrm{Self}.$$ Hierarchy self-recognition propagates the signatures of projectible components: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢Q\mathsf{projectible}\\ \mathrm{\Gamma }⊢Q:\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\\ \mathrm{\Gamma }⊢Q.1:{\sigma }_1^{\prime }\\ \mathrm{\Gamma }⊢{\sigma }_1^{\prime }{⪯}_{\mathsf{s}}{\sigma }_1\end{array}}{\mathrm{\Gamma }⊢Q:\mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2}\mathrm{Self}-\mathrm{First},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢Q\mathsf{projectible}\\ \mathrm{\Gamma }⊢Q:\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2\\ \mathrm{\Gamma }⊢Q.2:{\sigma }_2^{\prime }\\ \mathrm{\Gamma }⊢{\sigma }_2^{\prime }{⪯}_{\mathsf{s}}{\sigma }_2\end{array}}{\mathrm{\Gamma }⊢Q:\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2^{\prime }}\mathrm{Self}-\mathrm{Second}.$$ Finally, functors are checked by $$\frac{\mathrm{\Gamma },X:{\sigma }_1⊢M:{\sigma }_2}{\mathrm{\Gamma }⊢\lambda X:{\sigma }_1.M:\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2}\mathrm{Functor}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢F:\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2\\ \mathrm{\Gamma }⊢A:{\sigma }_1\\ X\notin \mathrm{FV}({\sigma }_2)\end{array}}{\mathrm{\Gamma }⊢F(A):{\sigma }_2}\mathrm{Apply}.$$ Thus the range dependency must be eliminated before application. As above, an underscore in this binder abbreviates the displayed freshness premise.

The conclusion of Basic recognizes the constructor it contains. The conclusion of Seal has exactly the written interface, and the result is not a path. Transparent ascription is not a second term former: it is matching by subsignature, which retains every singleton written in the target. Opaque sealing forgets every equation absent from its target.

A surface constraint with type s = c is represented by the singleton signature $\mathsf{B}(s::\mathsf{Sing}(c);\tau )$. A sharing type constraint uses $\mathsf{Sigma}$-dependency followed by singleton matching, while opaque ascription is $M\upharpoonright \sigma$.

Matching, hierarchies, and sharing

Write $\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2$ when every module matching ${\sigma }_1$ may be used at ${\sigma }_2$. Subkinding is written ${\kappa }_1{⪯}_{\mathsf{k}}{\kappa }_2$; ordinary dynamic-type subtyping retains . These judgments express signature matching, kind inclusion, and dynamic type conversion, respectively; none entails either of the others. Subsignature matching is the least relation generated by $$\frac{\mathrm{\Gamma }⊢\sigma \mathsf{sig}}{\mathrm{\Gamma }⊢\sigma {⪯}_{\mathsf{s}}\sigma }\mathrm{Sig}-\mathrm{Refl},\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2\\ \mathrm{\Gamma }⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_3\end{array}}{\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_3}\mathrm{Sig}-\mathrm{Trans},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1\equiv {\sigma }_1^{\prime }\mathsf{sig}\\ \mathrm{\Gamma }⊢{\sigma }_1^{\prime }{⪯}_{\mathsf{s}}{\sigma }_2^{\prime }\\ \mathrm{\Gamma }⊢{\sigma }_2^{\prime }\equiv {\sigma }_2\mathsf{sig}\end{array}}{\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2}\mathrm{Sig}-\mathrm{Convert},$$ and these variance rules: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_1^{\prime }\\ \mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_2^{\prime }\end{array}}{\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2{⪯}_{\mathsf{s}}\mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }}\mathrm{Sigma}-\mathrm{Match},$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢{\sigma }_1^{\prime }{⪯}_{\mathsf{s}}{\sigma }_1\\ \mathrm{\Gamma },X:{\sigma }_1^{\prime }⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_2^{\prime }\end{array}}{\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2{⪯}_{\mathsf{s}}\mathsf{Pi}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }}\mathrm{Pi}-\mathrm{Match}.$$ In Sigma-Match, self-recognition of the first component propagates its singleton equations while the second components are compared. This is the sharing mechanism.

Proof of Proposition 14.7 — Termination and soundness of algorithmic matching

Proof. Order calls by the sum of the numbers of $\mathsf{B}$, $\mathsf{Sigma}$, and $\mathsf{Pi}$ nodes in the two inputs. Every recursive call compares proper component signatures, so this measure decreases. Constructor normalization and all leaf decisions terminate by proposition 14.1.

For soundness, induct on the returned trace. A basic trace contains exactly the two premises of B-Match. A hierarchy trace contains the first component derivation and the continuation derivation under $X:{\sigma }_1$, exactly as required by Sigma-Match. A functor trace records the reversed domain derivation and covariant codomain derivation required by Pi-Match. The normalization records are constructor and signature conversions, so Sig-Convert transports the structural derivation back to the input signatures. ◻

For a fixed element constructor $a::\mathsf{Ty}$, let $$\mathsf{SET}[a]:=\mathsf{B}(r::\mathsf{Ty};r\times (a\to r\to r)\times (a\to r\to \mathbf{2})).$$ The shared hierarchy signature is $$\mathsf{ORDSET}:=\mathsf{Sigma}(X:\mathsf{ORDERED}).\mathsf{SET}[X.s].$$ Suppose $p_O:\mathsf{ORDERED}[\mathbb{N}]$ and $p_S:\mathsf{SET}[\mathbb{N}]$ are projectible values. Their explicit pair is first checked at the nondependent signature $$\mathsf{Sigma}{(}_{:}\mathsf{ORDERED}[\mathbb{N}]).\mathsf{SET}[\mathbb{N}].$$ Matching the first component to $X:\mathsf{ORDERED}$ makes $X.s\equiv \mathbb{N}$ while the second is checked, so the pair also matches $\mathsf{ORDSET}$. The equality was transported by the hierarchy; it was not reconstructed from dynamic operations.

The algorithmic trace has three nodes. At the root, the two signatures are $\mathsf{Sigma}$-signatures. Their first components match by B-Match: $\mathsf{Sing}(\mathbb{N}){⪯}_{\mathsf{k}}\mathsf{Ty}$, and expanding the dynamic comparison type replaces its carrier by $\mathbb{N}$. For the second recursive call the context is $X:\mathsf{ORDERED}[\mathbb{N}]$, whose static projection contributes the manifest equation $X.s\mapsto \mathbb{N}$. Expansion therefore changes $\mathsf{SET}[X.s]$ to $\mathsf{SET}[\mathbb{N}]$, and the basic-signature comparison succeeds reflexively. The returned root is Sigma-Match with exactly these two subderivations.

Here is the complete derivation in the selected rules. Let ${\tau }_S(a,r):=r\times (a\to r\to r)\times (a\to r\to \mathbf{2})$, and suppose $v_S:{\tau }_S(\mathbb{N},\mathsf{List}\mathbb{N})$. Rule Basic, followed by B-Match and Sub, gives $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathsf{List}\mathbb{N}::\mathsf{Ty}\\ v_S:{\tau }_S(\mathbb{N},\mathsf{List}\mathbb{N})\end{array}}{⟨\mathsf{List}\mathbb{N};v_S⟩:\mathsf{B}(r::\mathsf{Sing}(\mathsf{List}\mathbb{N});{\tau }_S(\mathbb{N},r))}}\mathrm{Basic}\\ \mathsf{B}(r::\mathsf{Sing}(\mathsf{List}\mathbb{N});{\tau }_S(\mathbb{N},r)){⪯}_{\mathsf{s}}\mathsf{SET}[\mathbb{N}]\end{array}}{p_S:\mathsf{SET}[\mathbb{N}]}\mathrm{Sub}.$$ Together with $p_O:\mathsf{ORDERED}[\mathbb{N}]$, Hierarchy yields $$\frac{\begin{array}{c}{p}_O:\mathsf{ORDERED}[\mathbb{N}]\\ p_S:\mathsf{SET}[\mathbb{N}]\end{array}}{⟨p_O;p_S⟩:\mathsf{Sigma}{(}_{:}\mathsf{ORDERED}[\mathbb{N}]).\mathsf{SET}[\mathbb{N}]}\mathrm{Hierarchy}.$$ Finally, under $X:\mathsf{ORDERED}[\mathbb{N}]$, rule Static and the singleton elimination give $X.s\equiv \mathbb{N}$. Therefore $\mathsf{SET}[\mathbb{N}]\equiv \mathsf{SET}[X.s]$, and the final matching and subsumption are $$\frac{\begin{array}{c}⟨p_O;p_S⟩:\mathsf{Sigma}{(}_{:}\mathsf{ORDERED}[\mathbb{N}]).\mathsf{SET}[\mathbb{N}]\\ {\displaystyle \frac{\begin{array}{c}\mathsf{ORDERED}[\mathbb{N}]{⪯}_{\mathsf{s}}\mathsf{ORDERED}\\ X:\mathsf{ORDERED}[\mathbb{N}]⊢\mathsf{SET}[\mathbb{N}]{⪯}_{\mathsf{s}}\mathsf{SET}[X.s]\end{array}}{\mathsf{Sigma}{(}_{:}\mathsf{ORDERED}[\mathbb{N}]).\mathsf{SET}[\mathbb{N}]{⪯}_{\mathsf{s}}\mathsf{ORDSET}}}\mathrm{Sigma}-\mathrm{Match}\end{array}}{⟨p_O;p_S⟩:\mathsf{ORDSET}}\mathrm{Sub}.$$

Second projection is deliberately restricted. A phrase $M.2$ may be typed directly only after the range signature is nondependent. For the pair above, matching first specializes $\mathsf{SET}[X.s]$ to $\mathsf{SET}[\mathbb{N}]$, and only then is the projection formed. This order prevents a local path $X$ from escaping.

Proof of Proposition 12.4 — Sharing preservation

Proof. Rule B-Match gives $\mathsf{ORDERED}[c]{⪯}_{\mathsf{s}}\mathsf{ORDERED}$: its static premise is $\mathsf{Sing}(c){⪯}_{\mathsf{k}}\mathsf{Ty}$, and its dynamic premise is reflexive after singleton elimination. Rule Self-First, using this match and the last premise of the proposition, derives $$\mathrm{\Gamma }⊢M:\mathsf{Sigma}(X:\mathsf{ORDERED}[c]).\mathsf{SET}[X.s].$$ Under $X:\mathsf{ORDERED}[c]$, rules Static and Self give $X.s::\mathsf{Sing}(c)$, hence $X.s\equiv c::\mathsf{Ty}$. By Sigma-Eq, $$\mathsf{Sigma}(X:\mathsf{ORDERED}[c]).\mathsf{SET}[X.s]\equiv \mathsf{Sigma}{(}_{:}\mathsf{ORDERED}[c]).\mathsf{SET}[c].$$ Rule Second now derives $\mathrm{\Gamma }⊢M.2:\mathsf{SET}[c]$. Its dynamic product contains $c\to r\to r$, which is the stated insert type. ◻

Generative functors

Rule Apply requires a nondependent result. A dependent functor is used by first matching its projectible argument to a manifest signature and reducing the result dependency.

Assume the core list constructor and its usual empty, insertion, and membership operations. In a context $X:\mathsf{ORDERED}$, let ${\mathsf{member}}_X$ be list membership computed with the comparison in $X.d$, and define The three dynamic fields have types $\mathsf{List}X.s$, $X.s\to \mathsf{List}X.s\to \mathsf{List}X.s$, and $X.s\to \mathsf{List}X.s\to \mathbf{2}$. Hence Basic, Seal, and Functor derive $$\mathsf{SetFn}:\mathsf{Pi}(X:\mathsf{ORDERED}).\mathsf{SET}[X.s].$$ Given $p_O:\mathsf{ORDERED}[\mathbb{N}]$, Pi-Match compares the domain contravariantly and specializes the result under the manifest argument; Sub then gives $$\mathsf{SetFn}:\mathsf{Pi}(X:\mathsf{ORDERED}[\mathbb{N}]).\mathsf{SET}[\mathbb{N}].$$ Now Apply derives $\mathsf{SetFn}(p_O):\mathsf{SET}[\mathbb{N}]$.

The application is not projectible. If the body creates an abstract representation, each annotated binding $$(\mathsf{let}{S}_i=\mathsf{SetFn}(p_O)\upharpoonright \mathsf{SET}[\mathbb{N}]\mathsf{in}{M}_i):\sigma$$ introduces a fresh abstract representation path for $S_i.s$. Even with the same functor and argument, $S_1.s$ and $S_2.s$ are unrelated unless an outer hierarchy explicitly shares them. This is the principal generative discipline.

Elaboration of the matched fragment

Dependent paths must be resolved before ordinary existential packages can be a target. We therefore state elaboration only for signatures whose hierarchy and functor dependencies have already been eliminated by matching.

The module reduction relation ${⟶}_{\mathcal{D}}$ is call by value. Its operational module values, written $V$, are $$V::=⟨c;v⟩\mid ⟨V_1;V_2⟩\mid \lambda X:\sigma .M.$$ Unlike the open module-value judgment, this grammar has no variable case. The let and application contractions below use only this operational grammar. In particular a seal is not a value, matching PFPL’s abstraction boundary.

The sorted root contractions are exactly The seal step is administrative erasure at runtime. Its label retains the matching derivation $\mathcal{D}::{\sigma }_0{⪯}_{\mathsf{s}}\sigma$: the reduct is typed at $\sigma$ by Sub, so erasure does not restore a hidden static equation. Static projection computes by constructor equivalence, $(⟨c;v⟩).s\equiv c$; hierarchy-path projections compute in the same way. They are not dynamic steps.

Module evaluation contexts are module-sorted: Ordinary expression contexts are those of the core. Two cross-sort rules evaluate a module inside a dynamic projection and an expression inside a basic structure. Compatible closure is therefore the following complete family: $$\frac{R⟶R^{\prime }}{{\mathcal{E}}_M[R]⟶{\mathcal{E}}_M[R^{\prime }]}\mathrm{M}-\mathrm{Context}.$$ $$\frac{M⟶M^{\prime }}{M.d⟶M^{\prime }.d}\mathrm{D}-\mathrm{Context}.$$ $$\frac{e⟶e^{\prime }}{⟨c;e⟩⟶⟨c;e^{\prime }⟩}\mathrm{Basic}-\mathrm{Context}.$$ No reduction crosses a functor body or the body of an annotated let before its binder is discharged. Equations (12.1)–(12.5) and the three context rules are the entire selected module dynamics.

The rules compute rather than merely classify. Let $\sigma =\mathsf{B}(u::\kappa ;\tau )$, let $V=⟨c;v⟩$ match $\sigma$, and let $W$ be a module value of a functor’s domain. Then By contrast, a functor abstraction is a value, so no rule reduces inside its body before application.

Proof of Lemma 14.15 — Projectible-witness coherence

Proof. Use the recursion defining $\mathsf{View}$. For an opened variable, all three judgments are entries installed together by $\rho {\oplus }_{\sigma }(X\mapsto z)$. For an explicit basic path they are the premises of Basic. A projection selects the corresponding recursively typed component. A final Sub preserves the static constructor and applies its displayed dynamic coercion; signature conversion transports the three judgments without computation. The three self rules select or reassemble the same recursively computed view. These cases exhaust the projectible grammar and its possible final typing rules.

The conversion $c_Q\equiv {\mathsf{stat}}_{\rho }(Q)$ lets singleton checking view $c_Q$ at $\mathsf{Sing}({\mathsf{stat}}_{\rho }(Q))$. Existential introduction with the already typed $e_Q$ gives the final package judgment. No equality between two independently unpacked witnesses is used. ◻

Proof of Theorem 12.7 — Supported elaboration

Proof. Induct on $\mathcal{E}$. The Var case uses its corresponding opened component. The Basic case is existential introduction, using $c::\kappa$ and $e:\tau [c/u]$. Seal and subsumption use the matching coercion defined above. Hierarchy introduction and projection are product introduction and elimination. The projectible-witness lemma gives the Self case. Each hierarchy-self case uses product introduction, with induction hypotheses for the original hierarchy and its refined component.

Functor cases are function introduction and elimination. The term former ${\mathsf{Open}}_{\sigma }$ places the argument witness around the translated body. Annotated let uses the same opening operation after one target let has evaluated its definition; its annotated result excludes $X$, so existential elimination is well scoped. For Dynamic, if $\rho (X.d)=e$, elaboration returns the already opened field $e$; otherwise the nondependent result type permits unpacking the module locally. Basic, hierarchy, functor, seal, let, self, static-projection, and dynamic-projection cases exhaust the selected elaboration forms. ◻

Proof of Lemma 14.17 — Operational values elaborate to target values

Proof. Induct on $V$. A basic value translates to a package whose payload is a target value by the inherited expression-value lemma. A hierarchy translates componentwise; reduce each component by the induction hypotheses to obtain a pair of values. A functor abstraction translates to a target abstraction. Final matching adds only the terminating package coercions displayed above; their unpack redexes contract once the induction hypothesis has produced the package value. Self-recognition instead repacks the already exposed projectible view and introduces no fresh unpack redex. ◻

Proof of Lemma 14.18 — Derivation substitution

Proof. By lemma 14.17, the translated $V$ reaches a target value, so every package opening below reaches its unpack contraction. Induct on ${\mathcal{E}}_M$. If the last rule is Var for $X$, the opening clauses expose exactly the static, dynamic, and whole-module components of $V$. A different variable is unchanged. The Basic case is the inherited expression-substitution lemma under existential introduction. Seal and subsumption retain their displayed matching derivation, so the induction hypothesis is closed under the same ${\mathsf{mcoe}}_{\mathcal{D}}$. Hierarchy formation and both projections use product congruence. In a Self case, hereditary substitution either preserves the projectible path or exposes a basic value and rebuilds Basic; the view recursion of lemma 14.15 gives the same static and dynamic components on both sides. For either hierarchy-self rule, an exposed hierarchy value is decomposed, the selected component is rebuilt recursively, and Hierarchy reassembles the result. Thus a functor in an unselected component causes no false projectibility premise. The two Dynamic cases use respectively the installed field and existential beta-reduction. In annotated let and functor abstraction, alpha-renaming prevents capture and the induction hypothesis applies beneath the new opening. Application uses function congruence. This exhausts the module grammar. ◻

Proof of Theorem 12.8 — Simulation and module safety

Proof. The dynamic projection of an explicit basic module takes zero target steps; a hierarchy projection takes one product step. Let and application use lemma 14.18 after the target let or beta step. For the seal root, the reduct is translated through the retained Sub derivation, so both sides contain the same ${\mathsf{mcoe}}_{\mathcal{D}}$; zero target steps suffice. If $\mathcal{E}$ ends in Self, its reduct derivation retains the rule or rebuilds Basic after hereditary substitution. In both cases the induction hypothesis is closed under the projectible view by lemma 14.15. For either hierarchy-self rule, hereditary substitution decomposes an exposed value as in lemma 14.18; product congruence then applies to the original hierarchy and to the retranslated selected component. The three context rules follow by target compatible closure. Target progress gives the final claim after theorem 12.7; preservation retains its package type. This is a target-safety consequence, not a proof of source progress. ◻

Representation independence at one interface

Let $$\mathsf{COUNTER}:=\mathsf{B}(t::\mathsf{Ty};t\times ((t\to t)\times (t\to \mathbb{N}))).$$ Consider Relate $n:\mathbb{N}$ to $(m,\star ):\mathbb{N}\times \mathbf{1}$ exactly when $n=m$. The initial states are related, the step functions preserve this relation, and the read functions return equal naturals.

The three interface obligations are calculations: Thus initial states are related, steps preserve $R$, and reads of related states agree.

Proof of Lemma 12.10 — Counter fundamental relation

Proof. First record the compatibility calculation for applications. Assume $$f{C}_{A\to B}g\text{and}a{C}_{A}b.$$ Evaluate the four terms to $f_0,g_0,a_0,b_0$. Their value relations and the arrow clause give $$f_0{a}_0{C}_B{g}_0{b}_0.$$ Call-by-value compatibility prefixes the four evaluation sequences. Products and projections have the corresponding calculation.

Now induct on the typing derivation. Variables reduce in zero steps to the related values from the environment; constants relate to themselves. Pairing and projection use product compatibility. For abstraction, if $a_N{V}_A{a}_P$, the body induction hypothesis proves $e[{\rho }_N,x\mapsto a_N]C_{B}e[{\rho }_P,x\mapsto a_P]$. Therefore the two abstraction values satisfy the arrow clause; application uses the compatibility calculation above. The three distinguished variables satisfy their clauses by the initial-state, step-preservation, and observation calculations. No other case inspects a value of abstract type $t$. ◻

Proof of Theorem 12.11 — Counter representation independence

Proof. Opening either translated sealed package introduces exactly the abstract state, initial state, step, and read components named in definition 12.9. Existential elimination keeps the witness out of the result type, so a client in that grammar cannot name it. Apply lemma 12.10 to the environments containing the related states and operations. The resulting computations evaluate to $V_{\mathbb{N}}$-related values, which are the same numeral. Strong normalization of the simply typed client calculus gives the two values, and determinacy of pure evaluation makes them the stated observations. ◻

Principal matching, exactly where it exists

Opaque seals and generative applications erase or create static identity. Principal recognition is therefore about projectible paths, not arbitrary module phrases.

Assume principal core typing: each closed value $v$ has a partial principal type $\mathsf{pty}(v)$, and every other type of $v$ is a supertype. A closed constructor $c$ has principal kind $\mathsf{Sing}(c)$. Core typing has inversion modulo equivalence and subsumption.

Proof of Lemma 14.26 — Static shape of every principal basic component

Proof. Induct on the derivation that computes the principal-signature tree of $p$, with the induction claim quantified over every position in that tree. At a basic leaf $⟨c;v⟩$, the first clause of $\mathsf{psig}$ and $(⟨c;v⟩).s\equiv c$ give the equation. At a hierarchy, a position begins with $1$ or $2$; apply the corresponding component induction hypothesis to the remaining position. A projection selects exactly that subtree, so the same component hypothesis applies without requiring the whole hierarchy to have a basic principal signature. These are all clauses that compute $\mathsf{psig}$. ◻

Proof of Lemma 14.27 — Narrowing

Proof. Prove both statements simultaneously by induction on the affected derivation. Variable cases use the assumed subkind or subsignature and one transitivity step. Binder cases first alpha-rename and apply the induction hypothesis to the extended context. Conversion cases use preservation of constructor equality under the narrower context, established by the simultaneous induction; termination of conversion is irrelevant here. Singleton elimination is the only new case beyond the inherited core. In the dependent Sigma-Match case, first narrow the first-component matching premise; then apply the induction hypothesis to the second-component judgment in the narrowed context and rebuild Sigma-Match. The B-Match and Pi-Match cases follow the variance in their premises. The typing rules use the signature half of the simultaneous statement. ◻

Proof of Lemma 14.28 — Structural matching inversion

Proof. Induct on the matching derivation. Reflexive and conversion steps disappear. In a transitive composite, apply the induction hypotheses and compose the kind, type, or component premises. The bound context in the second component may change at the middle signature; lemma 14.27 transports that premise before transitivity is applied. Shape preservation of the assumed conversion procedure rules out a basic-to-hierarchy or hierarchy-to-functor conversion. The remaining last rule is the corresponding structural rule. ◻

Proof of Corollary 14.29 — Decision and completeness of structural matching

Proof. The reverse implication is proposition 14.7. For the forward implication, apply lemma 14.28. Its normalized last rule is B-Match, Sigma-Match, or Pi-Match; the corresponding algorithm clause invokes the induction hypothesis on exactly its premises. Signature-conversion steps are absorbed by the initial normalization. Induction on the total signature-node count terminates with the basic case. ◻

Proof of Lemma 14.30 — Typing factorization for projectible paths

Proof. Induct first on the height of $\mathcal{P}$, using the grammar of $p$ in the introduction and projection cases. A final Sub or signature-equivalence conversion composes the induction matching with its displayed match by Sig-Trans or Sig-Convert.

Suppose the final rule is Self. Write $\mathsf{psig}(p)=\mathsf{B}(a::{\kappa }_0;{\tau }_0)$. The induction hypothesis factors the premise typing through $$\mathsf{B}(a::{\kappa }_0;{\tau }_0){⪯}_{\mathsf{s}}\mathsf{B}(u::\kappa ;\tau ).$$ After self-recognition the required match is $$\mathsf{B}(a::{\kappa }_0;{\tau }_0){⪯}_{\mathsf{s}}\mathsf{B}(u::\mathsf{Sing}(p.s);\tau ),$$ whose premises are ${\kappa }_0{⪯}_{\mathsf{k}}\mathsf{Sing}(p.s)$ and . Structural matching inversion proves the second premise under $a::{\kappa }_0$. By lemma 14.26, ${\kappa }_0\equiv \mathsf{Sing}(p.s)$, which proves the first. These premises form a B-Match to the conclusion $\mathsf{B}(u::\mathsf{Sing}(p.s);\tau )$.

Suppose the final rule is Self-First. Normalize the induction match for its hierarchy premise. Its second component gives the required match from the nondependent second component of $\mathsf{psig}(p)$ to ${\sigma }_2$. The induction hypothesis for the premise $p.1:{\sigma }_1^{\prime }$ gives $\mathsf{psig}(p.1){⪯}_{\mathsf{s}}{\sigma }_1^{\prime }$. These two premises combine by Sigma-Match. The displayed ${\sigma }_1^{\prime }{⪯}_{\mathsf{s}}{\sigma }_1$ premise of Self-First justifies checking the reused range ${\sigma }_2$ under its refined binder. The Self-Second case is symmetric: its original hierarchy match proves the first-component premise, and the induction hypothesis for $p.2:{\sigma }_2^{\prime }$ proves the refined second-component premise; then apply Sigma-Match.

The remaining last rules follow the path grammar. For $p=⟨c;v⟩$, inversion leaves Basic. Core factorization gives $\mathsf{Sing}(c){⪯}_{\mathsf{k}}\kappa$ and ; singleton substitution and B-Match finish. For $p=⟨p_1;p_2⟩$, inversion leaves Hierarchy, and the component induction hypotheses combine by Sigma-Match. For $p=q.i$, inversion leaves First or Second; normalize the induction match for $q$ and select its corresponding component premise. A closed derivation cannot end in Var, and no other typing rule concludes a projectible phrase. ◻

Proof of Theorem 12.13 — Principal matching for closed projectible values

Proof. The canonical derivation and the displayed match are lemma 14.30. If ${\sigma }^{\prime }$ has the same universal property, then $p:{\sigma }^{\prime }$ gives $\mathsf{psig}(p){⪯}_{\mathsf{s}}{\sigma }^{\prime }$. Applying the property of ${\sigma }^{\prime }$ to the canonical typing $p:\mathsf{psig}(p)$ gives the reverse match. No antisymmetry principle is among the selected rules, so mutual matching is the strongest conclusion. ◻

Proof-relevant phase distinction: a backward comparison

The reduced calculus keeps static constructors and dynamic terms in one judgment but restricts dependency to projectible paths. Sterling and Harper instead make the phase boundary an internal proposition, written $\mathsf{bst}$: under that assumption dynamic inhabitants of a fixed type are identified, while type and signature components retain their static information. A static-extent signature then classifies modules whose restriction under $\mathsf{bst}$ agrees with a specified module. This can constrain a whole nested structure, not only one type projection [SH21].

Here is one concrete nested family on which the distinction matters. This is comparison notation for ModTT, not an extension of the grammar in section 12.1. It uses ModTT’s dependent products over dynamic signatures, not an assumed object-language function type [SH21]. For a closed type $T$, put The angle brackets classify dynamic values at the displayed type from the object language, and $\mathsf{Pi}$ classifies a module functor. Thus a value of $\sigma (T)$ is a nested module $$U=[X,[\mathsf{pack},\mathsf{unpack}]],$$ whose outer static component is $X$ and whose inner structure contains the two dynamic maps. Define the closed module functor $$V(T,U):=[X,\lambda z:⟨T⟩.\mathsf{pack}(\mathsf{unpack}z)]:\tau (T).$$ The result preserves the input’s static type component and computes its dynamic round trip.

Fix closed types $T_0,T_1$, modules $U_i=[X_i,[{\mathsf{pack}}_i,{\mathsf{unpack}}_i]]:\sigma (T_i)$, and a proof-relevant relation $\tilde{T}(t_0,t_1)$, an $\alpha$-small set of witnesses rather than a truth value, indexed by pairs of closed dynamic values $t_i:T_i$. An input relation witness consists of an $\alpha$-small family of sets $\tilde{X}(x_0,x_1)$ and maps The nested output witness is calculated, not merely asserted: If a fiber of $\tilde{T}$ or $\tilde{X}$ has two inhabitants, the construction retains which witness was supplied. Replacing each fiber by a mere proposition would erase that distinction.

The phase sensitivity appears in the two components of this calculation. The map on static components sends the witness family $\tilde{X}$ for the input type components to the same family for the output type components. The dynamic map sends each witness $r$ to $w_{\mathsf{round}}(r)$. Under $\mathsf{bst}$, the dynamic maps are identified and only the tracked static component remains observable. Outside that open phase, the dynamic witness transformation is retained.

Proof of Theorem 14.32 — Phase-sensitive transport—imported

Proof. The displayed function of phase-separated sets is Sterling and Harper’s generalized abstraction theorem [SH21]. Unfolding the dependent-sum and dependent-product relational actions specializes its dynamic action to $w_{\mathsf{round}}$, while its static action preserves $\tilde{X}$. The model construction and fundamental theorem that justify the general transport are imported; the two-line calculation is local. Neither is a consequence of principal matching in ${\mathrm{MLMod}}_0$. ◻

This comparison adds neither ModTT nor its model theory to the principal calculus. In particular, its generalized abstraction theorem does not transfer to Standard ML, the reduced matching judgment, applicative functors, modular implicits, or separate compilation. The local representation theorem above remains proof-irrelevant and tied to one counter interface.

When a generated name must leave scope

The annotation on module let is forced by an extrusion problem. The following is Crary’s comparison-language example, not a phrase of the reduced grammar in definition 12.1: that grammar has neither parameterized type components nor datatypes. In the comparison notation, $\mathsf{int}u$ means postfix application of the unary type component $u$ to the type $\mathsf{int}$, and $\mathsf{datatype}v=D\mathsf{of}t$ introduces a fresh result type $v$ with constructor $D:t\to v$. Consider a local generative declaration of $t$, followed by a sealed result with $$\mathsf{type}{}^{\prime }au=t,\mathsf{datatype}v=D\mathsf{of}t,x:\mathsf{int}u,y:\mathsf{bool}u.$$ The local name $t$ cannot occur in the exported signature. Replacing it by one visible component is not principal. A signature may reveal ${}^{\prime }au=v$, or retain different relationships among $u$, $v$, $x$, and $y$; here $u$ is a unary type component and $D:t\to v$ is the datatype constructor. Two ordinary avoiding signatures can retain all four visible fields while assigning the constructor, respectively, $$D:\mathsf{int}u\to v\text{and}D:\mathsf{bool}u\to v.$$ The first signature types $Dx$ but not $Dy$; the second types $Dy$ but not $Dx$. Each therefore exposes a typing fact absent from the other, so neither signature subsigns the other. This incomparability does not by itself exclude a third ordinary signature below both. It does show that the two visible candidates do not determine a unique answer, and the reduced algorithm specified here has no least-avoidance construction. It therefore rejects the phrase or requests an annotation.

Focused avoidance.

Crary extends the signature language with existential signatures. In his calculus an existential signature is the least avoiding supersignature of the dependent body; consequently it lies below every admissible ordinary avoiding answer in the subsignature order. For user modules in synthesis contexts, focused synthesis is sound and complete for the declarative system, with subsignature completeness restricted to synthesis signatures on the left and analysis signatures on the right [Cra21]. Our reduced PFPL calculus has neither existential signatures nor that algorithm. We use the counterexample to justify annotations; no avoidance theorem is imported into theorem 12.13.

Generativity and the applicative alternative

Applicative functors.

PFPL’s alternative adds exactly $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢F\mathsf{projectible}\\ \mathrm{\Gamma }⊢A\mathsf{val}\end{array}}{\mathrm{\Gamma }⊢F(A)\mathsf{projectible}}\mathrm{App}-\mathrm{P},\frac{\mathrm{\Gamma }⊢Q\mathsf{projectible}}{\mathrm{\Gamma }⊢Q\upharpoonright \sigma \mathsf{projectible}}\mathrm{Seal}-\mathrm{P}.$$ The first premise asserts that the functor expression is a stable path; the argument need only be a value. The second rule is required because an applicative functor body may seal its result. The price is a new equivalence problem: equality of result paths depends on equality of the functor, argument, and sealed module expressions, which may expose executable code to static comparison. A runtime conditional module therefore has no stable path. This is the complete boundary developed in PFPL Section 45.4, rules 45.7–45.8. We add neither rule to the principal calculus, and none of the generativity, elaboration, or principality results above should be reread applicatively.

The main calculus therefore follows a Standard-ML-style generative policy: each functor application may allocate fresh abstract identities. A common OCaml-style applicative policy instead equates repeated applications $F(P).s$ only when the argument is a stable module path $P$; generativity can then be requested by applying a unit functor. PFPL’s displayed App-P is broader because its argument premise admits any value. These are three distinct policies, and the companion’s optional applicative mode is an experiment rather than a claim that they coincide.

Generated interfaces and incremental compilation.

Crary’s algorithm writes synthesized interfaces that may contain existential signatures. A downstream unit may compile against such a generated synthesis interface because it occurs in the context, while programmer-written modules and annotations remain existential-free user syntax. The right side of each subsignature query is therefore an analysis signature, exactly the condition used by completeness. This supports the incremental-compilation scenario of [Cra21]; it is not a separate-compilation theorem for Standard ML, MixML, or the reduced calculus of this chapter.

Recursive mixin linking.

MixML unifies structures and signatures as mixins with specified and defined components. Its published system supports recursive, higher-order, and first-class linking, proves soundness and completeness of a three-pass checker, and elaborates to an internal language with single-assignment references, recursive type generativity, and linear definedness [RD13]. This language is richer than our acyclic $\mathsf{Sigma}/\mathsf{Pi}$ fragment. Its theorems are source-gated facts about MixML, not missing cases of theorem 12.7, theorem 12.13.

Cardelli and Wegner’s classification of universal, existential, inclusion, and ad-hoc polymorphism orients the package boundary [CW85]; it does not supply path, sharing, or matching theorems. The load-bearing module rules and projectibility boundary are the reduced PFPL system. The avoidance, applicative, and MixML paragraphs mark separate proof boundaries where a reader might otherwise conflate them.