Generative ML modules, sharing, and matching

The reduced PFPL calculus has basic signatures $\mathsf{B}(u::\kappa ;\tau )$, dependent hierarchies $\mathsf{Sigma}(X:{\sigma }_1).{\sigma }_2$, and functors $\mathsf{Pi}(X:{\sigma }_1).{\sigma }_2$. Values and projectible paths are distinct. Opaque seals and generative applications are not paths. Subkinding ${⪯}_{\mathsf{k}}$, type subtyping , and signature matching ${⪯}_{\mathsf{s}}$ are separate semantic relations.

Singleton self-recognition and the two hierarchy self-recognition rules propagate manifest constructor identities before a dependent second projection is formed. The exact preservation result is proposition 12.4.

Package elaboration applies only when its derivation is recursively admissible: every signature of a module subderivation, every displayed matching endpoint (including hierarchy self matches), every opened context signature, and the result are closed-result. Matching derivations induce explicit coercions. Module computations are bound once before scoped opening; the three self-recognition rules preserve or retranslate the same projectible witnesses. Supported target typing is theorem 12.7; derivation substitution and forward simulation/target safety are lemma 14.18, theorem 12.8. This is not a progress theorem for the source.

Counter representation independence is theorem 12.11. Principal signatures exist only for closed projectible paths whose dynamic core components have principal types; typing factorization yields theorem 12.13. Least signatures are unique up to mutual matching, not judgmental equality. Seals and generative applications lie outside this theorem.

The nested family in section 14.7 separates a static type component from dynamic pack/unpack module functors. An $\alpha$-small set-valued input witness is transformed pointwise by the round-trip functor while its static component is tracked. The general transport is imported at the exact Sterling–Harper boundary in theorem 14.32. ModTT’s static open, static extent, proof-relevant families, and model theory are not added to the reduced ML-module calculus, so no local theorem is strengthened.

Crary’s existential solution is the least avoiding supersignature and is scoped to his synthesis contexts. PFPL’s applicative alternative adds its separate projectibility/equality rules. Crary’s separate-compilation result and MixML’s recursive-mixin results remain theorem cards for those languages; none is transferred to the generative principal calculus.

The finite Kappa checker in appendix E observes sharing propagation, fresh opaque or generative identities, structural applicative identities, matching rejection, and target shapes. It proves none of the module metatheorems.