Generative ML modules, matching, and sharing

The reduced calculus uses one mixed context and the signatures $$\sigma ::=\mathsf{B}(u::\kappa ;\tau )\mid \mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\mid \mathsf{Pi}(X:{\sigma }_1).{\sigma }_2.$$ Its singleton-kind delta is

$\mathrm{\Gamma }⊢c::\mathsf{Ty}$

$\mathrm{\Gamma }⊢\mathsf{Sing}(c)\mathsf{kind}$

$\mathrm{\Gamma }⊢c::\mathsf{Ty}$

$\mathrm{\Gamma }⊢c::\mathsf{Sing}(c)$

$\mathrm{\Gamma }⊢c::\mathsf{Ty}$

$\mathrm{\Gamma }⊢\mathsf{Sing}(c){⪯}_{\mathsf{k}}\mathsf{Ty}$

$\mathrm{\Gamma }⊢d::\mathsf{Sing}(c)$

$\mathrm{\Gamma }⊢d\equiv c::\mathsf{Ty}$

Their formation rules are

$\mathrm{\Gamma }⊢\kappa \mathsf{kind}$$\mathrm{\Gamma },u::\kappa ⊢\tau \mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{B}(u::\kappa ;\tau )\mathsf{sig}$

$\mathrm{\Gamma }⊢{\sigma }_1\mathsf{sig}$$\mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\mathsf{sig}$

$\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\mathsf{sig}$

$\mathrm{\Gamma }⊢{\sigma }_1\mathsf{sig}$$\mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\mathsf{sig}$

$\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2\mathsf{sig}$

Signature equality is the congruence generated by inherited kind, constructor, and type equality:

$\mathrm{\Gamma }⊢{\kappa }_1\equiv {\kappa }_2\mathsf{kind}$$\mathrm{\Gamma },u::{\kappa }_1⊢{\tau }_1\equiv {\tau }_2\mathsf{type}$

$\mathrm{\Gamma }⊢\mathsf{B}(u::{\kappa }_1;{\tau }_1)\equiv \mathsf{B}(u::{\kappa }_2;{\tau }_2)\mathsf{sig}$

$\mathrm{\Gamma }⊢{\sigma }_1\equiv {\sigma }_1^{\prime }\mathsf{sig}$$\mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\equiv {\sigma }_2^{\prime }\mathsf{sig}$

$\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2\equiv \mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }\mathsf{sig}$

$\mathrm{\Gamma }⊢{\sigma }_1\equiv {\sigma }_1^{\prime }\mathsf{sig}$$\mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2\equiv {\sigma }_2^{\prime }\mathsf{sig}$

$\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2\equiv \mathsf{Pi}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }\mathsf{sig}$

The open module-value judgment is generated by

$X:\sigma \in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢X\mathsf{mval}$

$\mathrm{\Gamma }⊢v\mathsf{val}$

$\mathrm{\Gamma }⊢⟨c;v⟩\mathsf{mval}$

$\mathrm{\Gamma }⊢V_1\mathsf{mval}$$\mathrm{\Gamma }⊢V_2\mathsf{mval}$

$\mathrm{\Gamma }⊢⟨V_1;V_2⟩\mathsf{mval}$

$\mathrm{\Gamma }⊢\lambda X:\sigma .M\mathsf{mval}$

Stable paths are generated by $$Q::=X\mid ⟨c;v⟩\mid ⟨Q_1;Q_2⟩\mid Q.1\mid Q.2.$$ Their complete projectibility rules are

$X:\sigma \in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢X\mathsf{projectible}$

$\mathrm{\Gamma }⊢v\mathsf{val}$

$\mathrm{\Gamma }⊢⟨c;v⟩\mathsf{projectible}$

$\mathrm{\Gamma }⊢Q_1\mathsf{projectible}$$\mathrm{\Gamma }⊢Q_2\mathsf{projectible}$

$\mathrm{\Gamma }⊢⟨Q_1;Q_2⟩\mathsf{projectible}$

$\mathrm{\Gamma }⊢Q\mathsf{projectible}$

$\mathrm{\Gamma }⊢Q.i\mathsf{projectible}$

Seals, annotated lets, functor abstractions, and applications are not paths in the generative system.

The selected module typing family is

$X:\sigma \in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢X:\sigma$

$\mathrm{\Gamma }⊢c::\kappa$$\mathrm{\Gamma }⊢e:\tau [c/u]$

$\mathrm{\Gamma }⊢⟨c;e⟩:\mathsf{B}(u::\mathsf{Sing}(c);\tau )$

$\mathrm{\Gamma }⊢M:{\sigma }_0$$\mathcal{D}::\mathrm{\Gamma }⊢{\sigma }_0{⪯}_{\mathsf{s}}\sigma$

$\mathrm{\Gamma }⊢M\upharpoonright \sigma :\sigma$

$\mathrm{\Gamma }⊢M:{\sigma }_1$$\mathcal{D}::\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2$

$\mathrm{\Gamma }⊢M:{\sigma }_2$

$\mathrm{\Gamma }⊢\sigma \mathsf{sig}$$\mathrm{\Gamma }⊢M_1:{\sigma }_1$$\mathrm{\Gamma },X:{\sigma }_1⊢M_2:\sigma$

$\mathrm{\Gamma }⊢(\mathsf{let}X=M_1\mathsf{in}{M}_2):\sigma$

$\mathrm{\Gamma }⊢M_1:{\sigma }_1$$\mathrm{\Gamma }⊢M_2:{\sigma }_2$

$\mathrm{\Gamma }⊢⟨M_1;M_2⟩:\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2$

$\mathrm{\Gamma }⊢M:\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2$

$\mathrm{\Gamma }⊢M.1:{\sigma }_1$

$\mathrm{\Gamma }⊢M:\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2$$X\notin \mathrm{FV}({\sigma }_2)$

$\mathrm{\Gamma }⊢M.2:{\sigma }_2$

$\mathrm{\Gamma }⊢Q\mathsf{projectible}$$\mathrm{\Gamma }⊢Q:\mathsf{B}(u::\kappa ;\tau )$

$\mathrm{\Gamma }⊢Q.s::\kappa$

$\mathrm{\Gamma }⊢M:\mathsf{B}(u::\kappa ;\tau )$$u\notin \mathrm{FV}(\tau )$

$\mathrm{\Gamma }⊢M.d:\tau$

$\mathrm{\Gamma }⊢Q:\mathsf{B}(u::\kappa ;\tau )$$\mathrm{\Gamma }⊢Q\mathsf{projectible}$

$\mathrm{\Gamma }⊢Q:\mathsf{B}(u::\mathsf{Sing}(Q.s);\tau )$

$\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$

$\mathrm{\Gamma }⊢Q:\mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2$

$\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$

$\mathrm{\Gamma }⊢Q:\mathsf{Sigma}{(}_{:}{\sigma }_1).{\sigma }_2^{\prime }$

$\mathrm{\Gamma },X:{\sigma }_1⊢M:{\sigma }_2$

$\mathrm{\Gamma }⊢\lambda X:{\sigma }_1.M:\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2$

$\mathrm{\Gamma }⊢F:\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2$$\mathrm{\Gamma }⊢A:{\sigma }_1$$X\notin \mathrm{FV}({\sigma }_2)$

$\mathrm{\Gamma }⊢F(A):{\sigma }_2$

Subkinding is ${⪯}_{\mathsf{k}}$, dynamic-type subtyping is , and subsignature matching is ${⪯}_{\mathsf{s}}$. Its structural rules are

$\mathrm{\Gamma }⊢\sigma \mathsf{sig}$

$\mathrm{\Gamma }⊢\sigma {⪯}_{\mathsf{s}}\sigma$

$\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2$$\mathrm{\Gamma }⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_3$

$\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_3$

$\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}$

$\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_2$

Its variance rules are

$\mathrm{\Gamma }⊢{\kappa }_1{⪯}_{\mathsf{k}}{\kappa }_2$

$\mathrm{\Gamma }⊢\mathsf{B}(u::{\kappa }_1;{\tau }_1){⪯}_{\mathsf{s}}\mathsf{B}(u::{\kappa }_2;{\tau }_2)$

$\mathrm{\Gamma }⊢{\sigma }_1{⪯}_{\mathsf{s}}{\sigma }_1^{\prime }$$\mathrm{\Gamma },X:{\sigma }_1⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_2^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2{⪯}_{\mathsf{s}}\mathsf{Sigma}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }$

$\mathrm{\Gamma }⊢{\sigma }_1^{\prime }{⪯}_{\mathsf{s}}{\sigma }_1$$\mathrm{\Gamma },X:{\sigma }_1^{\prime }⊢{\sigma }_2{⪯}_{\mathsf{s}}{\sigma }_2^{\prime }$

$\mathrm{\Gamma }⊢\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2{⪯}_{\mathsf{s}}\mathsf{Pi}(X:{\sigma }_1^{\prime }).{\sigma }_2^{\prime }$

Operational module values are $$V::=⟨c;v⟩\mid ⟨V_1;V_2⟩\mid \lambda X:\sigma .M.$$ Unlike the open judgment, this grammar has no variable case. Write $\mathsf{hsubst}(M;V;X)$ for substitution followed only by contraction of hierarchy projections exposed by substituting $V$, recursively along the original projection spine. It performs no seal, functor, or unrelated dynamic reduction. The sorted root contractions are The complete compatible-context family is

$R⟶R^{\prime }$

${\mathcal{E}}_M[R]⟶{\mathcal{E}}_M[R^{\prime }]$

$M⟶M^{\prime }$

$M.d⟶M^{\prime }.d$

$e⟶e^{\prime }$

$⟨c;e⟩⟶⟨c;e^{\prime }⟩$

Here No context crosses a functor or undischarged let body. Package elaboration is defined only for recursively elaboration-admissible derivations: every module-subderivation signature, every displayed matching endpoint, every opened signature, and the final result are closed-result. This includes the matching premises on Self-First and Self-Second. Matching nodes insert ${\mathsf{mcoe}}_{\mathcal{D}}$; module bindings first bind the translated computation to a fresh target variable and then apply ${\mathsf{Open}}_{\sigma }$, so no module computation is duplicated and no existential witness escapes. Rule Self repacks the unchanged witness at its singleton kind. Rules Self-First and Self-Second retranslate the refined component and pair it with the unchanged translated component; projectibility ensures that this duplication allocates no generative name.

The proof-relevant phase card imports no further rule into ${\mathrm{MLMod}}_0$. Its comparison uses ModTT dependent products over dynamic signatures, rather than adding an object-language arrow. The imported endpoint has closed families $\sigma ,\tau :\mathsf{Val}(\mathsf{type})\to \mathsf{Sig}$, an $\alpha$-small relation family on pairs of closed values, and the function of phase-separated sets stated in theorem 14.32.