Hindley–Milner polymorphism and principal inference

Pure rank-one HM has variables, unannotated abstraction, application, and nonrecursive let. Monotypes are finite trees over type variables and a fixed constructor signature; schemes have only an outer universal prefix. Instantiation may occur at variable use, while declarative Gen may close any derivable scheme judgment whose variable is absent from the context. W performs deterministic contextual generalization at a nonrecursive let and when its final monotype is presented as a scheme. The list extension adds one unary type constructor, nil, cons, and one saturated two-branch case. The state extension separately adds $\mathsf{Unit}$, $\mathsf{Ref}$, locations, allocation, dereference, and assignment, and replaces unrestricted let generalization by the displayed conservative generalizable-form restriction. The named signature ${\mathcal{L}}_{\mathsf{ref}}$ contains the reference delta without lists; ${\mathcal{L}}_{\mathsf{list}\mathsf{+}\mathsf{ref}}$ is its cumulative extension by the complete list constructor, case, W, and run-time clauses. There is no recursion, polymorphic recursion, higher-rank parameter, impredicative instantiation, subtyping, row polymorphism, or effect system.

Monotypes are finite trees. Scheme prefixes are considered up to renaming. Generality is inclusion of monotype-instance sets. The printed unifier consumes an ordered equation list by Done, Delete, Orient, Eliminate with occurs check, and left-to-right constructor Decompose. Algorithm W consumes one monotone fresh-variable supply and threads substitutions in the printed left-to-right order. The constraint-generation calculation of section 3.3 is a batch teaching judgment and is not identified with W’s incremental trace.

Weakening and term/type substitution, unifier termination, soundness, completeness, and most-generality, agreement of declarative and syntax-directed typing, W soundness, the protected principal-pair induction, principal schemes over closed contexts, and adequacy of the checked evidence core for successful W results are proved in chapter 3. For the reference extension, store weakening, preservation, progress, and safety are proved only with the displayed value restriction and with generalization relative to both the term context and store typing. No normalization theorem for the effectful language is claimed.

The pinned Kappa companion in artifacts/ch04-hm/ executes the substitution-based unifier and Algorithm W on five principal schemes, an occurs-check failure, constructor decomposition, a constructor clash, a unifier replay, an open-context supply regression, and a capture-avoiding scheme-action regression. It is implementation evidence, not a proof of MGU completeness, W soundness, or principality.