Distributivity Subtyping
The distribution laws that let intersections be pushed through arrows and recursive binders. They are the declarative escape hatch that the algorithmic cover cannot mimic at coarse granularity.
The laws
- dist-arrow:
(Int→T1) & (Int→T2) ≡ Int → (T1 & T2)(a genuine equivalence). - dist-mu:
μa.(B1) & μa.(B2) <: μa.(B1 & B2)(forward), with the reverse holding only in the positive case.
The pivotal asymmetry (2026-05-31)
Splitting the target is always sound; positivity only governs completeness.
To prove A <: μ(S & T), split it: prove A <: μS and A <: μT, then
A <: μS & μT <: μ(S & T) by dist-mu forward, which always holds. Likewise
A <: Int→T1 and A <: Int→T2 give A <: (Int→T1)&(Int→T2) <: Int→(T1&T2) by dist-arrow forward.
The reverse direction (μ(S&T) <: μS & μT, the positive-only direction) is not needed for soundness — it is only needed to know the split did not discard a solution. So splitting is free for soundness; positivity merely decides whether a split is worth taking.
This reframes the whole positivity worry: you never need positivity to stay sound — only to decide completeness. It is the justification for Deep Target Splitting.
Why declarative beats the cover
The declarative system decouples covariant subsumption (A1<:T1, CLIMB) from rigid match (A2≈T2, RIGID) into separate dist-arrow / dist-mu steps. The cover, working at ordinary-leaf granularity, bundles them into one certificate — hence incompleteness.
Related
Weakly Positive Subtyping · Split-Cover and Polarity Certificates · Deep Target Splitting · Incompleteness of the Algorithmic Mu-Rule · project note Distributivity Subtyping, Kick-off prompts - Distributivity, Claude’s response on Recursive Distributivity