Strict data rows, qualified inference, and evidence

Types contain $\mathsf{Nat}$, $\mathsf{Bool}$, $\mathsf{String}$, arrows, $\mathsf{Rec}(\rho )$, and $\mathsf{Var}(\rho )$. Rows are empty, variables, or finite extensions and are formed only when every label is unique. Qualified rank-one schemes quantify ordinary and row variables and carry normalized lacks predicates. Terms are the pure HM let-language plus fixed nullary constants, record empty/extension/selection/restriction, variant injection/embedding/case, and the derived update. Every source constructor is saturated. Source evaluation is left-to-right call by value on finite label maps and tagged payloads.

Row equality is generated only by exchange of adjacent distinct labels and is transported through types; it has no contraction equation. $P⊩\rho \mathrm{\backslash }\ell$ is symbolic entailment, whereas $G{\vDash }_{\mathsf{g}}P$ is ground semantic satisfaction. Every substitution is sorted and admissible $S:P\to Q$: it preserves strict formation and makes the substituted source predicates entailed by $Q$. This signature is not the scoped duplicate-label effect-row calculus of chapter 25 and inherits none of its equations or metatheorems.

Constrained insertion exposes one requested field and may create a fresh tail together with its new lacks obligation. The mutually recursive solver uses normalized predicates, sorted occurs-check elimination, rigid decomposition, insertion for extension equations, and a fixed left-to-right work-list order. Qualified W returns $(P,S,\tau )$, generalizes type and row variables only at let, retains predicates mentioning environment variables, and threads all solver and branch substitutions in the displayed order.

Formation/equality no-confusion, lacks conversion, admissible-substitution composition, qualified substitution, canonical forms, preservation, progress, and ground safety are proved in chapter 4. The insertion/solver pair is proved terminating, sound, complete, and principal, including failure completeness. Qualified W is proved sound and principal by factorization at exactly this strict-row signature.

Lacks derivations elaborate to affine offset expressions and the explicit target uses canonical label order, arrays, and integer tags. The target has a nullary empty-array rule and an explicit conversion rule equating exactly those types with the same recursively sorted canonical image. Type preservation and operational simulation are proved for the displayed source/target pair. Administrative coherence is claimed only for unambiguous interfaces $\mathrm{ftv}(P)\subseteq \mathrm{ftv}(\mathrm{\Gamma },\tau )$; ambiguous source typings remain safe but are not accepted by the evidence-passing compiler. The coherence result does not identify arbitrary target programs or import a general proof-irrelevance principle.

The pinned Kappa companion in artifacts/ch7-rows/ executes strict formation, lacks normalization, constrained insertion/solving, qualified W, record/variant evaluation, a principal-factor check, and duplicate-label/nonprincipal-naive failures. It uses object-language datatypes rather than Kappa’s own row feature and is not a proof of termination, principality, inference, or safety.

Width subtyping, dependent rows or records, scoped duplicate labels, effect-row handling, and implicit first-match lookup are not in this signature. Each requires its own equality, substitution, decidability/inference, and metatheorems.