Algebraic subtyping and principal inference

The theorem owner is Dolan–Mycroft MLsub with polar schemes, guarded equi-recursive types, stable bisubstitutions, and type automata. Its inference is sound, complete, terminating, and principal at that signature.

${\mathsf{MLsub}}_0$ has four primitive rigid heads, lambda-lifted declarative typing, sorted decomposition, stable atomic actions, and its own finite polar automata. The local automaton proof gives terminating solution or exact failure in theorem 19.11; structural induction on the complete ${\mathsf{P}}_0$ equations gives sound, complete, principal inference in theorem 19.13. Principality is up to mutual scheme subsumption. No singleton-record embedding is used: in full MLsub the join of two records with distinct singleton labels is the empty record, whereas the corresponding join of two rigid ${\mathsf{MLsub}}_0$ atoms is not $\mathrm{\top }$.

The POPL paper’s Theorems 8–10 establish biunification solution/failure and automaton representation; Section 5.7 gives termination and the quadratic worst-case bound. The dissertation supplies the full principality development.

MLstruct+, MLstruct, Simple-sub, and semantic subtyping are distinct calculi. The MLstruct+ Boolean soundness/decision result does not transfer to MLsub, and MLsub principality does not transfer back.

artifacts/ch19-polar-biunification/ checks five finite decomposition cases and is not an MLsub implementation.