ch:disjoint-intersections: ch:disjoint-intersections

Problem, result, and invariant. Implement the chapter’s top-free structural disjointness calculation, source subtyping rules, merge formation, and ordinary-demand contributor selection. The observable result is eight named cases plus the final count in appendix E. The maintained invariant is that an accepted merge has at most one contributor to any ordinary demanded type.

Representation. Represent $\mathsf{Int}$, arrows, products, and intersections by a nominal recursive Ty; represent contributor outcomes by a separate four-case datatype. This makes ambiguity an inspectable result. Using Kappa intersection types would be shorter, but would test Kappa’s type relation rather than the printed source calculus. A Boolean-only contributor function would erase which projection was selected and could not expose coherence failure.

First complete version. Begin with structural type equality and the two ordinary-head cases. Add intersection distribution, then arrow-result recursion and product-coordinate disjunction. Implement subtyping separately: decompose a demanded intersection first; for an ordinary demand, project from an offered intersection; compare arrow domains contravariantly and results covariantly; compare products componentwise. Form a merge only after disjointness succeeds. On , ask separately for an integer and an integer function. The first end-to-end run must return left and right contributors, never ambiguity.

Remaining cases. Add the equal-integer rejection, arrows with distinct and equal results, and products separated in one coordinate. Demand $\mathsf{Int}\times \mathsf{Int}$ from a left branch of type ; full subtyping must select that branch even though the two types are not syntactically equal. Finally disable only merge disjointness, offer integer values $1,2$, and apply both contributor choices to the same pair. Observe $\mathsf{Projected}1$ and $\mathsf{Projected}2$. This models the two target projections rather than treating $1\ne 2$ itself as the counterexample.

A failing version. Classify arrows by their domains. The mutant accepts arrows with disjoint domains but a shared integer result, even though their raw common supertype is . The named arrow case fails. Alternatively, delete either intersection-distribution call; a nested common demand then escapes contributor detection.

Acceptance test. Run check, test, run, and audit as recorded in appendix E. Require all eight named PASS lines, the exact final count, and audit output []. Confirm that the counterexample computes both projection observations. Derive recursion fuel from the two input-tree sizes; the fuel is an executable termination measure, not evidence about disjointness in the mathematical calculus.

Mathematical boundary. The artifact executes finite cases of disjointness, subtyping, merge formation, and contributor choice. It provides no proof of completeness, uniqueness, preservation, coherence, or safety.