ch:hindley-milner: ch:hindley-milner

Problem and result. Implement the exact pure W signature of exercise 4.16: variables, unannotated lambdas, application, and nonrecursive let. The finished program is artifacts/ch04-hm/hm.kp. It prints five successful schemes, three ordinary unification boundaries, a named unifier replay, an open-context fresh-supply regression, and a capture-avoiding scheme-action regression.

Representation. Use the four datatypes HmType, HmTerm, HmScheme, and HmSubBinding. A scheme stores its quantified natural-number indices and its monotype body. A substitution is a list of one-variable bindings. The list order is semantic: applying [S,T] means applying $S$ first and $T$ second, matching $\tau [S;T]=(\tau [S])[T]$. Keeping this simple representation makes every printed proof invariant visible. A union–find representation would make unification faster, but would require a separate extraction pass to recover the chapter’s finite substitution and replay it on the original equations.

Stage 1: a variable–lambda vertical slice. Begin with only the variable and lambda constructors of HmTerm. Implement free-variable collection for types and schemes, scanning of an input context, prefix instantiation, and the variable and lambda clauses of W. The public wrapper starts above the greatest context index, retains the monotype returned by W, and generalizes it relative to the substituted final context. Run the complete wrapper immediately on $\lambda x.x$ and require the observable scheme $\mathrm{\forall }\alpha .\alpha \to \alpha$. This is the first end-to-end source–inference–scheme path; no unifier or let rule is needed for it.

Stage 2: substitution, unification, and application. Add one-variable action, left-to-right substitution action, and composition. Test composition on a type containing both a domain variable and a variable introduced by its image. Represent a unification problem as an ordered list of Equation nodes. Delete a reflexive head. Treat constructor–variable orientation as local preprocessing, then eliminate the variable or report the occurs failure. For equal constructors, prepend corresponding child equations in their original order; unequal heads report a constructor clash. After a successful named call, apply its result to the saved original list and require equationsReflexive. The implementation uses separate computed fuels for variable elimination, constructor decomposition, and deletion. Reaching an internal zero is an invariant failure, not an ordinary inference failure. Add W’s application clause and require $\lambda f.\lambda x.f(fx)$ to produce the expected scheme for $\mathsf{twice}$.

Stage 3: let, generalization, and the global supply. Add generalization and W’s let clause in that order. The definition is generalized relative to $\mathrm{\Gamma }[S_1]$, not the stale input context, and the body is called under the updated context. Scan both quantified prefixes and bodies of every input scheme before the first W call. Every W clause returns the unconsumed counter; application passes the counter from its function call to its argument call, and let passes the counter from the definition to the body. Do not restart a sibling. The open regression $$f:{\alpha }_0⊢\lambda x.f:\mathrm{\forall }{\alpha }_1.{\alpha }_1\to {\alpha }_0$$ distinguishes this implementation from one that always starts at zero. Then run the complete $\mathsf{twice}$-at-itself trace to exercise independent instantiation at let-bound uses.

Stage 4: capture avoidance, oracle, and regression report. For general scheme action, first collect every variable in the substitution domain and range. If that set meets the quantified prefix, alpha-rename the whole prefix above the maximum index occurring in either input, then apply the substitution with the fresh prefix removed from its domain. The regression $$(\mathrm{\forall }{\alpha }_1.{\alpha }_0)[{\alpha }_1/{\alpha }_0]{=}_{\alpha }\mathrm{\forall }{\alpha }_2.{\alpha }_1$$ kills the tempting implementation that merely removes ${\alpha }_1$ from the substitution domain. To compare schemes independently of printed names, rigidify the right-hand scheme’s prefix and match the left body against it using only the left prefix as flexible variables. Run that check in both directions. This decides mutual generality for the rank-one trees used by the corpus. It is an expected-answer oracle, not a proof that an inferred answer is principal.

Failure-directed tests. The self-application case kills an occurs-check mutant: if the guard is deleted, $\alpha \doteq \alpha \to \beta$ is accepted or the recursion invariant fails. The open-context case kills a reset-to-zero supply mutant. The range-collision case kills a domain-only scheme-action mutant. The constructor-clash case distinguishes rigid $\mathsf{List}$ and $\mathsf{Ref}$; the nested-pair case checks decomposition order and the saved-equation replay.

Expected boundary. The completed regression report contains five successful schemes, the occurs failure, constructor decomposition and clash, one saved-equation replay, the open-context supply case, and the range-collision scheme action. Appendix E records the repository locator, pinned toolchain, exact commands, accepted digest, and raw transcript; this tutorial records only the construction order and named mathematical outcomes.

Mathematical boundary. The replay checks only that named returned substitutions solve named finite problems; mutual generality checks only the named expected schemes. The runs do not prove unifier completeness, inference soundness, or the protected principal-pair theorem. The list and reference extensions in the chapter are mathematical extensions and are deliberately outside this executable’s pure signature.