ch:ml-modules: ch:ml-modules
Problem, result, and invariant. Implement the finite matching and identity-allocation fragment used by the ordered-set hierarchy of chapter 12. The finished program must preserve a transparent All 9 ML-modules corpus cases passed.
Maintain two invariants. First, the second component of a hierarchy resolves FromFirst against the static identity recognized in the actual first component, never against a caller-supplied guess. Second, every generative operation consumes the current internal supply and returns its successor; client data cannot select or reuse an allocated stamp.
Representation. Use a datatype of identities with manifest constants, nominal stamps, and structural applicative paths. Keep static information separate: Hidden, Manifest id, and FromFirst. Signatures then have four constructors for ordered modules, sets, hierarchies, and functors. This representation makes identity comparison structural and keeps the dependent second-component check visible. Strings would shorten printing, but would move identity well-formedness into an unverified parser; hash-consed mutable nodes would obscure the fresh-supply invariant.
First complete version. Begin with ordered modules. Define equality on identities and a static match in which a hidden target accepts every actual identity and a manifest target requires equality. Check FromFirst must fail, because there is no enclosing hierarchy supplying the first identity.
Add hierarchies by matching their first components, extracting the manifest identity recognized there, and passing it only to the recursive match of the second components. This yields the first useful end-to-end program: the natural-number ordered-set hierarchy is accepted and its Boolean near miss is rejected. Compute the recursion budget from the sizes of both finite input trees. Every recursive call removes one hierarchy or functor layer, so this budget mirrors the printed structural argument without a fixed depth cutoff.
Generative and applicative cases. Represent the name supply by one natural number. Opaque sealing checks the visible interface, allocates StampId next, and returns next+1. Generative application performs the same allocation for its abstract result representation. Test each operation twice in sequence.
Only after these tests pass, add the separate applicative mode. Its result identity is AppId functorPath argumentPath, so repeating the same stable paths gives equality while changing either path does not. Do not reuse that identity in the generative branch: doing so would silently replace the chapter’s functor discipline.
For the finite elaboration observation, map a basic signature to an existential shape, a hierarchy to a product, and a functor to an arrow. This is a target-shape calculation, not a term elaborator or target typechecker.
A failing version. The tempting hierarchy matcher compares FromFirst with the wanted second component itself and therefore accepts the Boolean set. The input Hierarchy natOrder boolSet against the wanted shared hierarchy exposes the error. A second tempting bug returns the old supply after an opaque seal; the two-seal case then allocates the same stamp twice.
Acceptance test and boundary. Run the four commands recorded in appendix E. Require all nine named cases, an empty audit, and rejection of the three documented semantic mutations. The program illustrates the matching and fresh-identity mechanisms used by proposition 12.4, theorem 12.13. Running it proves neither theorem, the package-elaboration theorem, nor the representation-independence result; those remain mathematical obligations in the chapter.