ch:row-polymorphism: ch:row-polymorphism

Abbreviate the three field types by $H=\mathsf{String}$, $N=\mathsf{Nat}$, and $B=\mathsf{Bool}$. The original row already has $\mathsf{host}$ first: $$\{\mathsf{host}:H,\mathsf{port}:N,\mathsf{secure}:B\mid \xi \}.$$ One adjacent exchange puts $\mathsf{port}$ first: $$\{\mathsf{host}:H,\mathsf{port}:N,\mathsf{secure}:B\mid \xi \}{=}_{\mathsf{r}}\{\mathsf{port}:N,\mathsf{host}:H,\mathsf{secure}:B\mid \xi \}.$$ To put $\mathsf{secure}$ first, move it left twice: Every exchange is between distinct labels. The assumptions that $\xi$ lacks all three labels rebuild the Row-Ext premises on both sides of each exchange, so these raw equalities are equalities under $P$.

If the last label is another $\mathsf{port}$, formation already fails. After forming the inner row $\{\mathsf{port}:N\mid \xi \}$, adding the outer $\mathsf{port}$ would require $$P⊩\{\mathsf{port}:N\mid \xi \}\mathrm{\backslash }\mathsf{port}.$$ Predicate simplification reaches $\mathrm{\perp }$ at the displayed matching head. Consequently there is no strict row on which the proposed exchange calculation could begin.

Let $$e:\alpha ,r:\mathsf{Rec}(\{\ell :\beta \mid \xi \}),P=\{\xi \mathrm{\backslash }\ell \}.$$ The update abbreviation expands as $$\{\ell :=e\mid r\}=\{\ell =e\mid r-\ell \}.$$ Rule Q-Restrict removes the exposed field and preserves the single tail: $$r-\ell :\mathsf{Rec}(\xi ).$$ Rule Q-Extend then combines $e:\alpha$ with that residual record: $$\{\ell =e\mid r-\ell \}:\mathsf{Rec}(\{\ell :\alpha \mid \xi \}).$$ Its only new premise is $P⊩\xi \mathrm{\backslash }\ell$. The same predicate is also exactly the premise that forms the input row $\{\ell :\beta \mid \xi \}$ and the output row $\{\ell :\alpha \mid \xi \}$.

Abstracting the two term variables and generalizing gives $$\mathrm{\forall }\alpha \mathrm{\forall }\beta \mathrm{\forall }\xi .(\xi \mathrm{\backslash }\ell )\Rightarrow \alpha \to \mathsf{Rec}(\{\ell :\beta \mid \xi \})\to \mathsf{Rec}(\{\ell :\alpha \mid \xi \}).$$ The same $\xi$ at all three stages expresses preservation of every untouched field.

Put $$\rho =\{\mathsf{error}:\mathsf{String}\mid \xi \}.$$ The assumptions on $\xi$ imply $P⊩\rho \mathrm{\backslash }\mathsf{ok}$, because $\mathsf{error}\ne \mathsf{ok}$. The required term is The scrutinee has type $\mathsf{Var}(\{\mathsf{ok}:\alpha \mid \rho \})$. In the matching branch, $x:\alpha$, hence $fx:\beta$. Choose residual row $\rho$ in Q-Inject; its lacks premise gives $$⟨\mathsf{ok}=fx⟩:\mathsf{Var}(\{\mathsf{ok}:\beta \mid \rho \}).$$ In the residual branch, $y:\mathsf{Var}(\rho )$. Rule Q-Embed chooses the fresh alternative type to be $\beta$ and gives $${\mathsf{embed}}_{\mathsf{ok}}y:\mathsf{Var}(\{\mathsf{ok}:\beta \mid \rho \}).$$ Both branches therefore have the same result type. Expanding $\rho$ gives exactly $$\mathsf{Var}(\{\mathsf{ok}:\beta ,\mathsf{error}:\mathsf{String}\mid \xi \}).$$ Only the $\mathsf{ok}$ payload passes through $f$; every other tag enters the residual branch and is embedded unchanged.

Suppose the lookup has been typed, after any final row conversion, as $$\cdot {⊢}_q\{m=w\mid R\}.\ell :\varnothing \Rightarrow \tau .$$ Inverting Q-Select gives a closed strict row $\rho$ with $$\cdot {⊢}_q\{m=w\mid R\}:\varnothing \Rightarrow \mathsf{Rec}(\rho ),\rho \equiv \{\ell :\tau \mid {\rho }_{\ell }\}.$$ Peeling the record value at its run-time head gives a type $\upsilon$ and a row ${\rho }_0$ such that $$\rho \equiv \{m:\upsilon \mid {\rho }_0\},\cdot {⊢}_{q}w:\varnothing \Rightarrow \upsilon ,\cdot {⊢}_{q}R:\varnothing \Rightarrow \mathsf{Rec}({\rho }_0).$$ Thus ${\rho }_0\equiv \rho -m$.

Because $m\ne \ell$, deleting $m$ does not remove the $\ell$ field. Deletion commutation gives $$(\rho -m)-\ell \equiv (\rho -\ell )-m.$$ Equivalently, the finite-map characterization exposes $${\rho }_0\equiv \{\ell :\tau \mid (\rho -\ell )-m\}.$$ Convert the typing of $R$ along this equality and apply Q-Select: $$\cdot {⊢}_{q}R.\ell :\varnothing \Rightarrow \tau .$$ This is exactly the type of the source redex, so the primitive reduction $$\{m=w\mid R\}.\ell ⟶R.\ell$$ preserves $\tau$.

Write the displayed rows with their tails exposed. Their formation needs $$P_0=\{\xi \mathrm{\backslash }\mathsf{x},\xi \mathrm{\backslash }\mathsf{y},\zeta \mathrm{\backslash }\mathsf{x},\zeta \mathrm{\backslash }\mathsf{z}\}.$$ Insertion first exposes the $\mathsf{x}$ field on the right, passing the distinct $\mathsf{z}$ field. It unifies $\alpha$ with $\mathsf{Nat}$ and leaves $$\{\mathsf{y}:\mathsf{Bool}\mid \xi \}\doteq \{\mathsf{z}:\mathsf{String}\mid \zeta \}.$$ To expose $\mathsf{y}$ on the right, insertion reaches the open tail $\zeta$. Choose fresh $\eta$ and put $\zeta =\{\mathsf{y}:\mathsf{Bool}\mid \eta \}$, generating the strictness requirement $\eta \mathrm{\backslash }\mathsf{y}$. Deleting the exposed field leaves $\{\mathsf{z}:\mathsf{String}\mid \eta \}$, so the final tail equation sets $\xi =\{\mathsf{z}:\mathsf{String}\mid \eta \}$. Thus one printed MGU is $$U=[\mathsf{Nat}/\alpha ,\{\mathsf{z}:\mathsf{String}\mid \eta \}/\xi ,\{\mathsf{y}:\mathsf{Bool}\mid \eta \}/\zeta ],$$ and normalization of $P_0[U]$ gives $$Q=\{\eta \mathrm{\backslash }\mathsf{x},\eta \mathrm{\backslash }\mathsf{y},\eta \mathrm{\backslash }\mathsf{z}\}.$$ For the two additional predicates, $$\xi [U]\mathrm{\backslash }\mathsf{z}=\{\mathsf{z}:\mathsf{String}\mid \eta \}\mathrm{\backslash }\mathsf{z}\Downarrow \mathrm{\perp },\zeta [U]\mathrm{\backslash }\mathsf{y}\Downarrow \mathrm{\perp }.$$ Hence the equation problem has the displayed MGU, but the problem augmented by either requested predicate has no admissible solution.

Give $x$ fresh type $\alpha$. Injection chooses fresh $\xi$ and returns $$\{\xi \mathrm{\backslash }\mathsf{ok}\},\mathsf{Var}(\{\mathsf{ok}:\alpha \mid \xi \}).$$ For embedding, choose a fresh type $\beta$ for the new $\mathsf{error}$ alternative and a fresh row variable $\zeta$ for the old row. Solving $$\mathsf{Var}(\{\mathsf{ok}:\alpha \mid \xi \})\doteq \mathsf{Var}(\zeta )$$ sets $\zeta =\{\mathsf{ok}:\alpha \mid \xi \}$. Its new requirement $\zeta \mathrm{\backslash }\mathsf{error}$ normalizes to $\xi \mathrm{\backslash }\mathsf{error}$. Lambda formation and generalization give $$\mathrm{\forall }\alpha \beta \xi .(\xi \mathrm{\backslash }\mathsf{ok},\xi \mathrm{\backslash }\mathsf{error})\Rightarrow \alpha \to \mathsf{Var}(\{\mathsf{error}:\beta ,\mathsf{ok}:\alpha \mid \xi \}).$$ If $\xi$ contained $\mathsf{ok}$, injection would duplicate its selected alternative; if it contained $\mathsf{error}$, embedding would duplicate the newly added alternative. The two residual predicates are therefore independent and both necessary.

In the first row, only $\mathsf{host}$ is smaller than $\mathsf{ok}$, so the offset is $1$. In the second, only $\mathsf{error}$ is smaller than $\mathsf{host}$, so that offset is also $1$. These counts are unchanged if the two fields are displayed in the opposite syntactic order.

An $\mathsf{ok}$ injection into the one-alternative row has tag $0$. Embedding it past a new $\mathsf{host}$ alternative inserts a smaller label, so evidence increments the tag to $1$. Embedding the result past $\mathsf{error}$ inserts another smaller label and increments it to $2$. The payload never changes; only its position in the canonical ordered sum does.

Let $$A=\{\mathsf{host}:\mathsf{String},\mathsf{port}:\mathsf{Nat},\mathsf{secure}:\mathsf{Bool}\},B=\{\mathsf{port}:\mathsf{Nat}\}.$$ Since the label set of $B$ is contained in that of $A$, Width derives . From $r:A$, Sub gives $r:B$. With $\mathsf{portOf}:B\to \mathsf{Nat}$, application yields $$\mathsf{portOf}r:\mathsf{Nat}.$$

For the row-polymorphic derivation, instantiate $$\mathsf{portOf}:\mathrm{\forall }\alpha \xi .(\xi \mathrm{\backslash }\mathsf{port})\Rightarrow \mathsf{Rec}(\{\mathsf{port}:\alpha \mid \xi \})\to \alpha$$ by $$\alpha =\mathsf{Nat},\xi =\{\mathsf{host}:\mathsf{String},\mathsf{secure}:\mathsf{Bool}\}.$$ The chosen row lacks $\mathsf{port}$ by two unequal-head reductions followed by L-Empty. Row permutation identifies the instantiated domain with $\mathsf{Rec}(A)$, so the application again has type $\mathsf{Nat}$.

Width subtyping may discard the $\mathsf{host}$ and $\mathsf{secure}$ fields when it views $A$ as $B$. A fixed result type for adding $\mathsf{timeout}$ can mention the fields retained in $B$, but contains no variable linked to all the fields forgotten by subsumption. It therefore cannot prove that those arbitrary fields survive. A row type can express that link: $$\mathrm{\forall }\xi .(\xi \mathrm{\backslash }\mathsf{timeout})\Rightarrow \mathsf{Rec}(\xi )\to \mathsf{Rec}(\{\mathsf{timeout}:\tau \mid \xi \}).$$ The same $\xi$ in domain and codomain preserves all three input fields in this instance.

The principal declaration is $$\mathsf{withSecure}:\mathrm{\forall }\xi .(\xi \mathrm{\backslash }\mathsf{secure})\Rightarrow \mathsf{Rec}(\xi )\to \mathsf{Rec}(\{\mathsf{secure}:\mathsf{Bool}\mid \xi \}).$$ Set $\xi [G]=\{\mathsf{host}:\mathsf{String}\}$. Its predicate discharges by $$\{\mathsf{host}:\mathsf{String}\}\mathrm{\backslash }\mathsf{secure}\Downarrow {ϵ}_{\rho }\mathrm{\backslash }\mathsf{secure}\Downarrow \mathrm{\top }.$$ Ground discharge therefore gives The argument is typed by Q-Empty, Q-Const, and Q-Extend: Application is therefore ground typed at the displayed result record type. Its reduction is

Now try a ground row containing $\mathsf{secure}:\mathsf{Nat}$, for example $$\xi [G^{\prime }]=\{\mathsf{host}:\mathsf{String},\mathsf{secure}:\mathsf{Nat}\}.$$ Normalization of the required predicate first passes the unequal $\mathsf{host}$ head and then reaches the matching one: Hence $G^{\prime }$ is not admissible and there is no corresponding ground instantiation or application typing.

Because $(V,Q_V)$ is a solution of the original problem, principality of $(U,Q_U)$ supplies an admissible $R:Q_U\to Q_V$ such that $V{\equiv }_{Q_V}U;R$ on every problem variable. Interchanging the two solutions supplies an admissible $S:Q_V\to Q_U$ with $U{\equiv }_{Q_U}V;S$. Literal equality is neither needed nor generally true: row permutation and the names chosen for fresh tails are invisible to the equation problem.

For example, solve $$\{\mathsf{x}:\mathsf{Nat}\mid \xi \}\doteq \{\mathsf{y}:\mathsf{Bool}\mid \zeta \}$$ under the two input strictness predicates. One run gives $$\xi [U]=\{\mathsf{y}:\mathsf{Bool}\mid \omega \},\zeta [U]=\{\mathsf{x}:\mathsf{Nat}\mid \omega \},Q_U=\{\omega \mathrm{\backslash }\mathsf{x},\omega \mathrm{\backslash }\mathsf{y}\}.$$ Applying $U$ to the two original rows displays the same finite map in different orders: $$\{\mathsf{x}:\mathsf{Nat},\mathsf{y}:\mathsf{Bool}\mid \omega \}{\equiv }_{Q_U}\{\mathsf{y}:\mathsf{Bool},\mathsf{x}:\mathsf{Nat}\mid \omega \}.$$ The adjacent exchange is legal because $\mathsf{x}\ne \mathsf{y}$; the two predicates in $Q_U$ form both displays strictly. A run that chooses $\nu$ instead gives the analogous $(V,Q_V)$; it may also print the two substitutions and predicates in the opposite order. Define $\omega [R]=\nu$ and $\nu [S]=\omega$, acting identically elsewhere. Both are admissible, and the two displayed factorization equations hold modulo their target predicate contexts. Thus the fresh names and print orders differ while the principal solution does not.

Give the new values types $\alpha$ and $\beta$, the old $\ell$ and $m$ fields types $\gamma$ and $\delta$, and let the remaining row be $\xi$. Take $$P=\{\xi \mathrm{\backslash }\ell ,\xi \mathrm{\backslash }m\},\ell \ne m.$$ The principal scheme is

For the inner update, first permute the input to expose $m$: $$\mathsf{Rec}(\{\ell :\gamma ,m:\delta \mid \xi \})\equiv \mathsf{Rec}(\{m:\delta ,\ell :\gamma \mid \xi \}).$$ Restriction and extension calculate The extension premise reduces to $P⊩\{\ell :\gamma \mid \xi \}\mathrm{\backslash }m$, which follows from $\xi \mathrm{\backslash }m$ and $\ell \ne m$.

For the outer update, permute the intermediate row to expose $\ell$: $$\{m:\beta ,\ell :\gamma \mid \xi \}\equiv \{\ell :\gamma ,m:\beta \mid \xi \}.$$ Then This extension uses the other predicate, $\xi \mathrm{\backslash }\ell$.

Reversing the updates produces the displayed result row $\{m:\beta ,\ell :\alpha \mid \xi \}$, which is equal to the former result by one adjacent exchange. Operationally each restriction removes one distinct field and each extension restores it with its new value. Since $\ell \ne m$, the two operations affect disjoint map entries; the final finite maps are identical even if the record spines display the fields in different orders.

In the scoped-duplicate record fragment, row and term formation admit repeated labels, record values retain repeated fields, and the operational rules for selection and restriction stop at the first displayed matching field. Equality may exchange adjacent distinct labels, but it never exchanges two equal labels. Consequently the relative order of the occurrences of any one label is invariant.

The sentence in the original canonical-forms proof that fails is the claim that the satisfied lacks predicate makes the new label absent and hence that extension creates exactly the finite map of the extended row. There is no lacks premise in the new calculus, and a value may contain several entries with the same label, so it is not a finite map from labels to values.

The repaired record canonical-form statement is this: if a closed value has a scoped-duplicate record row, then for each label it contains exactly the same ordered sequence of occurrences as the row. The payloads at those occurrences have the corresponding field types. Selection returns the payload at the first occurrence, and restriction removes that occurrence while preserving the order and types of all later occurrences. The proof is induction on the displayed record spine. Extension adds one leading occurrence; an exchange of distinct labels changes no same-label sequence.

This statement does not by itself justify an update notation containing an unqualified $\rho -\ell$. When $\rho$ contains several $\ell$ occurrences, deleting the first, the last, or another occurrence gives different residual rows, often with different next selected types; equal labels cannot be exchanged to identify those results. The update equation becomes sound only after restriction is specified to remove the first displayed occurrence. Then extension installs the replacement as the new first occurrence and leaves all later occurrences available. No claim about variants follows: their run-time tags would additionally need to record the nesting level of equal labels.

Every ground instance of $$\mathrm{\forall }\xi .(\xi \mathrm{\backslash }\ell )\Rightarrow \mathsf{Nat}$$ has result type $\mathsf{Nat}$. Its evidence argument nevertheless depends on the chosen row. If $\xi ={ϵ}_{\rho }$, the canonical offset is $0$. If $\xi =\{m:A\}$ with , the canonical offset is $1$. Thus the target scheme abstraction is applied to certificates describing different layouts, even though neither layout variable occurs in the visible result type.

For an open judgment the usual condition is $$\mathrm{ftv}(P)\subseteq \mathrm{ftv}(\mathrm{\Gamma },\tau );$$ for a closed scheme it is $$\mathrm{ftv}(P)\subseteq \mathrm{ftv}(\tau ).$$ The displayed scheme violates the second condition because $\xi$ occurs in $P$ but not in $\mathsf{Nat}$.

Run W on the case term. Injection first returns $$P_0=\{{\xi }_0\mathrm{\backslash }\ell \},S_0=\mathrm{id},{\tau }_0=\mathsf{Var}(\{\ell :\mathsf{Nat}\mid {\xi }_0\}),$$ with fresh ${\xi }_0$. The case clause chooses fresh $\alpha ,{\xi }_1$ and solves $$\mathsf{Var}(\{\ell :\mathsf{Nat}\mid {\xi }_0\})\doteq \mathsf{Var}(\{\ell :\alpha \mid {\xi }_1\}).$$ Its principal solution follows the solver’s fixed left-variable orientation: $\alpha =\mathsf{Nat}$ and ${\xi }_0={\xi }_1$, retaining $Q_0=\{{\xi }_1\mathrm{\backslash }\ell \}$. The matching branch has $x:\mathsf{Nat}$ and returns $\mathsf{zero}:\mathsf{Nat}$. The residual branch has $y:\mathsf{Var}({\xi }_1)$ and returns the same type. The final branch equation is the reflexive equation $\mathsf{Nat}\doteq \mathsf{Nat}$, so W returns $$(\{{\xi }_1\mathrm{\backslash }\ell \},U_0,\mathsf{Nat}).$$ After closed generalization, its scheme is precisely of the ambiguous form above.

One repair is to reject a principal inference result when definition 7.53 fails; this is the policy selected by the main evidence-passing compiler. A different language could default every hidden row to a documented ground row, for example ${ϵ}_{\rho }$, and consequently pass offset $0$. That choice is deterministic but discards the ambiguous row polymorphism, so it must be part of the language specification rather than an unstated elaboration step.