Chapter 7Core route

Row Polymorphism and Extensible Records and Variants

A record is a finite collection of values tagged by distinct names, called labels; its field at label $ℓ$ is retrieved by the selector $r . ℓ$ . Mathematically, a closed record is an element of the finite indexed product of its field types: it chooses one value at every label. A variant instead chooses one label and one value of the type associated with that label. The corresponding sum of alternatives is called the indexed coproduct of the field types. A row is the finite partial map from labels to component types that indexes either construction.

A record selector is easy to type when the whole record is known. For example, $λ r . r . port : Rec ({host : String, port : Nat}) \to Nat .$ But this type fixes something that the program does not use: the selector works just as well when the record has a timeout, a log handle, or fifty other fields. Repeating one type for every possible remainder is not a solution, and ordinary Hindley–Milner substitutions replace type variables by types, not by rows of fields.

Extension makes the obstruction sharper. We want one principal type for $withSecure : = λ r . {secure = true ∣ r},$ and we want the result to retain every field of $r$ . A type variable for the entire argument loses those fields; a fixed record type chooses them in advance. The missing object is a variable ranging over the row of untouched fields.

The same objects occur outside software records. A measurement result can be a record of named channels, while a tagged experimental outcome is a variant; row polymorphism lets a calculation mention the channels or outcomes it uses while remaining uniform in the unmentioned part of the index family.

Rows are finite maps: each label occurs at most once, and field order is irrelevant. The judgment $ρ \ ℓ$ proves that extending $ρ$ at $ℓ$ preserves this invariant. Rows with duplicate labels and first-match selection obey a different equality.

Rows and the strictness invariant

Fix a countably infinite set of labels. Labels are written $ℓ, m, n$ ; names such as $host$ and $port$ are particular labels. Type variables $α, β, \dots$ and row variables $ξ, ζ, \dots$ are disjoint countable supplies.

Definition 4.1 — Types, rows, and lacks predicates ¶

Types and rows are formed simultaneously by $\begin{aligned} τ & ::= α ∣ Nat ∣ Bool ∣ String ∣ τ \to τ ∣ Rec (ρ) ∣ Var (ρ), \\ ρ & ::= ξ ∣ ϵ_{ρ} ∣ {ℓ : τ ∣ ρ} . \end{aligned}$ Here $ϵ_{ρ}$ is the empty row. A lacks predicate is $ρ \ ℓ$ , read as the assertion that row $ρ$ lacks label $ℓ$ . The backslash is a relation between a row and a label, not row subtraction or set difference. A finite set of predicates is denoted $P$ . Type substitutions send type variables to types and row variables to rows, and act structurally on both sorts and on predicates. A row substitution is allowed only when it sends every assumed lacks fact to a true lacks fact; otherwise substitution could create a duplicate label.

Referenced from 5 locations

The four operations that later share a minus-like glyph have different input and output sorts: $\begin{array}{cl} ρ \ ℓ & lacks proposition \\ ρ - ℓ & metalevel deletion from a finite row \\ ρ^{-} & residual row returned by constrained insertion \\ e - ℓ & source term restricting a record . \end{array}$

The braces in ${ℓ : τ ∣ ρ}$ construct a row, not a record type; $Rec$ and $Var$ turn the same row into a record type and a variant type. Thus $Var$ abbreviates variant; it never denotes a term or row variable. For a closed row $ρ$ , these types denote respectively the indexed product and indexed coproduct over $dom (ρ)$ . We abbreviate nested extensions by $\begin{aligned} {ℓ_{1} : τ_{1}, \dots, ℓ_{k} : τ_{k} ∣ ρ}, \\ {ℓ_{1} : τ_{1}, \dots, ℓ_{k} : τ_{k}} : = {ℓ_{1} : τ_{1}, \dots, ℓ_{k} : τ_{k} ∣ ϵ_{ρ}} . \end{aligned}$

The grammar alone permits ${ℓ : τ, ℓ : υ ∣ ρ}$ . The formation judgment now excludes it.

Definition 4.2 — Constraint entailment and strict formation ¶

The function $simp$ scans a row until it finds $ℓ$ , reaches the empty row, or reaches an open tail. It is defined by structural recursion on the row argument: $\begin{aligned} simp (ϵ_{ρ} \ ℓ) & = ⊤, \\ simp ({m : τ ∣ ρ} \ ℓ) & = simp (ρ \ ℓ) & (m \neq ℓ), \\ simp ({ℓ : τ ∣ ρ} \ ℓ) & = ⊥, \\ simp (ξ \ ℓ) & = ξ \ ℓ . \end{aligned}$ The row-variable clause returns a normal form; $simp$ is a total function, not a term-reduction relation. For a set, apply it to every predicate, discard $⊤$ , fail at $⊥$ , and remove duplicates. Write $nf (P)$ for the resulting set. A predicate context is always normalized: every member therefore has form $ξ \ ℓ$ . In particular it is satisfiable, by sending every row variable to $ϵ_{ρ}$ . For example, $simp ({host : String ∣ ξ} \ port) = ξ \ port .$ For a one-predicate calculation, write $p ⇓ q$ when $simp (p) = q$ .

For normalized $P$ , the entailment $P ⊩ ρ \ ℓ$ is generated by

ξ \ ℓ \in P

P ⊩ ξ \ ℓ

L-Assume

P ⊩ ϵ_{ρ} \ ℓ

L-Empty

P ⊩ ρ \ ℓ

m \neq ℓ

P ⊩ {m : τ ∣ ρ} \ ℓ

L-Extend

For normalized predicate contexts, write $Q ⊩ P$ when $Q$ entails every predicate in $P$ .

Referenced from 6 locations

For example, the two rule applications needed to pass a displayed field distinct from the requested label are $\frac{\begin{matrix} \frac{ξ \ port \in P}{P ⊩ ξ \ port} L - Assume \\ host \neq port \end{matrix}}{P ⊩ {host : String ∣ ξ} \ port} L - Extend .$

Definition 7.3 — Admissible substitution ¶

An admissible substitution $S : P \to Q$ is a finite, sort-preserving substitution for which every nonidentity type image is a $Q$ -formed type, every nonidentity row image is a $Q$ -formed strict row, $nf (P [S])$ exists, and $Q ⊩ nf (P [S])$ . Thus the target may contain more information than substitution alone produces, but it may not license an ill-formed image. All substitution statements below use admissible substitutions; an attempted substitution whose normalized context is $⊥$ is rejected rather than treated as a map of strict rows. The notation $S : P \to Q$ records the source and target predicate contexts of the substitution. It is not a function type inside the object language.

Referenced from 5 locations

Definition 7.4 — Strict formation ¶

Write $P ⊢ ρ row$ for strict row formation. The empty row and every row variable are rows. Type variables and the three base types are types; arrows are formed componentwise. The row-specific rules are

P ⊢ ξ row

Row-Var

P ⊢ ϵ_{ρ} row

Row-Empty

P ⊢ ρ row

P ⊢ τ type

P ⊩ ρ \ ℓ

P ⊢ {ℓ : τ ∣ ρ} row

Row-Ext

The remaining type-formation rules are $\begin{matrix} \frac{\begin{matrix} P ⊢ τ type \\ P ⊢ υ type \end{matrix}}{P ⊢ τ \to υ type} Ty - Arrow \\ \frac{P ⊢ ρ row}{P ⊢ Rec (ρ) type} Ty - Record \frac{P ⊢ ρ row}{P ⊢ Var (ρ) type} Ty - Variant . \end{matrix}$

Referenced from 3 locations

The definitions are well founded. Simplification and lacks entailment recurse on the row tail; strict formation also recurses on a smaller tail and uses, but never defines, lacks entailment.

For example, $ξ \ port ⊩ {host : String ∣ ξ} \ port,$ because the assumption is the tail judgment $ξ \ port$ and $host \neq port$ is the side condition of L-Extend. Hence $ξ \ port ⊢ {port : Nat, host : String ∣ ξ} row .$ By contrast, formation of ${port : Bool, port : Nat ∣ ξ}$ would require a derivation of ${port : Nat ∣ ξ} \ port$ , and no rule can produce one.

Rows are unordered, but only distinct labels may pass one another.

Definition 4.3 — Row equality ¶

Row equality $=_{r}$ on types and rows is the least two-sorted congruence containing ${ℓ : τ, m : υ ∣ ρ} =_{r} {m : υ, ℓ : τ ∣ ρ} (ℓ \neq m),$ without a formation side condition. Under a predicate context $P$ , write $a \equiv_{P} a^{'}$ when both expressions have the same sort, are well formed under $P$ , and $a =_{r} a^{'}$ . Thus row equality permutes distinct fields, and type equality transports those permutations through $Rec$ , $Var$ , arrows, and field types.

Referenced from 4 locations

Lemma 7.6 — Formation and constructor separation ¶

If $a$ is a type or row formed under $P$ and $a =_{r} a^{'}$ , then $a^{'}$ is formed under $P$ . More precisely, the raw equality can be represented by a finite chain of adjacent exchanges in constructor contexts, and every expression in that chain is formed under $P$ .
Type equality preserves and reflects outer constructors. In particular, $\begin{aligned} τ_{1} \to τ_{2} \equiv_{P} υ_{1} \to υ_{2} & ⟹ τ_{1} \equiv_{P} υ_{1} and τ_{2} \equiv_{P} υ_{2}, \\ Rec (ρ) \equiv_{P} Rec (ρ^{'}) & ⟹ ρ \equiv_{P} ρ^{'}, \\ Var (ρ) \equiv_{P} Var (ρ^{'}) & ⟹ ρ \equiv_{P} ρ^{'} . \end{aligned}$ No arrow, record, variant, base type, or type variable is equal to a type with another outer constructor; equal base types and type variables are identical.

Referenced from 5 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.6 — Formation and constructor separation

Proof. Flatten a raw-equality derivation into a chain. Reflexivity gives the empty chain, symmetry reverses a chain, transitivity concatenates two chains, and congruence places every link in the same constructor context. Thus each link changes only one adjacent pair ${ℓ : τ, m : υ ∣ ρ} \leftrightarrow {m : υ, ℓ : τ ∣ ρ}, ℓ \neq m,$ possibly below constructors.

One such link preserves formation. Formation of the left row says that $ρ$ lacks $m$ and that ${m : υ ∣ ρ}$ lacks $ℓ$ . Since $ℓ \neq m$ , the latter premise reduces to the fact that $ρ$ lacks $ℓ$ . These two facts build the right row in the opposite order. The reverse direction is the same calculation. If the exchange occurs inside a tail, the same calculation is performed there and each enclosing Row-Ext is rebuilt; its lacks premise is unchanged because an exchange of labels distinct from the queried label merely changes the order of two L-Extend steps. Type constructors and field types rebuild structurally. Induction along the flattened chain proves item 1, including formation of every intermediate expression.

An exchange has row sort. Placing it in a type context can change only the components below that fixed context; it cannot change the outer type constructor. Follow the chain and project its links into the two arrow components or the single $Rec$ or $Var$ component. The projected chains are the equalities displayed in item 2. A base type or type variable has no row-containing subexpression, so its chain is empty. ◻

Lemma 4.4 — Lacks respects row equality ¶

If $ρ \equiv_{P} ρ^{'}$ , then $P ⊩ ρ \ ℓ$ exactly when $P ⊩ ρ^{'} \ ℓ$ .

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.4 — Lacks respects row equality

Proof. It suffices to inspect one adjacent exchange in its constructor context. If the exchanged pair belongs to the row whose lack of $ℓ$ is being proved and either exchanged label is $ℓ$ , neither side has a lacks derivation. If both labels differ from $ℓ$ , two uses of L-Extend remove them in either order and leave the same tail judgment. An exchange inside a field type leaves that row unchanged. An exchange in its tail is handled by the induction hypothesis before rebuilding the identical outer L-Extend steps. Congruence, symmetry, and transitivity preserve the resulting equivalence. ◻

Thus ${host : String, port : Nat ∣ ξ} \equiv_{P} {port : Nat, host : String ∣ ξ},$ provided $P ⊩ ξ \ host$ and $P ⊩ ξ \ port$ . The order has changed; the label-to-type association has not.

Lemma 4.5 — Finite-map character of strict rows ¶

Let $P ⊢ ρ row$ .

Every displayed label occurs at most once before any row-variable tail.
Two rows with the same tail variable (or both with empty tail) are equal exactly when their displayed fields determine the same finite map from labels to types, with field types compared by type equality.
If $ℓ : τ$ occurs in $ρ$ , there is a row $ρ - ℓ$ , unique up to $\equiv_{P}$ , such that $ρ \equiv_{P} {ℓ : τ ∣ ρ - ℓ}$ .

Referenced from 10 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.5 — Finite-map character of strict rows

Proof. For item 1, induction on formation. The premise of Row-Ext says the tail lacks the new label. For item 2, adjacent exchanges of distinct labels generate every permutation of a finite list, so equal finite maps give equal rows. Conversely, one exchange preserves the finite map; induction on an equality derivation proves the other direction.

For item 3, scan the displayed fields. At the desired label, delete its field. Before reaching it, exchange it leftward past each distinct label. Item 1 guarantees that there is only one field to delete. Any two scans leave the same finite map and tail, hence item 2 makes their results equal. ◻

The tempting equation ${ℓ : τ, ℓ : υ ∣ ρ} \equiv {ℓ : υ, ℓ : τ ∣ ρ}$ is not merely absent: neither side is a strict row. If duplicates were admitted and the equation were added, selection would have to decide which $ℓ$ is meant. A system that retains the first matching label can be coherent, but it is a different calculus.

Exercise 4.1 ¶

★☆☆ Assume $P$ entails that $ξ$ lacks $host$ , $port$ , and $secure$ . Give adjacent-exchange derivations putting each of the three labels first in ${host : String, port : Nat, secure : Bool ∣ ξ} .$ Explain at which formation premise the same calculation fails if the last label is another $port$ .

Referenced from 3 locations

Qualified types and record operations

A lacks predicate is useful only if it can travel with a polymorphic function. We therefore refine the schemes of definition 3.6.

Definition 4.6 — Qualified schemes ¶

A qualified type and a qualified scheme have forms $χ ::= P \Rightarrow τ, σ ::= \forall \bar{α} \bar{ξ} . P \Rightarrow τ .$ Read $P \Rightarrow τ$ as type $τ$ subject to the assumptions $P$ . This double arrow belongs to qualified types; the mapsto arrow in a case term separates a pattern from its branch body. The prefix binds both sorts of variables. A ground substitution $G$ satisfies $P$ , written $G ⊧_{g} P$ , when every $ρ \ ℓ \in P$ becomes a closed strict row lacking $ℓ$ . This notation is used in the ground-discharge interface below.

A symbolic instance of $σ$ in an ambient predicate context $P^{'}$ chooses a substitution $T$ for exactly the quantified prefix, sends type variables to $P^{'}$ -formed types and row variables to $P^{'}$ -formed strict rows, and requires $P^{'} ⊩ nf (P [T]) .$ It then has type $τ [T]$ . Thus a symbolic use retains residual row variables and discharges their lacks requirements from the ambient assumptions. A ground instance additionally requires every image of $T$ to be closed; taking $P^{'} = \emptyset$ alone does not close a row-variable image. Generalize every type or row variable absent from $Γ$ . A predicate mentioning a variable fixed by $Γ$ remains outside the scheme as a residual assumption, because no use of the let-bound variable can discharge it. Formally, put $X = ftv (P, τ) ∖ ftv (Γ), P^{r} = {p \in P ∣ ftv (p) ⊈ X} .$ Then ${Gen}_{Γ} (P \Rightarrow τ) : = \forall X . P \Rightarrow τ,$ where $\forall X$ lists all type variables first and then all row variables, using once-and-for-all orders on the two countable supplies. On type variables this is the fixed order of definition 3.12; the row-variable order extends that convention rather than replacing it. Generalization keeps all of $P$ in the scheme. The residual predicates $P^{r}$ mention variables fixed by the environment and must additionally remain assumptions of the enclosing let judgment. Thus the whole predicate set travels with the scheme, while the enclosing let also retains $P^{r}$ outside it; otherwise an unused binding could hide an unsatisfied ambient requirement. Here $ftv$ is deliberately two-sorted: it collects both free type variables and free row variables.

Referenced from 4 locations

The constraint is a condition on instantiation, not a hidden field. For example, $\forall α ξ . (ξ \ port) \Rightarrow Rec ({port : α ∣ ξ}) \to α$ has an instance at every record row containing one $port$ field. It has no instance in which $ξ$ itself supplies another $port$ .

The qualified judgment $Γ ⊢_{q} e : P \Rightarrow τ$ records the constraints required by $e$ . Contexts contain qualified schemes. We use a separate nullary signature $Σ_{0} = {zero : Nat, true : Bool, false : Bool} \cup {"s" : String ∣ s is a string} .$ Its constants are values. Thus a closed term has empty $Γ$ without losing the base literals, and no unmentioned arrow-valued primitive can create a stuck application.

Definition 4.7 — Qualified typing ¶

Let $σ = \forall \bar{α} \bar{ξ} . Q \Rightarrow τ_{0}$ . A symbolic instance chooses such a sorted, formation-preserving substitution $T$ for exactly the displayed prefix. Qualified typing is generated by

Γ (x) = σ

P ⊩ nf (Q [T])

P ⊢ τ_{0} [T] type

Γ ⊢_{q} x : P \Rightarrow τ_{0} [T]

Q-Var

c : σ is in the fixed signature

P ⊩ nf (Q [T])

P ⊢ τ_{0} [T] type

Γ ⊢_{q} c : P \Rightarrow τ_{0} [T]

Q-Const

Γ, x : τ_{1} ⊢_{q} e : P \Rightarrow τ_{2}

Γ ⊢_{q} λ x . e : P \Rightarrow τ_{1} \to τ_{2}

Q-Lam

Γ ⊢_{q} e_{1} : P_{1} \Rightarrow τ_{1} \to τ_{2}

Γ ⊢_{q} e_{2} : P_{2} \Rightarrow τ_{1}

nf (P_{1} \cup P_{2}) = P

Γ ⊢_{q} e_{1} e_{2} : P \Rightarrow τ_{2}

Q-App

Γ ⊢_{q} e_{1} : P_{1} \Rightarrow τ_{1}

Γ, x : {Gen}_{Γ} (P_{1} \Rightarrow τ_{1}) ⊢_{q} e_{2} : P_{2} \Rightarrow τ_{2}

nf (P_{1}^{r} \cup P_{2}) = P

Γ ⊢_{q} let x = e_{1} in e_{2} : P \Rightarrow τ_{2}

Q-Let

Γ ⊢_{q} e : P \Rightarrow τ

τ \equiv_{P} τ^{'}

Γ ⊢_{q} e : P \Rightarrow τ^{'}

Q-Conv

Every judgment $Γ ⊢_{q} e : P \Rightarrow τ$ presupposes that $Γ$ is a context of $P$ -formed schemes and that $P ⊢ τ type$ . A monotype declaration abbreviates the scheme $\forall \emptyset . \emptyset \Rightarrow τ$ .

Referenced from 4 locations

The six rules already type a complete qualified let before any transport lemma is needed. With $id = λ x . x$ , the derivation $\frac{\begin{matrix} \frac{x : α ⊢_{q} x : \emptyset \Rightarrow α}{\cdot ⊢_{q} λ x . x : \emptyset \Rightarrow α \to α} Q - Lam \\ id : \forall α . \emptyset \Rightarrow α \to α ⊢_{q} id zero : \emptyset \Rightarrow Nat \end{matrix}}{\cdot ⊢_{q} let id = λ x . x in id zero : \emptyset \Rightarrow Nat} Q - Let$ uses the $Nat$ instance at the body occurrence. A predicate-bearing let differs only in the residual set retained by Q-Let; the first such calculation follows the record rules below.

Qualified typing is declarative: it constrains instances and lets but chooses no fresh variables, work-list order, or unification strategy. Rules Q-Var and Q-Const instantiate constraints at use sites, while Q-Let is the sole generalization rule.

The opening programs force four saturated record operations before any transport theorem is required.

Definition 4.13 — Record terms and typing ¶

Extend the pure let-language of definition 3.1 by $e ::= \dots ∣ {} ∣ {ℓ = e ∣ e} ∣ e . ℓ ∣ e - ℓ .$ The empty record is the base case. Selection exposes a field after row conversion, and restriction retains the exposed tail:

Γ ⊢_{q} {} : \emptyset \Rightarrow Rec (ϵ_{ρ})

Q-Empty

Γ ⊢_{q} r : P \Rightarrow Rec ({ℓ : τ ∣ ρ})

Γ ⊢_{q} r . ℓ : P \Rightarrow τ

Q-Select

Γ ⊢_{q} r : P \Rightarrow Rec ({ℓ : τ ∣ ρ})

Γ ⊢_{q} r - ℓ : P \Rightarrow Rec (ρ)

Q-Restrict

Extension joins the constraints of its two subterms with the exact absence fact that makes the result strict:

Γ ⊢_{q} a : P_{1} \Rightarrow τ

Γ ⊢_{q} r : P_{2} \Rightarrow Rec (ρ)

nf (P_{1} \cup P_{2} \cup {ρ \ ℓ}) = P

Γ ⊢_{q} {ℓ = a ∣ r} : P \Rightarrow Rec ({ℓ : τ ∣ ρ})

Q-Extend

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Update is derived rather than primitive: ${ℓ := e ∣ r} : = {ℓ = e ∣ r - ℓ} .$ If $e : α$ and $r : Rec ({ℓ : β ∣ ξ})$ , restriction returns $Rec (ξ)$ and extension returns $Rec ({ℓ : α ∣ ξ})$ under the constraint $ξ \ ℓ$ . The repeated tail $ξ$ expresses preservation of every untouched field.

Lemma 7.12 — Predicate weakening ¶

If $P^{'}$ entails every predicate of $P$ and $Γ ⊢_{q} e : P \Rightarrow τ$ , then $Γ ⊢_{q} e : P^{'} \Rightarrow τ$ , provided the displayed context and type are formed under $P^{'}$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.12 — Predicate weakening

Proof. Induct on the typing derivation. Variable and constant leaves retain their instance entailments by transitivity. Lambda, application, and the record and variant rules use the induction hypotheses and normalization idempotence.

For Q-Let, keep the first premise $Γ ⊢_{q} e_{1} : P_{1} \Rightarrow τ_{1}$ , its generalized declaration $σ = {Gen}_{Γ} (P_{1} \Rightarrow τ_{1})$ , and the residual split fixed. The induction hypothesis weakens only the body premise from $P_{2}$ to $P^{'}$ . Since the original conclusion has $P = nf (P_{1}^{r} \cup P_{2})$ and $P^{'} ⊩ P$ , every member of $P_{1}^{r}$ and every member of $P_{2}$ is entailed by $P^{'}$ . Hence $nf (P_{1}^{r} \cup P^{'}) = P^{'},$ where normalized duplicates are discarded and every residual assumption is already a consequence of $P^{'}$ . Reapply Q-Let with conclusion context $P^{'}$ . This argument does not require $P^{'}$ to entail predicates that were generalized into $σ$ ; those remain checked only at instances of the bound variable. For Q-Conv, lacks conversion preserves the row equalities used by the final type conversion. ◻

Definition 4.8 — Substitution and qualified-context equivalence ¶

For a finite two-sorted set $X$ of variables, write $S \equiv_{P} T on X$ when the two substitutions have $P$ -formed images there and $α [S] \equiv_{P} α [T]$ for every type variable $α \in X$ , while $ξ [S] \equiv_{P} ξ [T]$ for every row variable $ξ \in X$ . Literal list equality would be wrong: two factors may display the same strict row in different field orders.

Two scheme contexts are $P$ -equivalent, written $Γ \equiv_{P} Γ^{'}$ , when they have the same term variables and every pair of corresponding schemes satisfies the following three conditions after common freshening:

their quantified prefixes are identical;
their bodies are raw-equal up to row permutation;
for each predicate $ρ \ ℓ$ in the normalized instance predicates of one scheme, the other contains a predicate $ρ^{'} \ ℓ$ with the same label and $ρ \equiv_{P} ρ^{'}$ , and conversely.

Formation here is qualified-scheme formation. For a declaration of the form $\forall \bar{α} \bar{ξ} . Q_{σ} \Rightarrow τ,$ treat its bound prefix as parameters and form every predicate row and $τ$ under $nf (P \cup Q_{σ})$ . Thus a scheme may use the very lacks facts that it records. The definition is deliberately structural rather than merely extensional at $P$ . By lacks conversion, every symbolic instance usable at a variable leaf under $P$ has a $P$ -equal instance in the other context, in both directions.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

For example, under $P = {ξ \ host, ξ \ port}$ , the declarations $\begin{aligned} Γ_{1} & = x : Rec ({host : String, port : Nat ∣ ξ}), \\ Γ_{2} & = x : Rec ({port : Nat, host : String ∣ ξ}) \end{aligned}$ form $P$ -equivalent one-variable contexts. A variable leaf may use either declaration, and conversion identifies the two resulting record types. For a predicate-bearing pair, take $\begin{aligned} y & : \forall ξ . (ξ \ host, ξ \ port) \Rightarrow Rec ({host : String, port : Nat ∣ ξ}), \\ y & : \forall ξ . (ξ \ port, ξ \ host) \Rightarrow Rec ({port : Nat, host : String ∣ ξ}) . \end{aligned}$ Normalization pairs the two $host$ predicates and the two $port$ predicates by label; each paired row is literally $ξ$ .

Row permutation may change the written context without changing any symbolic instance. Admissible substitutions compose, and generalization retains the environmental lacks assumptions needed after substitution. The following transport lemmas state these facts.

Lemma 4.9 — Changing the predicate context ¶

Suppose $Γ \equiv_{P} Γ^{'}$ , and suppose a predicate context $Q$ forms every corresponding scheme in $Γ$ and $Γ^{'}$ in this qualified sense. Then $Γ \equiv_{Q} Γ^{'}$ , and $ftv (Γ) = ftv (Γ^{'})$ .

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.9 — Changing the predicate context

Proof. Work one corresponding declaration at a time, after commonly freshening its quantified prefix. Raw equality is independent of a predicate context, and it preserves every free variable. Under the common internal predicate set $Q_{σ}$ , the assumed qualified $Q$ -formation therefore turns the same raw body equality into equality under $nf (Q \cup Q_{σ})$ . It does the same for the paired rows in the normalized instance predicates; the lacks-conversion lemma then transfers their entailment. Hence a prefix substitution is a symbolic instance of one declaration under $Q$ exactly when it is a symbolic instance of the other, and their instance bodies are $Q$ -equal. This is $Γ \equiv_{Q} Γ^{'}$ . Equality of free-variable sets follows at the same time, declaration by declaration. ◻

Lemma 4.10 — Qualified typing respects equivalent contexts ¶

If $Γ \equiv_{P} Γ^{'}$ and $Γ ⊢_{q} e : P \Rightarrow τ$ , then $Γ^{'} ⊢_{q} e : P \Rightarrow τ$ . In particular, if $S \equiv_{P} T$ on every type and row variable free in $Γ$ , then $Γ [S] \equiv_{P} Γ [T]$ , and either image context may replace the other in a qualified typing under $P$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.10 — Qualified typing respects equivalent contexts

Proof. Induct on the typing derivation. For a variable leaf, commonly freshen $Γ (x)$ and $Γ^{'} (x)$ . If the original symbolic instance uses prefix substitution $T$ , the definition of context equivalence gives $τ_{x} [T] \equiv_{P} τ_{x}^{'} [T] and P ⊩ nf (Q_{x} [T]) .$ Thus Q-Var derives the corresponding instance under $Γ^{'}$ , and Q-Conv restores the original result type. Constants do not inspect the context. For every other premise with predicate context $P_{i}$ , the formation presupposition of definition 4.7 supplies qualified $P_{i}$ -formation derivations for every declaration used in that premise. The change lemma therefore gives $Γ \equiv_{P_{i}} Γ^{'}$ . Apply the induction hypothesis to that premise, then reapply the lambda, application, record, or variant rule.

In a let, the first induction hypothesis preserves $P_{1}$ and $τ_{1}$ . The change lemma gives $ftv (Γ) = ftv (Γ^{'})$ , so both generalizations choose the same prefix and residual split. Extend both contexts by this common declaration and apply the second induction hypothesis under $P_{2}$ . Transitivity discharges the final conversion. The last assertion follows by induction on scheme bodies; pointwise row equality is preserved by every type constructor, and the preceding lacks-conversion lemma preserves every instantiated predicate. ◻

Lemma 7.16 — Admissibility of one-variable elimination ¶

Suppose $a$ is $P$ -formed, $z$ has the same sort as $a$ , $z \notin ftv (a)$ . Put $I = [a / z]$ , and suppose $Q = nf (P [I])$ exists. Then $I : P \to Q$ is admissible.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.16 — Admissibility of one-variable elimination

Proof. The substitution is finite and sort preserving. Its only nonidentity image is formed and, at row sort, strict by hypothesis. Substitute $[a / z]$ through its formation derivation. In the Row-Ext case, substitute through the lacks derivation as well. Each resulting assumption leaf occurs in $Q = nf (P [I])$ , so it is entailed by $Q$ . This proves that the image is $Q$ -formed. Finally $Q$ is the normal form of the substituted source predicates, so it entails that normal form by reflexivity. These are exactly the clauses of definition 7.3. ◻

Lemma 4.11 — Identity and composition of admissible substitutions ¶

The identity is admissible $P \to P$ . If $S : P \to Q$ and $R : Q \to P^{'}$ are admissible, then $S; R : P \to P^{'}$ is admissible. Moreover, substitution by $R$ sends every $Q$ -formation, lacks-entailment, and strict row equality derivation to the corresponding $P^{'}$ -derivation.

Referenced from 6 locations

Proof of Lemma 4.11 — Identity and composition of admissible substitutions

Proof. Identity substitution leaves every formation, entailment, and strict-equality derivation unchanged. For composition, induct first on type and row formation. Every image under $S$ is $Q$ -formed, and the induction sends it to a $P^{'}$ -formed image under $R$ . Induction on lacks entailment sends $Q ⊩ ρ \ ℓ$ to $P^{'} ⊩ ρ [R] \ ℓ$ : assumption leaves follow from $P^{'} ⊩ nf (Q [R])$ , and empty and unequal extension are preserved literally. Applying this to $Q ⊩ nf (P [S])$ shows $P^{'} ⊩ nf (P [S; R])$ . Adjacent exchanges retain their distinct labels, so the same induction preserves strict row equality. These are exactly the clauses in the definition of admissibility. ◻

A substituted environment may need ambient lacks assumptions to form its declarations. Let $F$ be the normalized lacks assumptions used in those formation derivations. Since every variable of $F$ occurs in the environment, generalization retains rather than quantifies them.

Lemma 4.12 — Ambient formation and generalized declarations ¶

Let $σ = {Gen}_{Γ} (P \Rightarrow τ)$ . Freshen its bound prefix away from $S$ , and write $S \cdot σ$ for substitution by $S$ on the free variables of the scheme only. Suppose $F$ is normalized, every variable of $F$ occurs in $Γ [S]$ , and $P_{S} = nf (P [S] \cup F), σ_{S} = {Gen}_{Γ [S]} (P_{S} \Rightarrow τ [S])$ are formed. If $Q$ entails $F$ , then every qualified derivation under $Γ [S], x : S \cdot σ$ and ambient predicates $Q$ remains derivable after replacing that declaration by $x : σ_{S}$ .

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.12 — Ambient formation and generalized declarations

Proof. Induct on the derivation. Only a leaf selecting $x$ changes. Such a leaf chooses an instance $T$ of the old bound prefix and has entailment premise $Q ⊩ nf (P [S; T])$ . The same $T$ is an instance of $σ_{S}$ . It fixes $F$ , because the variables of $F$ occur in $Γ [S]$ and hence are not generalized. Therefore $Q$ entails $nf (P [S; T] \cup F) = nf (P_{S} [T])$ , and the result type is still $τ [S; T]$ . Rebuild the leaf and then the surrounding derivation. ◻

The residual set of Q-Let is a deliberate difference from unrestricted qualified-implication introduction: a constraint involving an environmental variable cannot be hidden merely because the let-bound variable is unused. Record and variant operations are saturated term forms, so progress needs no run-time status for a half-applied selector or case operator.

Example 4.14 — The environment operations ¶

The definitions $\begin{aligned} portOf & : = λ r . r . port, \\ withSecure & : = λ r . {secure = true ∣ r}, \\ withoutPort & : = λ r . r - port \end{aligned}$ have the displayed schemes $\begin{aligned} portOf & : \forall α ξ . (ξ \ port) \Rightarrow Rec ({port : α ∣ ξ}) \to α, \\ withSecure & : \forall ξ . (ξ \ secure) \Rightarrow Rec (ξ) \to Rec ({secure : Bool ∣ ξ}), \\ withoutPort & : \forall α ξ . (ξ \ port) \Rightarrow Rec ({port : α ∣ ξ}) \to Rec (ξ) . \end{aligned}$ For example, put $P_{s} = {ξ \ secure}$ . Before generalization, the whole derivation of the second definition is $\begin{matrix} r : Rec (ξ) ⊢_{q} true : P_{s} \Rightarrow Bool, r : Rec (ξ) ⊢_{q} r : P_{s} \Rightarrow Rec (ξ), \\ nf (P_{s} \cup P_{s} \cup {ξ \ secure}) = P_{s} . \end{matrix}$ Thus Q-Extend gives the premise of the following Q-Lam instance: $\frac{r : Rec (ξ) ⊢_{q} {secure = true ∣ r} : P_{s} \Rightarrow Rec ({secure : Bool ∣ ξ})}{\cdot ⊢_{q} withSecure : P_{s} \Rightarrow Rec (ξ) \to Rec ({secure : Bool ∣ ξ})} Q - Lam .$ The two leaves are predicate weakenings of Q-Const and Q-Var. The same two-step calculation for $portOf$ ends in Q-Select; for $withoutPort$ it ends in Q-Restrict.

For instance, instantiate $ξ$ in $withSecure$ by ${host : String, port : Nat}$ . The lacks premise reduces twice by L-Extend and ends at L-Empty; the result retains both fields and adds $secure$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

The residual part of Q-Let is visible only when the environment fixes a row variable. Let $Γ = r : Rec (ξ), P_{s} = {ξ \ secure} .$ The extension calculation above gives $Γ ⊢_{q} {secure = true ∣ r} : P_{s} \Rightarrow Rec ({secure : Bool ∣ ξ}) .$ Here $ξ \in ftv (Γ)$ , so the generalized prefix is empty and $P_{s}^{r} = P_{s}$ . Even if the bound variable is unused, $Γ ⊢_{q} let x = {secure = true ∣ r} in zero : P_{s} \Rightarrow Nat .$ The constraint remains because it forms the bound expression; dropping it would accept an ambient record that already contains $secure$ . By contrast, in the closed definition $withSecure$ the row variable is absent from the environment, so the same predicate is generalized with $ξ$ .

The same instantiation fails on a row already containing $secure$ . That rejection is intentional: extension means adding a new field. Replacement is written with update, whose input explicitly contains the old field.

Exercise 4.2 ¶

★☆☆ Derive the scheme of update from restriction and extension using the defining equation above. Write the single tail row at every intermediate type and identify the one lacks predicate used by both operations.

Referenced from 3 locations

Variants from the same rows

A record with row $ρ$ carries every field of $ρ$ . A variant with the same row carries exactly one of them. The shared row language makes record extension and variant widening dual operations.

Definition 4.15 — Variant terms and typing ¶

Extend the grammar by injection $⟨ ℓ = e ⟩$ , embedding ${embed}_{ℓ} e$ , and the binding form ${case}_{ℓ} e of {⟨ ℓ = x ⟩ \mapsto e_{1}; y \mapsto e_{2}},$ where $x$ binds in $e_{1}$ and $y$ in $e_{2}$ . Injection selects the new alternative, while embedding preserves a value from the old row.

Γ ⊢_{q} a : P_{0} \Rightarrow τ

nf (P_{0} \cup {ρ \ ℓ}) = P

Γ ⊢_{q} ⟨ ℓ = a ⟩ : P \Rightarrow Var ({ℓ : τ ∣ ρ})

Q-Inject

Γ ⊢_{q} u : P_{0} \Rightarrow Var (ρ)

nf (P_{0} \cup {ρ \ ℓ}) = P

P ⊢ τ type

Γ ⊢_{q} {embed}_{ℓ} u : P \Rightarrow Var ({ℓ : τ ∣ ρ})

Q-Embed

Decomposition reverses that choice:

Γ ⊢_{q} u : P_{0} \Rightarrow Var ({ℓ : τ ∣ ρ})

Γ, x : τ ⊢_{q} e_{1} : P_{1} \Rightarrow υ

Γ, y : Var (ρ) ⊢_{q} e_{2} : P_{2} \Rightarrow υ

nf (P_{0} \cup P_{1} \cup P_{2}) = P

Γ ⊢_{q} {case}_{ℓ} u of {⟨ ℓ = x ⟩ \mapsto e_{1}; y \mapsto e_{2}} : P \Rightarrow υ

Q-Case

In Q-Inject, the payload derivation determines $τ$ , while the typing derivation chooses the residual row $ρ$ . In Q-Embed, the embedded value inhabits an old alternative, so it supplies no value at the newly added $ℓ$ alternative. Fresh variables make both choices most general.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Injection chooses the new alternative. Embedding preserves a value from the old alternatives. Decomposition reverses that choice. The following calculation shows decomposition and embedding; injection is practiced in the following exercise.

Example 4.16 — An extensible error case ¶

Assume $e : Var ({ok : α, error : String ∣ ξ}), ξ \ ok, ξ \ error .$ First permute the row to expose $error$ . With $ρ = {ok : α ∣ ξ}$ , the case term ${case}_{error} e of {⟨ error = s ⟩ \mapsto zero; y \mapsto zero}$ has type $Nat$ : under $s : String$ the first body is $zero : Nat$ , and under $y : Var (ρ)$ the second body has the same type. The second branch receives the whole residual variant; it may immediately decompose the known $ok$ alternative. An alternative represented only by $ξ$ can be decomposed later only when its label and a corresponding lacks fact are known.

Writing $P_{e}$ for the two displayed lacks predicates, the complete rule instance is $\frac{\begin{matrix} Γ ⊢_{q} e : P_{e} \Rightarrow Var ({error : String ∣ ρ}) \\ Γ, s : String ⊢_{q} zero : \emptyset \Rightarrow Nat \\ Γ, y : Var (ρ) ⊢_{q} zero : \emptyset \Rightarrow Nat \\ nf (P_{e} \cup \emptyset \cup \emptyset) = P_{e} \end{matrix}}{Γ ⊢_{q} {case}_{error} e of {⟨ error = s ⟩ \mapsto zero; y \mapsto zero} : P_{e} \Rightarrow Nat} Q - Case .$

Conversely, if $u : Var (ρ)$ , then ${embed}_{error} u$ has the original larger variant type. No case is lost and no run-time tag is fabricated.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Exercise 4.3 ¶

★★☆ Let $f : α \to β$ and $e : Var ({ok : α, error : String ∣ ξ})$ under the two corresponding lacks predicates. Construct a term of type $Var ({ok : β, error : String ∣ ξ})$ which applies $f$ only to the $ok$ alternative and preserves every other alternative. Display the decomposition, the new injection in the $ok$ branch, and the embedding that puts the residual branch at the common result type.

Referenced from 3 locations

Evaluation and safety

The constraints now have an operational purpose. A record is represented by a finite label-to-value map; a variant by one labeled value. The source syntax does not prescribe an ordering in memory yet.

Definition 4.17 — Values, contexts, and primitive reduction ¶

Evaluation is left-to-right call by value. Write $\begin{aligned} v ::= & c ∣ λ x . e ∣ R ∣ V, \\ R ::= & {} ∣ {ℓ = v ∣ R}, \\ V ::= & ⟨ ℓ = v ⟩, \\ E ::= & [] ∣ E e ∣ v E ∣ let x = E in e \\ ∣ {ℓ = E ∣ e} ∣ {ℓ = v ∣ E} ∣ E . ℓ ∣ E - ℓ ∣ ⟨ ℓ = E ⟩ \\ ∣ {embed}_{ℓ} E ∣ {case}_{ℓ} E of {⟨ ℓ = x ⟩ \mapsto e_{1}; y \mapsto e_{2}} . \end{aligned}$ Record values $R$ have distinct labels. This is the complete evaluation context grammar for the term syntax developed so far. The two base contractions are $(λ x . e) v ⟶ e [v / x], let x = v in e ⟶ e [v / x],$ and the compatible rule is $E ⟨ e ⟩ ⟶ E ⟨ e^{'} ⟩$ whenever $e ⟶ e^{'}$ . Write $e ⟶^{*} e^{'}$ for the reflexive–transitive closure of this source reduction. The primitive redexes are $\begin{aligned} {ℓ = v ∣ R} . ℓ & ⟶ v, \\ {m = w ∣ R} . ℓ & ⟶ R . ℓ & (m \neq ℓ), \\ {ℓ = v ∣ R} - ℓ & ⟶ R, \\ {m = w ∣ R} - ℓ & ⟶ {m = w ∣ R - ℓ} & (m \neq ℓ), \\ {embed}_{ℓ} ⟨ m = v ⟩ & ⟶ ⟨ m = v ⟩ & (m \neq ℓ), \\ {case}_{ℓ} ⟨ ℓ = v ⟩ of {⟨ ℓ = x ⟩ \mapsto e_{1}; y \mapsto e_{2}} & ⟶ e_{1} [v / x], \\ {case}_{ℓ} ⟨ m = v ⟩ of {⟨ ℓ = x ⟩ \mapsto e_{1}; y \mapsto e_{2}} & ⟶ e_{2} [⟨ m = v ⟩ / y] & (m \neq ℓ) . \end{aligned}$ Record extension with an already present label and variant embedding of an $ℓ$ -tag are not run-time states of a well-typed program; the lacks premise excludes them. Update first restricts and then extends.

Referenced from 5 locations

Row Polymorphism and Extensible Records and Variants

For a neutral scrutinee $z$ , a variant case does not reduce. Its typing derivation contains premises for both branch bodies, one under the inserted label and one under the residual row; neither premise determines which tag a future closing substitution will reveal.

Weakening and term substitution are unchanged by rows: predicates and types contain no term variables. Type-and-row substitution requires one extra observation.

Lemma 4.18 — Structural stability ¶

Let $S : P \to Q$ be admissible.

Lacks entailment. If $P ⊩ ρ \ ℓ$ , then $Q ⊩ ρ [S] \ ℓ$ .
Formation and equality. If $P ⊢ ρ row$ , then $Q ⊢ ρ [S] row$ ; if $ρ \equiv_{P} ρ^{'}$ , then $ρ [S] \equiv_{Q} ρ^{'} [S]$ .
Type-and-row substitution. From $Γ ⊢_{q} e : P \Rightarrow τ$ follows $Γ [S] ⊢_{q} e : Q \Rightarrow τ [S]$ .
Term substitution. If $x$ has monotype $τ_{x}$ , $Γ, x : τ_{x} ⊢_{q} e : P \Rightarrow τ$ , and $Γ ⊢_{q} a : P_{a} \Rightarrow τ_{x}$ , then $Γ ⊢_{q} e [a / x] : Q \Rightarrow τ$ for $Q = nf (P \cup P_{a})$ . If instead $Γ, x : {Gen}_{Γ} (P_{a} \Rightarrow τ_{a}) ⊢_{q} e : P \Rightarrow τ, Γ ⊢_{q} a : P_{a} \Rightarrow τ_{a},$ then $Γ ⊢_{q} e [a / x] : P \Rightarrow τ$ : the constraints of every instance of $a$ are entailed at the corresponding use of $x$ .
Weakening. Weakening by a declaration fresh for the term preserves typing.

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.18 — Structural stability

Proof. For item 1, normalize the substituted entailment derivation. An assumption $ξ \ ℓ$ becomes a predicate whose normal form occurs in $Q$ . Empty and unequal extension commute with $S$ , because substitutions do not change labels. Item 2 is simultaneous induction on formation and equality. At Row-Ext, substitution sends the premise $P ⊩ ρ \ ℓ$ to $Q ⊩ ρ [S] \ ℓ$ ; an adjacent exchange retains its two distinct labels.

For item 3, induct on qualified typing. Variable and constant instances compose their prefix substitution with $S$ . Application and each record/variant rule normalize the substituted union of premise constraints. Lambda is structural. In Q-Let, write its first predicates as $P_{1} = P_{1}^{g} \cup P_{1}^{r}$ and freshen the generalized prefix away from $S$ . Define the finite set without choosing formation derivations: $F = {ξ \ ℓ \in Q ∣ ξ \in ftv (Γ [S])} .$ Formation is syntax-directed on a row, so these are exactly the possible assumption leaves used to form the context images. Every variable of $F$ occurs in $Γ [S]$ . Then $P_{1}^{S} = nf (P_{1} [S] \cup F)$ contains the normal forms of every substituted premise and every context assumption used by $S$ . Hence the restriction of $S$ is an admissible map $P_{1} \to P_{1}^{S}$ , so the first induction hypothesis gives $Γ [S] ⊢_{q} e_{1} [S] : P_{1}^{S} \Rightarrow τ_{1} [S]$ . The body induction hypothesis initially uses the declaration $S \cdot {Gen}_{Γ} (P_{1} \Rightarrow τ_{1})$ . Apply lemma 4.12 to replace it by ${Gen}_{Γ [S]} (P_{1}^{S} \Rightarrow τ_{1} [S])$ . Finally $Q$ entails $F$ and $P_{1}^{r} [S]$ , so Q-Let returns exactly the ambient predicate context $Q$ . The case rule freshens both branch binders. Conversion uses item 2.

For item 4, induct on typing and freshen lambda, let, and case binders away from $a$ . At a monomorphic distinguished variable leaf use the premise for $a$ and normalize the union. At a polymorphic let leaf, its symbolic instance is a substitution $T$ on the generalized variables. First use the leaf premises to regard $T$ , extended by the identity elsewhere, as an admissible map $P_{a} \to P$ : its images are $P$ -formed and $P$ entails $nf (P_{a} [T])$ . Item 3 therefore types the same term $a$ at $τ_{a} [T]$ directly under the surrounding $P$ . The domain of $T$ contains only variables generalized away from $Γ$ , so $Γ [T] = Γ$ . Thus no extra copy of the scheme’s predicates is added to the conclusion. Every other variable is unchanged. Each record, variant, and case rule reapplies after the induction hypotheses for its immediate subterms. Weakening is the same induction, because no old variable leaf selects the fresh declaration. ◻

Corollary 4.19 — Ground discharge ¶

If $Γ ⊢_{q} e : P \Rightarrow τ$ and $G : P \to \emptyset$ is an admissible ground substitution on all free type and row variables of $Γ, P, τ$ , so in particular $G ⊧_{g} P$ , then $Γ [G] ⊢_{q} e : \emptyset \Rightarrow τ [G] .$

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Proof of Corollary 4.19 — Ground discharge

Proof. Admissibility says that every image is formed and every predicate in $P [G]$ normalizes to $⊤$ , hence $nf (P [G]) = \emptyset$ . Now item 3 of lemma 4.18 applies. ◻

The word admissible cannot be replaced by ground. A raw map sending an unconstrained $ξ$ to ${ℓ : Nat, ℓ : Bool}$ grounds $ξ$ and vacuously satisfies the empty predicate set, but its image is not a strict row and cannot classify a term.

The preservation proof needs to peel a run-time map in the same way as its static row.

Lemma 4.20 — Peeling and deletion ¶

Let $P$ be normalized, let $P ⊢ ρ row$ , and let $Γ$ be a context of $P$ -formed schemes.

if $Γ ⊢_{q} {m = w ∣ R} : P \Rightarrow Rec (ρ)$ , then there are $υ, ρ_{0}$ with $ρ \equiv_{P} {m : υ ∣ ρ_{0}}, Γ ⊢_{q} w : P \Rightarrow υ, Γ ⊢_{q} R : P \Rightarrow Rec (ρ_{0}) .$
If distinct labels $m, ℓ$ occur in $ρ$ , then $(ρ - m) - ℓ \equiv_{P} (ρ - ℓ) - m$ ; both deletions preserve the same tail variable, every other displayed field, and its type.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.20 — Peeling and deletion

Proof. Strip final uses of Q-Conv. Lemma 7.6(2) ensures that each conversion retains the outer $Rec$ constructor and projects to an equality of its rows. The only rule producing the displayed record constructor is Q-Extend, whose two premises give $w$ and $R$ ; its conclusion gives the extended row. If a premise uses a smaller normalized predicate context, apply lemma 7.12 to restore $P$ , then reapply the stripped conversions to obtain the first equality and both displayed qualified typings. For item 2, use the finite-map description of lemma 4.5: both orders of deletion leave the same finite map and the same row-variable or empty tail, so they are equal under $P$ . ◻

Lemma 4.21 — Ground canonical forms ¶

Let $P$ be normalized, let $P ⊢ ρ row$ , and let $Γ$ be a context of $P$ -formed schemes.

If $Γ ⊢_{q} R : P \Rightarrow Rec (ρ)$ and $R$ is a record value, then either $R = {}$ and $ρ \equiv_{P} ϵ_{ρ}$ , or $R = {ℓ = w ∣ R_{0}}$ and there are $τ, ρ_{0}$ such that $ρ \equiv_{P} {ℓ : τ ∣ ρ_{0}}, Γ ⊢_{q} w : P \Rightarrow τ, Γ ⊢_{q} R_{0} : P \Rightarrow Rec (ρ_{0}) .$
If $Γ ⊢_{q} V : P \Rightarrow Var (ρ)$ and $V$ is a variant value, then $V = ⟨ ℓ = w ⟩$ and there are $τ, ρ_{0}$ such that $ρ \equiv_{P} {ℓ : τ ∣ ρ_{0}}, Γ ⊢_{q} w : P \Rightarrow τ .$
If $Γ ⊢_{q} v : P \Rightarrow A \to B$ and $v$ is a value, then $v = λ x . e$ . This uses the deliberately nullary constant signature $Σ_{0}$ ; it contains no arrow-valued constants.

When $P = \emptyset$ , $Γ = \cdot$ , and $ρ$ is closed, repeated use of item 1 shows that a record value has exactly one value at each label of $ρ$ ; item 2 selects exactly one field of a closed variant row.

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.21 — Ground canonical forms

Proof. Strip final conversions and inspect the last introduction rule. Rules Q-Empty and Q-Extend give the two record cases and their displayed premises; Q-Inject gives the variant case. Projecting the stripped conversion through $Rec$ or $Var$ supplies the row equalities by lemma 7.6(2). An embedding is not a value form. Base constants, records, and variants cannot have arrow type, so the remaining arrow-valued form is an abstraction.

In the closed record case, repeat item 1 down the finite value spine. Every Q-Extend premise proves that the new label is absent from the tail, so no label repeats. The terminal Q-Empty fixes the empty tail, and row equality preserves the resulting finite label-to-type map. The closed variant statement is item 2 together with the same finite-map characterization. ◻

Theorem 4.22 — Safety of strict records and variants ¶

Suppose $\cdot ⊢_{q} e : P \Rightarrow τ$ . For every substitution $G : P \to \emptyset$ that is admissible and grounds all free type and row variables of $P, τ$ :

if $e ⟶ e^{'}$ , then $\cdot ⊢_{q} e^{'} : \emptyset \Rightarrow τ [G]$ ;
either $e$ is a value or some $e^{'}$ satisfies $e ⟶ e^{'}$ .

Consequently evaluation never selects or removes an absent field and never reaches a variant case without a matching branch.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Proof of Theorem 4.22 — Safety of strict records and variants

Proof. Ground discharge gives $\cdot ⊢_{q} e : \emptyset \Rightarrow τ [G]$ .

For preservation, prove first the stronger qualified assertion: if $Γ ⊢_{q} a : P_{0} \Rightarrow υ$ and $a ⟶ a^{'}$ , then $Γ ⊢_{q} a^{'} : P_{0} \Rightarrow υ$ . Induct on the reduction, with the typing derivation as a subsidiary induction to remove a final conversion. Beta and let use term substitution. This stronger statement is important in the compatible rule for $let x = a in b$ : the predicates stored in the scheme of $x$ need not occur among the body’s predicates, but the reduct of $a$ retains exactly its own qualified typing. For the let contraction, first weaken the body from $P_{2}$ to $nf (P_{1}^{r} \cup P_{2})$ and then apply the generalized term-substitution clause (item 4) of lemma 4.18. The retained residual predicates keep the bound expression formed even when $x$ has no occurrence in the body.

For record lookup, perform an inner induction on the run-time record. At a matching head, lemma 4.20 proves that its stored type is the unique $ℓ$ field type. At an unequal head $m$ , peeling types the tail at $ρ - m$ ; deletion commutation says this residual row still exposes $ℓ$ at the same type, so the inner induction applies. Restriction uses the same inner induction, but reattaches each unequal $m$ field; deletion commutation proves that the resulting row is $ρ - ℓ$ . At the matching head, the preservation subcalculation is therefore explicit: $\frac{Γ ⊢_{q} {ℓ = v ∣ r} : P \Rightarrow Rec ({ℓ : τ ∣ ρ})}{Γ ⊢_{q} {ℓ = v ∣ r} . ℓ : P \Rightarrow τ} Q - Select {ℓ = v ∣ r} . ℓ \overset{l o o k u p}{⟶} v,$ and peeling the record derivation recovers $Γ ⊢_{q} v : P \Rightarrow τ$ , the type of the reduct. The unequal-head induction repeats this calculation on $r$ .

For embedding, qualified value inversion says the old value is $⟨ m = v ⟩$ with $m$ in the residual row. The lacks premise gives $m \neq ℓ$ , and injection at the enlarged row types the reduct. In the matching case clause, the payload has the field type $τ$ from Q-Case; in the unequal clause, deleting $ℓ$ from the finite map leaves the tag $m$ in $ρ$ , so the residual value has type $Var (ρ)$ . More explicitly, lemma 4.5(3) writes the original row as ${m : υ ∣ ρ - m}$ ; deletion of the distinct $ℓ$ preserves that field, so Q-Inject types the residual tag. Term substitution types the selected branch. Compatible-context cases use the induction hypothesis under the corresponding displayed typing rule.

For progress, induct on the closed typing derivation with the strengthened property: for every predicate context $P_{0}$ and every ground admissible $H : P_{0} \to \emptyset$ , a closed judgment $\cdot ⊢_{q} a : P_{0} \Rightarrow A$ has a subject that is a value or steps. Reduction does not inspect types or $H$ , so changing the ground satisfier between premise calls does not change the subject or its next step. Every normalized predicate set has a ground admissible substitution: send every row variable to $ϵ_{ρ}$ and every unconstrained type variable to $Nat$ . Use such a substitution whenever an immediate premise carries predicates not retained by its conclusion. In particular, for a let, apply the induction hypothesis to the bound expression under a ground satisfier of its own $P_{1}$ ; if it steps, use the let context, and if it is a value, use the let contraction. For application, first step the function; when it is a lambda value, step the argument; when both are values, beta reduction applies and term substitution types the reduct. Constants and lambdas are already values. For Q-Let, use the bound premise under its own normalized $P_{1}$ , as above, because its generalized predicates need not occur in the conclusion. In every other multi-premise rule, each premise constraint belongs to the conclusion’s normalized union, so one ground satisfier serves all immediate premises.

If the scrutinee of a row operation steps, use the compatible rule. If it is a value, lemma 4.21 proves that it has the required field form, residual-record form, or one of the two variant forms, so exactly one displayed primitive clause applies. The strictness premise rules out the two forbidden duplicate states named after definition 4.17. ◻

Lemma 7.28 — Determinism of the extended source ¶

If $e ⟶ e_{1}$ and $e ⟶ e_{2}$ , then $e_{1} = e_{2}$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.28 — Determinism of the extended source

Proof. Every nonvalue that steps has a unique decomposition $e = E ⟨ r ⟩$ , where $r$ is one of the root redexes in definition 4.17. Prove this by induction on $e$ , following the left-to-right context grammar. For example, a record selection first follows its unique scrutinee decomposition. Once its scrutinee is a record value, exactly one of $m = ℓ$ and $m \neq ℓ$ selects the matching-head or unequal-head root clause. Restriction and variant case have the same exclusive split; an embedding root exists exactly when its tag differs from the inserted label. The beta and let roots have outer shapes distinct from all row roots. Hence two reductions of $e$ use the same context and root clause, whose contractum is unique. ◻

Exercise 4.4 ¶

★★☆ Suppose $m \neq ℓ$ and a closed record value begins ${m = w ∣ R}$ . Write the full preservation step from ${m = w ∣ R} . ℓ$ to $R . ℓ$ : expose the static $m$ field, type $R$ , and use deletion commutation to show that its row still contains the same $ℓ$ field.

Referenced from 3 locations

Type safety says why lacks predicates are not bureaucratic decoration: they are the static form of the fact that the operational lookup and deletion recursions will find exactly one component.

Unifying rows

Inference must solve equations such as ${port : α ∣ ξ} ≐ {host : String, port : Nat ∣ ζ} .$ The first labels disagree syntactically, but the equation is solvable: move $port$ to the front on the right, unify $α$ with $Nat$ , and make the two remainders agree. Ordinary first-order decomposition cannot perform the first step. The operation it lacks is: expose a requested field wherever it occurs, extending an open tail if necessary.

Exposing a field in an open tail must also preserve strictness. A substitution-only insertion clause would return $I_{0} = [{ℓ : τ ∣ ζ} / ξ] with no obligation on ζ .$ Instantiating the supposedly fresh tail by $ζ = {ℓ : υ}$ then produces ${ℓ : τ, ℓ : υ}$ , which is not a strict row. If the input context contains $ξ \ ℓ$ , applying $I_{0}$ should instead produce $⊥$ , but a substitution-only result has nowhere to record that failure. The repair is to return the new lacks obligation together with the substitution. Replacing an open tail $ξ$ by ${ℓ : τ ∣ ζ}$ is valid only if the fresh tail $ζ$ lacks $ℓ$ . Therefore insertion cannot return a substitution alone; it must return the new obligation at the moment the new tail is created.

Definition 4.23 — Constrained insertion and unification ¶

The insertion and unification algorithms below are mutually recursive. Within their clauses, $q, r, ρ, ρ^{'}$ range over rows. The disambiguation table following definition 4.1 fixes the overloaded row operations; the two signatures displayed below fix the inputs and outputs of $insert$ and $solve$ .

Given $P ⊢ τ type$ and $P ⊢ ρ row$ , ${insert}_{P} (ℓ : τ, ρ) = (I, Q, ρ^{-})$ returns an admissible substitution $I : P \to Q$ and a residual row such that $ρ [I] =_{r} {ℓ : τ [I] ∣ ρ^{-}}, Q ⊩ ρ^{-} \ ℓ .$ For one top-level call, let $A$ contain every variable in its predicate set, types, rows, equations, and any protected set named by the caller. Recursive calls share one supply; a fresh choice is the first variable, in the fixed type- and row-variable orders specified with generalization, outside $A$ and all earlier choices of that call. The insertion clauses are:

For a row variable $ξ$ , provided $ξ \notin ftv (τ)$ , choose fresh $ζ$ , set $I = [{ℓ : τ ∣ ζ} / ξ], Q = nf (P [I] \cup {ζ \ ℓ}), ρ^{-} = ζ .$ Fail if the occurs check or normalization fails.
Insertion into $ϵ_{ρ}$ fails.
For $ρ = {ℓ : υ ∣ ρ_{0}}$ , compute $solve (P; τ ≐ υ) = (U, Q)$ and return $(U, Q, ρ_{0} [U])$ .
For $ρ = {m : υ ∣ ρ_{0}}$ with $m \neq ℓ$ , compute ${insert}_{P} (ℓ : τ, ρ_{0}) = (I, Q, q)$ and return $(I, Q, {m : υ [I] ∣ q}) .$

The solver $solve (P; E) = (U, Q)$ takes a finite predicate set $P$ and a finite, well-sorted list $E$ of equations between types or rows formed under $nf (P)$ . Every call first normalizes $P$ and fails if normalization reaches $⊥$ . The clauses below are tried in their printed order, so the algorithm is deterministic up to fresh names.

On the empty work list, return $(id, nf (P))$ .
Discard a syntactic identity $a ≐ a$ at the head of a nonempty list.
If the head is $z ≐ a$ , where $z$ is a type variable and $a$ a type, or $z$ is a row variable and $a$ a row, fail when $z \in ftv (a)$ . Otherwise put $I = [a / z]$ , normalize $P_{1} = nf (P [I])$ , solve $solve (P_{1}; E [I]) = (V, Q),$ and return $(I; V, Q)$ . If both sides are variables of the same sort, this clause eliminates the left variable. A head $a ≐ z$ is oriented to $z ≐ a$ only when $a$ is not itself a variable. Thus the orientation is deterministic, row-variable equations are eliminated explicitly, and both the old predicates and the remaining equations are rewritten by $I$ . Thus U-Var fuses the orient and eliminate behaviours that definition 3.22 names separately.
This clause applies only to equations of type sort. Equal base-type constructors are discarded; unequal base types and unlike outer type constructors fail. Replace $τ_{1} \to τ_{2} ≐ υ_{1} \to υ_{2}$ by the two equations $τ_{1} ≐ υ_{1}, τ_{2} ≐ υ_{2}$ in that order. Replace $Rec (ρ) ≐ Rec (q)$ and $Var (ρ) ≐ Var (q)$ by $ρ ≐ q$ . A record constructor never unifies with a variant constructor.
Discard $ϵ_{ρ} ≐ ϵ_{ρ}$ . An empty row against an extension fails.
After the preceding variable clauses, an extension equation has an extension on each side. For ${ℓ : τ ∣ ρ} ≐ q$ , compute $\frac{\begin{matrix} {insert}_{P} (ℓ : τ, q) = (I, P_{1}, q^{-}) \\ solve (P_{1}; (ρ [I] ≐ q^{-}, E [I])) = (V, Q) \end{matrix}}{\begin{matrix} solve (P; ({ℓ : τ ∣ ρ} ≐ q, E)) \\ = (I; V, Q) \end{matrix}} .$ Here $(a ≐ b, E)$ means that $a ≐ b$ is placed at the front of the remaining work list. Insertion may scan through several distinct labels before it reaches the requested one or an open tail.

These clauses, together with the four insertion clauses above, are the complete mutually recursive algorithm. Rigid decomposition always prepends its subequations from left to right.

For reference, the complete clause sheet is $\begin{array}{ccll} insert & 1 & I - V a r & ξ \\ 2 & I - E m p t y & ϵ_{ρ} (failure) \\ 3 & I - M a t c h & {ℓ : υ ∣ ρ_{0}} \\ 4 & I - S k i p & {m : υ ∣ ρ_{0}}, m \neq ℓ \\ solve & 1 & U - D o n e & [] \\ 2 & U - D e l e t e & syntactic identity \\ 3 & U - V a r & z ≐ a or its allowed orientation \\ 4 & U - T y p e & type-sort rigid equation \\ 5 & U - E m p t y & empty-row comparison \\ 6 & U - R o w & extension equation via insert \end{array}$ These named rows list the ten clauses in priority order; the definitions above give their outputs and failure conditions. The algorithm is a partial recursive function, so these are defining clauses rather than derivability rules.

Referenced from 4 locations

The first insertion clause is the point that a “unify first, check lacks later” presentation misses. If $P$ already contains $ξ \ m$ with $m \neq ℓ$ , substitution reduces it to $ζ \ m$ . If it contains $ξ \ ℓ$ , normalization reaches $⊥$ , correctly rejecting an attempt to expose a field known to be absent. Independently, $ζ \ ℓ$ makes the newly constructed row itself strict.

For the equation displayed at the start of the section, insertion scans past $host$ , meets $port : Nat$ , and unifies $α$ with $Nat$ . It returns the residual row ${host : String ∣ ζ},$ so the remaining equation is $ξ ≐ {host : String ∣ ζ}$ . No new lacks predicate is needed in this particular scan: both fields were already displayed in a strict input row.

Example 4.24 — Exposing two open tails ¶

The fresh-tail clause appears in the smallest crossing equation. Start with $P = {ξ \ x, ζ \ y}$ and solve ${x : Nat ∣ ξ} ≐ {y : Bool ∣ ζ} .$ To expose $x$ on the right, insertion first passes the distinct $y$ field and then reaches the open tail $ζ$ . Choose fresh $ω$ and set $ζ [I] = {x : Nat ∣ ω} .$ The new tail must lack $x$ . The old predicate $ζ \ y$ also becomes $ω \ y$ . After reattaching the stored $y$ field, the residual equation is $ξ ≐ {y : Bool ∣ ω} .$ Eliminating $ξ$ leaves the principal answer $U = [{x : Nat ∣ ω} / ζ, {y : Bool ∣ ω} / ξ], Q = {ω \ x, ω \ y} .$ Thus the fresh tail is not an implementation trick: its two lacks facts are exactly what makes both substituted rows strict. Any larger common tail is obtained by an admissible instance of $ω$ .

Referenced from 4 locations

Definition 7.31 — Finite-multiset descent ¶

For finite multisets of natural numbers, write $M <_{mul} N$ when there are a nonempty submultiset $X \subseteq N$ and a finite multiset $Y$ such that $M = (N - X) ⊎ Y, and for every y \in Y some x \in X satisfies y < x .$ Thus one or more entries are removed and may be replaced by finitely many strictly smaller entries.

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Lemma 7.32 — Well-founded multiset descent ¶

The relation $<_{mul}$ of definition 7.31 is well founded.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.32 — Well-founded multiset descent

Proof. Suppose an infinite descending chain $M_{0} >_{mul} M_{1} >_{mul} \dots$ existed. A descending step never creates an entry larger than one it removes, so the maximum entry of $M_{0}$ bounds every later multiset. For multisets whose entries are at most $k$ , induct on $k$ . At $k = 0$ , a descending step can only delete zeroes, so cardinality decreases. For the successor step, the number of occurrences of $k$ never increases; whenever a removed occurrence of $k$ is not restored, that number decreases. Along the assumed infinite chain this can happen only finitely often, so the count is eventually constant. Remove those fixed occurrences of $k$ from every remaining multiset. Every subsequent change then concerns entries below $k$ , where the induction hypothesis excludes an infinite descending chain. ◻

Lemma 4.25 — Termination ¶

Constrained insertion and unification terminate on finite input.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.25 — Termination

Proof. Let $L$ be the finite set of labels occurring in the initial predicate set and equation list. No clause invents a label. At any recursive call, apply the accumulated substitution and regard each remaining row-variable tail $t$ as carrying the set $F_{t} : = {ℓ \in L ∣ the normalized predicate context contains t \ ℓ} .$ Equation size alone is not a decreasing measure. In I-Var, replacing $ξ$ by ${ℓ : τ ∣ ζ}$ can make a residual equation strictly larger: $ξ ≐ ρ is replaced by {ℓ : τ ∣ ζ} ≐ ρ .$ The decreasing resource is instead the set of labels that each open tail is still permitted to absorb. Define $Φ : = \sum_{t} (| L | - | F_{t} |) .$ Here $t$ ranges over the distinct row variables in the normalized active input and predicate context, not over their occurrences. The sum is finite because those objects are finite. A global substitution may duplicate occurrences of a tail, but it cannot duplicate a summand.

When insertion exposes $ℓ$ at a variable tail $t$ , normalization fails if $ℓ \in F_{t}$ . Otherwise the clause replaces $t$ globally by one fresh tail $t^{'}$ and gives $F_{t^{'}} = F_{t} \cup {ℓ}$ ; hence $Φ$ decreases by exactly one. If variable elimination identifies two tails, their forbidden sets are unioned and one tail disappears. This cannot increase $Φ$ : for $F, G \subseteq L$ , $| L | - | F \cup G | \leq (| L | - | F |) + (| L | - | G |) .$ Eliminating a tail against a closed row removes its summand. Eliminating it against a displayed row with one existing tail has the same union calculation after the displayed labels have been checked. Thus every row-variable elimination leaves $Φ$ unchanged or decreases it, and fresh-tail creation decreases it strictly.

Let the size of a type or row be its number of syntax nodes, and put $| a ≐ b | = 1 + | a | + | b |, | (ℓ : τ, ρ) | = 1 + | τ | + | ρ | .$ At a solver call, let $M$ be the multiset of equation sizes; at an insertion call, let it be the singleton containing the insertion-input size. Let $N$ count the distinct type variables and row tails in the normalized predicates and active input, after applying the accumulated substitution. Use the lexicographic measure $(Φ, N, M)$ , where $M$ is ordered by $<_{mul}$ .

Every mutually recursive edge is recorded in the following table. A dash means that the earlier component is merely nonincreasing; the rightmost named component is the first strict decrease.

caller clause	callee clause	$Φ$	$N$	strict component and reason
U-Var	solve	–	$↓$	$N$ : occurs-safe elimination
U-Delete/U-Empty	solve	–	–	$M$ : delete one equation
U-Type	solve	–	–	$M$ : proper subterms
U-Row	insert	–	–	$M$ : smaller insertion input
I-Match	solve	–	–	$M$ : field-type subterms
I-Skip	insert	–	–	$M$ : proper row tail
U-Row after insert	solve	–	–	first of $Φ, N, M$ changed below

For U-Var, the occurs check prevents the eliminated variable from reappearing. U-Delete, U-Type, and U-Empty delete an equation or replace one rigid equation by equations between proper subexpressions. In definition 7.31, take $X$ to contain the removed equation size and $Y$ to contain the sizes of the proper-subexpression equations; deletion takes $Y = \emptyset$ . Thus $M$ decreases when the earlier components are unchanged. The first call of U-Row, from solving to insertion, replaces its extension equation by the strictly smaller input $(ℓ : τ, q)$ . I-Match replaces an insertion input by the strictly smaller equation $τ ≐ υ$ , while I-Skip replaces it by the input on a proper row tail. Each of these is the single-element instance $X = {n}$ and $Y = {n^{'}}$ with $n^{'} < n$ .

It remains to compare the second call of U-Row, which solves the residual row equation and old work list. If its insertion computation uses I-Var at any depth, the new lacks fact makes $Φ$ strictly smaller. Otherwise insertion creates no tail. If its returned substitution is nonidentity, some nested solver call used U-Var on a type or row variable; no other clause creates a binding when I-Var is absent. The occurs check prevents that eliminated variable from reappearing, so $N$ strictly decreases. If the returned substitution is the identity, the old work list is unchanged and the residual comparison has removed the matched displayed field, so $M$ strictly decreases. These cases cover every actual mutually recursive edge. Lemma 7.32 and the lexicographic composition of the well-founded orders on $N, N$ , and $<_{mul}$ therefore prove termination. ◻

Lemma 4.26 — Fresh support of insertion and solving ¶

Let $Z$ be a finite set of variables disjoint from the active inputs of an insertion or solver call. The call may choose every fresh tail outside $Z$ , without changing its result except for fresh renaming, and its returned substitution is the identity on $Z$ .

Referenced from 7 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.26 — Fresh support of insertion and solving

Proof. Induct over the mutually recursive clauses. Empty, rigid, and failure clauses introduce no substitution. A variable clause changes only the displayed input variable; an exposing insertion changes only that input variable and chooses its new tail outside $Z$ . Composition preserves identity on $Z$ . In a recursive clause pass $Z$ together with all variables of the surrounding arguments that are absent from the recursive call. Thus neither the recursive result nor a later fresh choice can acquire one of those names. This proves both assertions simultaneously. ◻

Theorem 4.27 — Principal row solver ¶

Insertion. Suppose insertion returns ${insert}_{P} (ℓ : τ, ρ) = (I, Q, ρ^{-})$ . Then equation 4.1 holds and $Q ⊢ ρ^{-} row, ρ [I] \equiv_{Q} {ℓ : τ [I] ∣ ρ^{-}} .$ If $S : P \to P^{'}$ is admissible and $ρ [S] \equiv_{P^{'}} {ℓ : τ [S] ∣ q},$ then $S \equiv_{P^{'}} I; R$ on the variables of $P, τ, ρ$ for some admissible $R : Q \to P^{'}$ . If insertion fails, no such $S$ exists.

Solving. Suppose $E$ is well sorted and formed under $P$ . If $solve (P; E) = (U, Q)$ , then $U : P \to Q$ is admissible and solves every equation of $E$ under $Q$ . Every admissible solution $S : P \to P^{'}$ factors as $S \equiv_{P^{'}} U; R$ on the variables of $P, E$ for some admissible $R : Q \to P^{'}$ . If the solver fails, no admissible solution exists. In particular, a ground admissible solution of $E$ factors through $U$ by a ground admissible map out of $Q$ .

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Theorem 4.27 — Principal row solver

Proof. The calculation terminates by lemma 4.25. Use well-founded induction on that calculation, proving the insertion and solver clauses simultaneously.

For variables in a recursive input, the induction hypothesis gives $S \equiv_{P^{'}} I; R$ . The remaining variables form a protected set $Z$ . For each $z \in Z$ , define $R (z) = S (z)$ ; fresh support gives $I (z) = z$ , so the same factorization equation holds on the surrounding input without changing an equation already factored.

For insertion into a row variable $ξ$ , a target solution has, by lemma 4.5, a unique decomposition $ξ [S] \equiv_{P^{'}} {ℓ : τ [S] ∣ q}$ with $P^{'} ⊩ q \ ℓ$ . Define $ζ [R] = q$ and let $R$ agree with $S$ on the old variables. The displayed lacks judgment satisfies the new predicate $ζ \ ℓ$ ; admissibility of $S$ satisfies every predicate inherited from $P [I]$ . Hence $R : Q \to P^{'}$ and $I; R \equiv_{P^{'}} S$ on the insertion variables. Regard types and rows as one finite, mutually defined syntax tree: arrow components, record/variant indices, and extension field types and tails are its children. If the occurs check finds $z \in ftv (a)$ , any solution would equate the finite tree $S (z)$ with a tree containing $S (z)$ as a proper descendant, which is impossible. The empty row cannot expose a field. If normalization of $P [I] \cup {ζ \ ℓ}$ fails, an inherited predicate entails $ξ \ ℓ$ . Substitution stability would make every admissible target $S : P \to P^{'}$ satisfy $P^{'} ⊩ ξ [S] \ ℓ$ , while the required insertion equality writes $ξ [S]$ as ${ℓ : τ [S] ∣ q}$ . A formed strict row with an $ℓ$ -field cannot lack $ℓ$ , so no target solution exists.

Suppose the insertion input begins with $ℓ : υ$ . Strict finite-map equality separates the target equation into $τ [S] \equiv_{P^{'}} υ [S]$ and $ρ_{0} [S] \equiv_{P^{'}} q$ . Apply the simultaneous induction hypothesis to the smaller type-equation solve, protecting $Z = ftv (ρ_{0}) ∖ ftv (P, τ, υ) .$ Its factor $R_{0}$ agrees with $S$ after $U$ on the active solver variables. By lemma 4.26, $U$ fixes $Z$ . Extend $R_{0}$ by $z [R] = z [S]$ for $z \in Z$ . The new images are formed because $S$ is admissible, while no predicate of the solver output acquires a protected variable; hence the extension remains admissible. It now satisfies $ρ_{0} [U; R] \equiv_{P^{'}} ρ_{0} [S] \equiv_{P^{'}} q$ . Meanwhile substitution stability carries the original tail-lacks premise to $Q ⊩ ρ_{0} [U] \ ℓ$ . This proves the returned specification and its factorization.

Now let the insertion input be ${m : υ ∣ ρ_{0}}$ with $m \neq ℓ$ . In any target solution the unique $m$ field occurs in $q$ . Delete it and put $q_{m} = q - m$ . Deleting $m$ from the target equality gives $ρ_{0} [S] \equiv_{P^{'}} {ℓ : τ [S] ∣ q_{m}} .$ Protect also $Z = ftv (υ) ∖ ftv (P, τ, ρ_{0})$ . The insertion induction hypothesis on the proper tail yields a factor $R_{0}$ and residual $r$ such that $R_{0}$ agrees with $S$ after $I$ on the recursive input. By lemma 4.26, $I$ fixes $Z$ ; extend $R_{0}$ by $z [R] = z [S]$ there, preserving admissibility as in the same-head case. Then reattaching the stored $m : υ [I]$ gives the algorithm’s residual ${m : υ [I] ∣ r}$ , and applying $R$ makes it $P^{'}$ -equal to $q$ . The original strict tail lacks $m$ , and deletion of the distinct $ℓ$ field preserves that fact, so $r$ lacks $m$ . It also lacks $ℓ$ by the induction hypothesis. Thus the reattached residual is formed and the adjacent exchange with $ℓ$ proves the insertion specification.

For the solver, the ordinary sorted variable and rigid-constructor cases are the elimination and decomposition calculations of theorem 3.26, performed separately for type variables and row variables. Each recursive result must additionally normalize its target predicate context; admissibility of the elementary substitution supplies the formation and entailment premises for that normalization. In a variable elimination, the equation’s formation premise proves that the image is formed, the occurs check proves that the eliminated variable is absent from that image, and normalization forms the target predicate context. Therefore lemma 7.16 proves that the elementary substitution is admissible. In particular, a row image remains a formed strict row, and the same substitution preserves formation of the remaining equations by the direct formation induction used in that lemma. Then lemma 4.11 composes the returned factors. In the row-extension case, protect $Z = ftv (ρ, E) ∖ ftv (P, τ, q)$ in the insertion call. Restricting an arbitrary target solution to the insertion equation gives a solution of that insertion problem. Its induction hypothesis gives a factor $R_{1}$ on the active insertion variables. Extend $R_{1}$ by the target solution on $Z$ ; lemma 4.26 says $I$ fixes $Z$ , so the extended map is admissible and agrees with the target after $I$ on $ρ, E$ as well. Because the target solution satisfies the original extension equation, strict finite-map uniqueness identifies its exposed $ℓ$ -field with the one produced by insertion. Deleting that field on both sides gives the residual equation after $R_{1}$ ; agreement on the protected variables also preserves every equation in the old work list. Thus $R_{1}$ solves the residual equation and remaining work list. The solver induction hypothesis factors $R_{1}$ through $V$ , hence the target is $P^{'}$ -equivalent to the composite $I; V; R_{2}$ on every original problem variable. Conversely, the insertion equation reattaches the same $ℓ : τ [I; V]$ field to the residual rows equated by $V$ , so $I; V$ solves the original equation.

The failure cases use the same local obstructions. Predicate normalization at bottom contradicts admissibility. The occurs check contradicts finiteness of the joint tree. Unequal base or outer constructors contradict lemma 7.6(2). An empty row cannot equal an extension by lemma 4.5, and I-Empty is the same fact for insertion. The equal-head and unequal-head insertion failures reduce to a nested solver failure or to the duplicate-label contradiction displayed at the end of the I-Var paragraph. Hence each declared failure excludes a solution.

Finally suppose the competing solution $S : P \to \emptyset$ is ground. In the constructions above, every old or protected variable is mapped as $S$ maps it, and every fresh tail is mapped to a residual row obtained by deleting fields from a closed $S$ -image. Induction on the calculation therefore makes every image of the factor $R : Q \to \emptyset$ closed. This proves the ground conclusion; $P^{'} = \emptyset$ alone would not suffice. ◻

Example 4.28 — A successful and a failing solve ¶

Take the initial formation context $P_{0} = {ξ \ port, ζ \ host, ζ \ port} .$ For $E = {{port : α ∣ ξ} ≐ {host : String, port : Nat ∣ ζ}},$ insertion exposes $port$ on the right, unifies $α$ with $Nat$ , and leaves $ξ ≐ {host : String ∣ ζ}$ . Hence $U = [Nat / α, {host : String ∣ ζ} / ξ] .$ After applying $U$ , the residual context is $Q = {ζ \ host, ζ \ port} .$ The first predicate makes the substitution for $ξ$ a strict row; the second preserves both original row-formation derivations. Every other admissible solution chooses a row for $ζ$ satisfying $Q$ and factors through $U$ .

Now instead begin with $P = P_{0} \cup {ξ \ host}$ . Applying $U$ gives ${host : String ∣ ζ} \ host ⇓ ⊥ .$ The raw equations still unify, but the constrained problem has no admissible solution. This is the static detection of a duplicate-label extension.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Exercise 4.5 ¶

★★☆ Run insertion and row unification on ${x : α, y : Bool ∣ ξ} ≐ {z : String, x : Nat ∣ ζ} .$ First write the four residual lacks predicates needed to form both input rows. Give the MGU and its fresh common tail. Then also normalize the predicates $ξ \ z$ and $ζ \ y$ . State whether the constrained problem succeeds.

Referenced from 3 locations

Qualified Algorithm W and principality

Qualified Algorithm W returns principal source typings. Its predicates are carried through sequential calls and generalized with their types. Each saturated row form adds one syntax-directed clause using the principal solver. The application order is forced by the case term ${case}_{ℓ} ⟨ ℓ = zero ⟩ of {⟨ ℓ = x ⟩ \mapsto (λ z . z) x; y \mapsto (λ z . z) zero} .$ The scrutinee first determines the selected payload type; that substitution must reach the matching branch before the residual branch is inferred, and both branch substitutions must reach the final result equation. The clauses below are the least left-to-right threading that makes those four obligations simultaneously well formed. The calculation immediately after the definition checks every stage on this term.

Definition 4.29 — Qualified Algorithm W ¶

The judgmental notation $W_{r} (Γ, e) = (P, S, τ)$ means that inference returns predicates $P$ , substitution $S$ , and monotype $τ$ . At a top-level call, let $A$ be the finite set of all type and row variables, free or bound, written in $Γ$ and the constant schemes used by $e$ . The call owns two supplies in the fixed variable orders used by generalization. Each recursive call receives the unused suffixes; “choose fresh” means take the first variable outside $A$ and all earlier choices of this top-level call. The clauses are as follows.

For $x$ with $Γ (x) = \forall \bar{α} \bar{ξ} . Q \Rightarrow τ$ , replace the prefix by fresh variables and return the fresh instance of $(Q, id, τ)$ .
For $λ x . e$ , choose fresh $α$ , infer $(P, S, τ)$ under $Γ, x : α$ , and return $(P, S, α [S] \to τ)$ .
Constants use the same fresh qualified instantiation as variables.
For $e_{1} e_{2}$ , infer $(P_{1}, S_{1}, τ_{1})$ , then $(P_{2}, S_{2}, τ_{2})$ under $Γ [S_{1}]$ . Choose fresh $β$ , compute $solve (P_{1} [S_{2}] \cup P_{2}; τ_{1} [S_{2}] ≐ τ_{2} \to β) = (U, Q),$ and return $(Q, S_{1}; S_{2}; U, β [U])$ .
For $let x = e_{1} in e_{2}$ , infer $(P_{1}, S_{1}, τ_{1})$ , put $X_{1} = ftv (P_{1}, τ_{1}) ∖ ftv (Γ [S_{1}]), P_{1}^{g} = {p \in P_{1} ∣ ftv (p) \subseteq X_{1}},$ $P_{1}^{r} = P_{1} ∖ P_{1}^{g}, σ = {Gen}_{Γ [S_{1}]} (P_{1} \Rightarrow τ_{1}),$ infer $(P_{2}, S_{2}, τ_{2})$ under $Γ [S_{1}], x : σ$ , and return $(nf (P_{1}^{r} [S_{2}] \cup P_{2}), S_{1}; S_{2}, τ_{2}),$ failing if normalization does.
$W_{r} (Γ, {})$ returns $(\emptyset, id, Rec (ϵ_{ρ}))$ .
For ${ℓ = a ∣ r}$ , infer $(P_{1}, S_{1}, τ_{1})$ for $a$ , then $(P_{2}, S_{2}, τ_{2})$ for $r$ under $Γ [S_{1}]$ . Choose fresh $ξ$ and solve $solve (P_{1} [S_{2}] \cup P_{2} \cup {ξ \ ℓ}; τ_{2} ≐ Rec (ξ)) = (U, Q) .$ Return $(Q, S_{1}; S_{2}; U, Rec ({ℓ : τ_{1} [S_{2}; U] ∣ ξ [U]})) .$
For $r . ℓ$ , infer $(P, S, τ)$ , choose fresh $α, ξ$ , solve $solve (P \cup {ξ \ ℓ}; τ ≐ Rec ({ℓ : α ∣ ξ})) = (U, Q),$ and return $(Q, S; U, α [U])$ . Restriction uses the same calculation and returns $(Q, S; U, Rec (ξ [U]))$ .
For $⟨ ℓ = a ⟩$ , infer $(P, S, τ)$ , choose fresh $ξ$ , normalize the following set, and return it if normalization succeeds: $(nf (P \cup {ξ \ ℓ}), S, Var ({ℓ : τ ∣ ξ})) .$
For ${embed}_{ℓ} u$ , infer $(P, S, τ)$ , choose fresh $α, ξ$ , solve $solve (P \cup {ξ \ ℓ}; τ ≐ Var (ξ)) = (U, Q),$ and return $(Q, S; U, Var ({ℓ : α [U] ∣ ξ [U]}))$ . The fresh $α$ is intentionally unconstrained: embedding preserves a value from the old row and constructs no payload for the new $ℓ$ alternative.
For a case, infer the scrutinee $(P_{0}, S_{0}, τ_{0})$ , choose fresh $α, ξ$ , and solve $solve (P_{0} \cup {ξ \ ℓ}; τ_{0} ≐ Var ({ℓ : α ∣ ξ})) = (U_{0}, Q_{0}) .$ Infer the matching branch and then the residual branch in the contexts $Γ [S_{0}; U_{0}], x : α [U_{0}] and Γ [S_{0}; U_{0}; S_{1}], y : Var (ξ [U_{0}; S_{1}]),$ obtaining $(P_{1}, S_{1}, τ_{1})$ and $(P_{2}, S_{2}, τ_{2})$ , respectively. Finally solve $solve (Q_{0} [S_{1}; S_{2}] \cup P_{1} [S_{2}] \cup P_{2}; τ_{1} [S_{2}] ≐ τ_{2}) = (V, Q)$ and return $(Q, S_{0}; U_{0}; S_{1}; S_{2}; V, τ_{2} [V])$ .

Referenced from 7 locations

Lemma 7.38 — Fixed-choice determinism of qualified W ¶

With the two supplies just specified and the solver’s printed clause order, $W_{r} (Γ, e)$ has at most one result. If two runs instead use different legal fresh names, there is a unique sort-preserving renaming of the names they allocate, fixing every variable in $A$ , that carries one result and its induced typing derivation to the other.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 7.38 — Fixed-choice determinism of qualified W

Proof. Induct on $e$ . Its outer constructor selects exactly one W clause, and the clause fixes the order of recursive calls, substitutions, predicate normalizations, and solver work lists. The induction hypotheses identify the recursive results. The ordered solver is deterministic by definition 4.23; the fixed quantifier and predicate orders determine generalization at a let. Lambda, application, and the row-form clauses each consume their fresh names before the next recursive call, while the case clause consumes the scrutinee names, then the matching branch supply, then the residual branch supply. Hence the fixed-supply results are equal. For two legal supplies, pair their first choices at each corresponding clause. The induction extends this pairing once per allocation, producing the stated renaming and leaving all variables in $A$ fixed. ◻

Example 7.39 — Substitution order in a case ¶

Consider ${case}_{ℓ} ⟨ ℓ = zero ⟩ of {⟨ ℓ = x ⟩ \mapsto (λ z . z) x; y \mapsto (λ z . z) zero} .$ Injection gives a fresh tail $ξ_{0}$ and the predicate $ξ_{0} \ ℓ$ , so its result is $Var ({ℓ : Nat ∣ ξ_{0}})$ . The case clause chooses fresh $α, ξ_{1}$ and sends the equation $Var ({ℓ : Nat ∣ ξ_{0}}) ≐ Var ({ℓ : α ∣ ξ_{1}})$ to the solver. U-Type, U-Row, and I-Match expose the two equations $Nat ≐ α$ and $ξ_{0} ≐ ξ_{1}$ . The fixed variable orientations return $U_{0} = [Nat / α, ξ_{1} / ξ_{0}], Q_{0} = {ξ_{1} \ ℓ} .$ Hence the first branch is inferred under $x : Nat$ .

For $(λ z . z) x$ , choose fresh $β$ for the lambda domain and $γ$ for the application result. The generated equation is $β \to β ≐ Nat \to γ .$ Decomposition followed by the variable clauses gives $S_{1} = [Nat / β, Nat / γ]$ and branch type $Nat$ . The residual branch is then inferred under $Γ [U_{0}; S_{1}], y : Var (ξ_{1} [U_{0}; S_{1}]) = y : Var (ξ_{1}) .$ For $(λ z . z) zero$ , choose a disjoint fresh pair $δ, ε$ . The equation $δ \to δ ≐ Nat \to ε$ gives $S_{2} = [Nat / δ, Nat / ε]$ and the same branch type. The final equation is therefore $Nat ≐ Nat$ ; deletion returns $V = id$ . The algorithm returns $({ξ_{1} \ ℓ}, U_{0}; S_{1}; S_{2}, Nat) .$ Reading the postfix composite from left to right reproduces the computation: shape the scrutinee, solve the first branch, transport that result into the second branch, and finally equate the branch results. In a larger case the same positions are occupied by $U_{0}, S_{1}, S_{2}, V$ , yielding $S_{0}; U_{0}; S_{1}; S_{2}; V$ .

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Lemma 4.30 — Fresh support of qualified W ¶

Let $Z$ be a finite set of variables disjoint from $ftv (Γ)$ . A run of $W_{r} (Γ, e)$ may choose all fresh variables outside $Z$ ; its returned substitution is then the identity on $Z$ .

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.30 — Fresh support of qualified W

Proof. Induct on $e$ in the order of definition 4.29. Variable and constant instantiation return the identity, and a lambda changes only its freshly chosen domain variable and what the recursive call changes. At every sequential clause, pass to the later recursive call both $Z$ and the variables of earlier results that are not free in its input context. The induction hypothesis fixes them. Solver calls fix the same protected set by lemma 4.26; composition preserves that property. The let and case clauses differ only in the number of such successive calls. Thus no clause changes a protected variable. ◻

The first component of a let is not discarded. Its predicates travel in $σ$ and reappear, with its bound variables freshly instantiated, at each use of $x$ ; predicates mentioning the surrounding environment also remain in the returned residual set. This is qualified let polymorphism in exactly the same place where ordinary HM generalized type variables.

Example 4.31 — Inference of field-preserving extension ¶

Infer the body of $withSecure = λ r . {secure = true ∣ r}$ . Give $r$ fresh type $α$ . The extension clause infers $true : Bool$ and $r : α$ , then introduces fresh $ξ$ . Its equation $α ≐ Rec (ξ)$ and strictness condition give $P = {ξ \ secure}, τ = Rec (ξ) \to Rec ({secure : Bool ∣ ξ}) .$ Generalization quantifies $ξ$ , giving the scheme in example 4.14. Nothing in the calculation enumerates the untouched fields.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Definition 4.32 — Regular output of row inference ¶

Write $P ⊢_{reg} S : Γ$ when every image under $S$ of a variable free in $Γ$ is $P$ -formed and every declaration of $Γ [S]$ has its scheme body formed under the union of $P$ with its own predicate set. A triple $(P, S, τ)$ is regular for $Γ$ when $P$ is normalized, $P ⊢_{reg} S : Γ$ , and $P ⊢ τ type$ . The decorated turnstile is a regularity check, not another entailment relation.

Referenced from 3 locations

Lemma 4.33 — Restricted-support transport ¶

Suppose $P_{0}$ is normalized, every row $ρ$ occurring in a predicate $ρ \ ℓ \in P_{0}$ satisfies $P_{0} ⊢ ρ row$ , and $P_{0} ⊢ τ type$ for every type $τ$ in the finite list ${\bar{τ}}_{0}$ . Suppose also that $(P, S, τ)$ is regular for $Γ$ , and the fresh variables allocated by this run of W are disjoint from $ftv (P_{0}, {\bar{τ}}_{0}) ∖ ftv (Γ)$ . Put $Y = ftv (Γ, P_{0}, {\bar{τ}}_{0})$ and restrict $S$ to $Y$ , making it the identity elsewhere. Then $S |_{Y} : P_{0} \to nf (P_{0} [S] \cup P)$ is admissible, provided the displayed normalization succeeds, and the restriction agrees with $S$ on $Γ, P_{0}, {\bar{τ}}_{0}$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.33 — Restricted-support transport

Proof. A variable of $P_{0}$ or ${\bar{τ}}_{0}$ changed by $S |_{Y}$ either occurs in $Γ$ , in which case regularity forms its image, or would be a fresh variable of this run, which the disjointness condition excludes. Every other nonidentity component of $S$ has been discarded. The normalized union entails $P_{0} [S]$ . The global formation hypotheses therefore prove that the restriction is admissible. ◻

In applications of the lemma, the global fresh supply and lemma 4.30 establish its disjointness hypothesis before a later recursive call transports an earlier predicate set.

By lemma 4.11, an admissible $U : P \to Q$ sends a regular $(P, S, τ)$ to the regular $(Q, S; U, τ [U])$ . The restricted-support lemma explains why later calls may instead transport only the finite support actually used by an earlier premise.

Lemma 4.34 — Qualified generalization calculation ¶

Suppose $R : P \to P^{'}$ is admissible, $τ^{'} \equiv_{P^{'}} τ [R]$ , and $Γ^{'} = Γ [R]$ . Put $σ = {Gen}_{Γ} (P \Rightarrow τ)$ and $σ^{'} = {Gen}_{Γ^{'}} (P^{'} \Rightarrow τ^{'})$ . Freshen the prefix of $σ$ away from $R$ , and write $R \cdot σ$ for the scheme obtained by applying $R$ only to the free variables of $σ$ ; its displayed prefix remains bound. Every symbolic instance of $σ^{'}$ under a predicate context $Q$ entailing its instantiated predicates is also a symbolic instance of $R \cdot σ$ . Moreover, each predicate of $P^{r}$ is carried to a predicate entailed by $P^{'}$ . Consequently a qualified typing under $x : σ^{'}$ remains derivable after replacing that declaration by the more general $x : R \cdot σ$ in the already substituted surrounding context $Γ [R]$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.34 — Qualified generalization calculation

Proof. Let $X = ftv (P, τ) ∖ ftv (Γ)$ . Freshen $X$ away from the variables of $R$ and from the quantified prefix of $σ^{'}$ . A symbolic instance of $σ^{'}$ consists of a substitution $K$ on that latter prefix and an entailment of $P^{'} [K]$ . Instantiate each $z \in X$ in $R \cdot σ$ by $z [R; K]$ . This substitution is sorted and formed. Since $R : P \to P^{'}$ and $Q$ entails $P^{'} [K]$ , substitution stability gives $Q ⊩ nf (P [R; K])$ ; its result type is equal to $τ^{'} [K]$ by the displayed equality. Hence the chosen target instance is an instance of $R \cdot σ$ .

Each predicate in $P^{r}$ mentions a variable fixed by $Γ$ , so admissibility makes its $R$ -image a consequence of $P^{'}$ . For the final claim, induct on the body typing: only a leaf selecting $x$ changes, and the instance construction just given replaces it. ◻

Theorem 4.35 — Sound, complete, principal row inference ¶

Call a scheme context well formed when every declaration $\forall X . P \Rightarrow τ$ has $P ⊢ τ type$ , treating its unbound variables as parameters. For every such $Γ$ in the pure let-language with the saturated row forms of definition 4.13, definition 4.15:

Soundness. If $W_{r} (Γ, e) = (P, S, τ)$ , then $(P, S, τ)$ is regular for $Γ$ and $Γ [S] ⊢_{q} e : P \Rightarrow τ$ ;
Factorization. If $Γ [T] ⊢_{q} e : P^{'} \Rightarrow τ^{'}$ , where $T$ is sorted and its images and $Γ [T]$ are formed under $P^{'}$ , then W succeeds and, for its result $(P, S, τ)$ , there is an admissible $R : P \to P^{'}$ such that $T \equiv_{P^{'}} S; R$ on the variables of $Γ$ , $τ^{'} \equiv_{P^{'}} τ [R]$ , and $P^{'}$ entails every predicate of $nf (P [R])$ (spelling out the predicate-entailment component of admissibility);
Failure. W fails exactly when there is no qualified typing of this form under any $P^{'}, T, τ^{'}$ .

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Theorem 4.35 — Sound, complete, principal row inference

Proof. We prove soundness, regularity, and factorization simultaneously by induction on the term $e$ , following the clause order of definition 4.29. In the factorization assertion, the comparison substitution is admissible from the returned predicate context to the target context; equality between composite substitutions means pointwise $P^{'}$ -equivalence as in definition 4.8. Final uses of Q-Conv in the target derivation are stripped before inversion and restored by transitivity.

The induction invariant at every recursive call has two support clauses. Let $V_{sur}$ contain the variables needed by the surrounding factorization and let $V_{rec}$ contain the variables in the recursive input. First, $Z = V_{sur} ∖ V_{rec} .$ Second, the recursive substitution fixes $Z$ , and its residual factor is extended on $Z$ by the target solution. Lemma 4.26, Lemma 4.30 preserve the first clause; admissible composition and restricted-support transport preserve the second. Alongside these support clauses, regularity states that every returned type, predicate context, and substitution image is formed at its displayed target context. These are the recursive hypotheses used in every case below.

For each term form, inversion gives the equation in the middle column. Theorem 4.27 factors its target solution through the substitution returned by W; the last column records that factorization.

term form	constraint or fresh choice	factorization step
$x$	fresh scheme instance	map fresh variables to the target instance
$λ x . e$	fresh domain $α$	extend the target map by $α \mapsto A$
$e_{1} e_{2}$	$τ_{1} ≐ τ_{2} \to β$	factor the target arrow equation
$let x = e_{1} in e_{2}$	$Gen (P_{1} \Rightarrow τ_{1})$	qualified generalization, then the body factor
${}$	none	identity
${ℓ = e_{1} ∣ e_{2}}$	$τ_{2} ≐ Rec (ξ)$	factor the record-row equation
$e . ℓ$ , $e - ℓ$	$τ ≐ Rec ({ℓ : α ∣ ξ})$	factor the exposed-field equation
$⟨ ℓ = e ⟩$	fresh tail $ξ$	map $ξ$ to the target tail
${embed}_{ℓ} e$	$τ ≐ Var (ξ)$	factor the old-variant row
${case}_{ℓ} e of \dots$	scrutinee exposure and branch equality	compose three solver factors

The context invariance of lemma 4.10 permits every recursive target typing to be rebuilt under the compared composite context. Thus, if the second recursive call returns $S_{2}$ under $P_{2}$ , its fresh variables are disjoint from the earlier $P_{1}, τ_{1}$ , and lemma 4.33 proves that $S_{2} |_{Y} : P_{1} \to nf (P_{1} [S_{2}] \cup P_{2})$ is admissible on the support of the transported premise. On every variable occurring in those premise types, $S_{2} |_{Y}$ and $S_{2}$ agree, so those types may be written with $S_{2}$ . Subsequent solver maps compose by lemma 4.11.

For a variable, W replaces the quantified prefix by fresh variables. Rule Q-Var types this instance under its fresh predicate set. Any target leaf first applies the outer substitution $T$ to $Γ (x)$ , then chooses formed types and strict rows for its quantified prefix. Define the residual factor to agree with $T$ on the free variables of the original declaration and send W’s fresh prefix variables to those instance choices. Thus $S; R$ agrees with $T$ on $Γ (x)$ ; the target entailment premise proves that this map is admissible and gives the required type equality. Formation of the instance also proves regularity. Constants are identical, using Q-Const.

For $λ x . e_{0}$ , W assigns $x$ a fresh $α$ . The soundness induction hypothesis gives $Γ [S], x : α [S] ⊢_{q} e_{0} : P \Rightarrow τ,$ so Q-Lam gives the returned $α [S] \to τ$ . Conversely, inversion of a target lambda typing yields a domain $A$ and a typing of the body under $x : A$ . Extend the target substitution by $α \mapsto A$ and apply the body factorization. Removing the fresh component again gives the required factor on $Γ$ . Regularity follows from the formed domain image and the body result type.

For $e_{1} e_{2}$ , the two soundness hypotheses, transported through $S_{2}$ , give types $τ_{1} [S_{2}]$ and $τ_{2}$ . The solver returns $U$ with $τ_{1} [S_{2}; U] \equiv_{Q} τ_{2} [U] \to β [U]$ and with $Q$ entailing the transported premise constraints. Predicate weakening, Q-App, and Q-Conv therefore type the application at $β [U]$ . For factorization, invert a target application typing. The two recursive factorizations make its function and argument types an admissible solution of precisely the arrow equation and predicate set passed to the solver. The solving clause of theorem 4.27 factors that solution through $U$ ; composing the three factors gives $R$ . The regularity hypotheses prove that $P_{1} [S_{2}] \cup P_{2}$ is formed, and the solver theorem proves that $U$ is admissible from that context to $Q$ ; hence the returned composite and result type are regular.

At a let, soundness for the bound expression gives $Γ [S_{1}] ⊢_{q} e_{1} : P_{1} \Rightarrow τ_{1}$ . Generalize the variables absent from $Γ [S_{1}]$ and retain $P_{1}^{r}$ . Put $Q_{L} = nf (P_{1}^{r} [S_{2}] \cup P_{2}) .$ Regularity of the body call gives $P_{2}$ -formation derivations for the $S_{2}$ -images of variables free in $Γ [S_{1}]$ . Let $F \subseteq P_{2}$ be the normalized set of assumption leaves used by those derivations. With $P_{1}^{S} = nf (P_{1} [S_{2}] \cup F),$ the restricted-support transport observation types $e_{1}$ under $P_{1}^{S}$ . Predicate weakening moves the body hypothesis from $P_{2}$ to $Q_{L}$ , and lemma 4.12 replaces its declaration by ${Gen}_{Γ [S_{1}; S_{2}]} (P_{1}^{S} \Rightarrow τ_{1} [S_{2}]) .$ Now Q-Let returns $Q_{L}$ : the residual part of $P_{1}^{S}$ is $P_{1}^{r} [S_{2}] \cup F$ , already contained in or entailed by $Q_{L}$ . For principality, let $R_{1}$ be the factor returned by the first recursive call. The target declaration for $e_{1}$ is an instance of $R_{1} \cdot {Gen}_{Γ [S_{1}]} (P_{1} \Rightarrow τ_{1})$ by lemma 4.34; its non-generalizable predicates occur in the target let conclusion. Replace that target declaration by this more general substituted scheme, apply the body factorization, and compose. Regularity of $S_{2}$ and retention of $P_{1}^{r} [S_{2}]$ form the returned context and result. This is the ordinary HM let argument with the residual set carried in every displayed step.

The empty record is immediate from Q-Empty. For ${ℓ = a ∣ r}$ , transport the two soundness hypotheses through $S_{2}$ and then $U$ . The solver equation types the second term as $Rec (ξ [U])$ , and $Q$ entails $ξ [U] \ ℓ$ . Rule Q-Extend yields $Rec ({ℓ : τ_{1} [S_{2}; U] ∣ ξ [U]}),$ the returned type. A target extension typing, after inversion, contains a payload type, a residual record row, and the corresponding lacks judgment. The two recursive factors turn these data into an admissible solution of the solver call in the extension clause. Principal constrained unification then yields a factor $R$ through which that solution factors.

For $r . ℓ$ , soundness first gives $Γ [S] ⊢_{q} r : P \Rightarrow τ$ . Solver soundness gives $τ [U] \equiv_{Q} Rec ({ℓ : α [U] ∣ ξ [U]}),$ and both sides are formed under $Q$ ; solver admissibility transports the input typing from $P$ to $Q$ . The returned context also records the strictness predicate for $ξ [U]$ . Conversion followed by Q-Select therefore gives the returned type $α [U]$ . Conversely, inversion of a target selection exposes a unique field $Rec ({ℓ : A ∣ ρ})$ and its lacks judgment. Together with the recursive factor for $r$ , these are a solution of the displayed solver call; its principal factorization gives $R$ . Restriction begins with the same exposure, but Q-Restrict returns $Rec (ξ [U])$ . In the converse direction, the exposed target tail $ρ$ is therefore the image of the fresh $ξ$ ; no additional equation is needed.

For $⟨ ℓ = a ⟩$ , use the induction hypothesis for the payload, choose the fresh $ξ$ , and apply Q-Inject. Given any target injection typing, map that fresh $ξ$ to its residual row $ρ$ . The target lacks premise is $ℓ \notin ρ$ , so the map is admissible and the returned row and constraint are most general. For ${embed}_{ℓ} u$ , the recursive hypothesis types the old variant. The solver returns $U$ with $ξ [U] = ρ$ and records $ℓ \notin ρ$ ; Q-Embed adds the fresh alternative of type $α [U]$ . Inverting a target embedding derivation gives the same row equation and lacks predicate. The solver theorem therefore gives its factorization.

Finally consider a case. The first solver and the scrutinee hypothesis give $Γ [S_{0}; U_{0}] ⊢_{q} u : Q_{0} \Rightarrow Var ({ℓ : α [U_{0}] ∣ ξ [U_{0}]}) .$ The two recursive hypotheses type the branches in the two contexts printed in definition 4.29. Transport the first branch through $S_{2}$ ; soundness of the last solver call equates its type with the second branch type and combines all three predicate sets. Rule Q-Case, followed by conversion, gives $τ_{2} [V]$ . Inverting a target case typing gives its selected field, residual variant, and common branch type. Principal factorization of the scrutinee solver fixes the two branch contexts; the two branch induction hypotheses then factor their typings; the final solver factors the equality of their result types. Their ordered composite is the required $R$ .

In every row clause, the recursive triples are formed, transport proves each intervening substitution admissible, and solver soundness proves formation of the returned row and type. In the case clause the admissible substitutions are, successively, $S_{0}; U_{0}$ , $S_{0}; U_{0}; S_{1}$ , $S_{0}; U_{0}; S_{1}; S_{2}$ , and finally the admissible composite $S_{0}; U_{0}; S_{1}; S_{2}; V$ . Thus no composite used in the soundness argument is merely a sorted raw substitution.

At the first failing recursive or solver call, the corresponding induction hypothesis or factorization theorem rules out the inverted target typing. Two clauses can instead fail while normalizing predicates. In the let clause, an inverted target typing supplies a formed normalized union of the residual definition predicates and body predicates, so the requested normalization must exist. In the injection clause, the target Q-Inject premise supplies a formed residual row lacking the injected label, so adjoining and normalizing that lacks predicate must also succeed. Hence either normalization failure rules out the corresponding target typing. Therefore W fails exactly when no qualified typing exists. ◻

This theorem is deliberately limited to pure let. If references from section 3.9 are added, the same conservative value restriction must be applied to qualified schemes; a row constraint does not make allocation pure.

Exercise 4.6 ¶

★★☆ Run $W_{r}$ on $λ x . {embed}_{error} ⟨ ok = x ⟩ .$ Keep the independently fresh row tails introduced by injection and embedding until unification identifies them. Give the principal qualified scheme and explain why neither $ok$ nor $error$ may occur in its residual tail.

Referenced from 3 locations

Offset evidence and one concrete implementation

So far, $ξ \ ℓ$ has been used as a proposition. It also tells the compiler where an $ℓ$ field would be inserted into a canonical layout of $ξ$ . Fix a decidable total order $<$ on labels; store record fields in increasing order, and tag a variant by the zero-based position of its label in that order.

Elaboration reifies a proof of absence as an offset expression. The context $Δ$ contains variables standing for assumed lacks predicates, and the judgment $Δ ⊢ d : ρ \ ℓ$ reads: from those assumptions, expression $d$ computes the insertion offset of $ℓ$ in $ρ$ . Thus predicates remain static propositions in the source, while their derivations produce integer evidence for the target.

Definition 4.36 — Evidence for lacks ¶

A predicate assignment $Δ$ contains at most one variable $d_{ξ, ℓ}$ for each residual predicate $ξ \ ℓ$ . Evidence is computed by

d_{ξ, ℓ} : ξ \ ℓ \in Δ

Δ ⊢ d_{ξ, ℓ} : ξ \ ℓ

Ev-Assume

Δ ⊢ 0 : ϵ_{ρ} \ ℓ

Ev-Empty

Δ ⊢ d : ρ \ ℓ

ℓ < m

Δ ⊢ d : {m : τ ∣ ρ} \ ℓ

Ev-Before

Δ ⊢ d : ρ \ ℓ

m < ℓ

Δ ⊢ d + 1 : {m : τ ∣ ρ} \ ℓ

Ev-After

The evidence is the insertion offset for $ℓ$ . The two inequalities are exhaustive because a derivable lacks predicate rules out $m = ℓ$ .

Referenced from 4 locations

An affine evidence expression in this chapter has one of the forms $n$ or $d_{ξ, ℓ} + n$ , with $n \in N$ . Addition of zero is omitted. We call evidence coherent when all derivations of the same lacks judgment normalize to the same such expression.

For $ρ = {host : String, port : Nat}$ , suppose $host < port < secure$ . The evidence for $ρ \ secure$ is $0 + 1 + 1 = 2$ ; inserting the field at offset 2 appends it to the canonical two-field array. If the labels are displayed in another row order, the same comparison count gives the same answer.

Lemma 4.37 — Evidence coherence ¶

Let $P$ be normalized, and let $Δ_{P}$ contain one evidence variable for each predicate. Any two evidence derivations of $Δ_{P} ⊢ d : ρ \ ℓ$ yield the same affine expression in the variables of $P$ . This expression is invariant under every adjacent exchange of distinct displayed fields, hence under every presentation of the same strict finite row. For a closed row, that expression is the numeral $# {m \in labels (ρ) ∣ m < ℓ} .$

Referenced from 5 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.37 — Evidence coherence

Proof. Induct on the number of displayed fields of $ρ$ . At a row variable, normalization leaves exactly the unique matching evidence variable. At the empty row both derivations end at $0$ . At a displayed field $m$ , the order decides uniquely whether to retain the tail expression or add one; apply the induction hypothesis to the tail. Adjacent exchange of two distinct labels preserves the number of labels smaller than $ℓ$ , so the result is independent of the chosen row display. The closed formula follows by ending at the empty row. ◻

Definition 4.38 — Evidence-passing target calculus ¶

The target is a call-by-value let calculus with static type abstraction and explicit offset arguments. Its monotypes are $θ ::= α ∣ Nat ∣ Bool ∣ String ∣ θ \to θ ∣ Array (ρ) ∣ Sum (ρ) .$ A normalized predicate context $P$ indexes target formation. Write $P ⊢_{t} θ type$ when every row index in $θ$ is a strict $P$ -formed row and every field type is recursively target-formed. A substitution $S : P \Rightarrow_{t} Q$ is target-admissible when it maps type variables to $Q$ -formed target types, maps row variables to $Q$ -formed strict rows, and $Q$ entails every normalized predicate in $P [S]$ . For each assumption variable in $Δ_{P}$ , that entailment has an evidence derivation in $Δ_{Q}$ ; write $\hat{S}$ for the simultaneous replacement by the canonical affine evidence expressions from lemma 4.37.

Fix the label order used by evidence. Let $sort (ρ)$ sort the finite displayed prefix of a strict row by label, preserve its row-variable or empty tail, and recursively canonicalize field types. Let $canTy (θ)$ apply this operation to every row index and recurse through arrows. Target type conversion is the exact rule

Δ; Γ ⊢ t : θ

canTy (θ) = canTy (θ^{'})

Δ; Γ ⊢ t : θ^{'}

T-Conv

Target types are therefore not an implicit quotient: the displayed judgment uses syntactic types plus this one conversion rule. Since sorting commutes with target-admissible substitution up to a final sort, formation and substitution preserve the premise of T-Conv. In particular, if $ρ \equiv_{P} ρ^{'}$ , then $sort (ρ) = sort (ρ^{'})$ , and both $Array$ and $Sum$ convert between the two indices.

A target scheme has form $\forall X . Off (P) \Rightarrow θ,$ where $Off (P)$ is one offset-certificate argument for each member of the normalized set $P$ . Order these members first by the fixed order of their row variables and then by the label order $<$ . A target context may contain such schemes. The target term grammar is explicit: $\begin{aligned} t ::= & x ∣ c ∣ λ x . t ∣ t t ∣ let x = t in t \\ ∣ Λ X . λ \bar{d} . t ∣ t [T] \bar{d} \\ ∣ [] ∣ lookup d t ∣ delete d t \\ ∣ insert d t t ∣ tag d t \\ ∣ widen d t ∣ split d t t t . \end{aligned}$ The forms $Λ X . t$ and $t [T]$ are static type abstraction and application. Type abstraction erases; evidence lambdas execute at run time. Thus static instantiation may follow any term that evaluates to a scheme abstraction, while every data primitive is a saturated term former. The scheme rules are

Γ (x) = σ

Δ; Γ ⊢ x : σ

T-Var

c : θ \in Σ_{0}

Δ; Γ ⊢ c : θ

T-Const

Δ; Γ ⊢ t : \forall X . Off (P) \Rightarrow θ

T is sorted and formed

Δ ⊢ \bar{d} : Off (P [T])

Δ; Γ ⊢ t [T] \bar{d} : θ [T]

T-Inst

Δ, \bar{d} : Off (P); Γ ⊢ t : θ

X \cap ftv (Δ, Γ) = \emptyset

Δ; Γ ⊢ Λ X . λ \bar{d} . t : \forall X . Off (P) \Rightarrow θ

T-Ev-Abs

Δ; Γ ⊢ t_{1} : σ

Δ; Γ, x : σ ⊢ t_{2} : θ

Δ; Γ ⊢ let x = t_{1} in t_{2} : θ

T-Let

We identify a monotype $θ$ with the empty scheme $\forall \emptyset . Off (\emptyset) \Rightarrow θ$ . Instantiation of this empty scheme emits no target syntax: a monomorphic variable leaf elaborates to $x$ , and a monomorphic constant leaf to $c$ . The form $t [T] \bar{d}$ is emitted only when the type prefix or evidence tuple is nonempty. Dually, an empty abstraction emits no wrapper: $Λ \emptyset . λ \emptyset . t$ is represented simply by $t$ . Thus lambda-bound variables and monomorphic let bindings remain ordinary; an expression such as $(λ x . x) c$ does not reduce to a spurious static application of the base value $c$ . Here the type variables $X$ are parameters in the premise of T-Ev-Abs. The monomorphic variable, constant, lambda, and application rules, with the evidence context copied unchanged, are $\begin{matrix} \frac{Γ (x) = θ}{Δ; Γ ⊢ x : θ} T - MVar \frac{c : θ \in Σ_{0}}{Δ; Γ ⊢ c : θ} T - MConst \\ \frac{Δ; Γ, x : θ ⊢ t : υ}{Δ; Γ ⊢ λ x . t : θ \to υ} T - Lam \\ \frac{\begin{matrix} Δ; Γ ⊢ t : θ \to υ \\ Δ; Γ ⊢ u : θ \end{matrix}}{Δ; Γ ⊢ t u : υ} T - App . \end{matrix}$ The binder $Λ X$ is static and erases; the evidence lambdas remain ordinary run-time lambdas. Thus this is ML let polymorphism with explicit predicate arguments, not first-class polymorphism. Scheme abstractions are values, and their application computes by $(Λ X . λ \bar{d} . t) [T] \bar{n} ⟶ t [T / X, \bar{n} / \bar{d}] .$ Together with the ordinary call-by-value let contraction, this is the whole extra dynamics for schemes.

Referenced from 5 locations

Lemma 7.49 — Canonical target indices ¶

Let $P, Q$ be normalized and let $S : P \Rightarrow_{t} Q$ be target-admissible. Then the following properties hold.

If strict rows satisfy $ρ \equiv_{P} ρ^{'}$ , then $sort (ρ) = sort (ρ^{'})$ .
For every $P$ -formed target type $θ$ , $canTy (θ [S]) = canTy (canTy (θ) [S]) .$
If $Δ_{P}; Γ ⊢ t : θ$ , then

$Δ_{Q}; Γ [S] ⊢ t [S, \hat{S}] : θ [S] .$

Target formation is likewise stable under $S$ . A type in a judgment may also be replaced by a $Q$ -formed type with the same $canTy$ -image.

Referenced from 5 locations

Proof of Lemma 7.49 — Canonical target indices

Proof. For item 1, use the finite-map characterization of strict row equality in lemma 4.5. Both sorts list the same label–type map in the fixed label order and retain the same tail. For item 2, induct on $θ$ . The arrow case uses the two induction hypotheses. In an array or sum case, substitution may expose a displayed prefix from a row variable; the final call to $sort$ merges that prefix with the surrounding fields, so both sides list the same finite map in the same order.

For item 3, induct on the target formation or typing derivation. Target-admissibility supplies formed images in variable and row-index cases. At an evidence premise, substitute the corresponding component of $\hat{S}$ ; its derivation exists by the defining entailment of $S : P \Rightarrow_{t} Q$ . Every other syntax-directed rule follows from its induction hypotheses. In the T-Conv case, item 2 transports equality of canonical images through $S$ . Replacement by an equal canonical image is one further application of T-Conv. Thus a raw sort-preserving map such as $S (ξ) = {a : Nat, a : Bool}$ is excluded: its row image is not $Q$ -formed. ◻

Definition 7.50 — Target row primitives ¶

Run-time values additionally include arrays $[w_{0}, \dots, w_{n - 1}]$ and tagged payloads $⟨ i, w ⟩$ . If $Δ ⊢ d : ρ \ ℓ$ , the nullary array constructor and lookup rule are

Δ; Γ ⊢ [] : Array (ϵ_{ρ})

T-Empty

Δ; Γ ⊢ r : Array ({ℓ : α ∣ ρ})

Δ ⊢ d : ρ \ ℓ

Δ; Γ ⊢ lookup d r : α

T-Lookup

The other five saturated rules are $\begin{matrix} \frac{\begin{matrix} Δ; Γ ⊢ r : Array ({ℓ : α ∣ ρ}) \\ Δ ⊢ d : ρ \ ℓ \end{matrix}}{Δ; Γ ⊢ delete d r : Array (ρ)} T - Delete \\ \frac{\begin{matrix} Δ; Γ ⊢ a : α \\ Δ; Γ ⊢ r : Array (ρ) \\ Δ ⊢ d : ρ \ ℓ \end{matrix}}{Δ; Γ ⊢ insert d a r : Array ({ℓ : α ∣ ρ})} T - Insert \\ \frac{\begin{matrix} Δ; Γ ⊢ a : α \\ Δ ⊢ d : ρ \ ℓ \end{matrix}}{Δ; Γ ⊢ tag d a : Sum ({ℓ : α ∣ ρ})} T - Tag \\ \frac{\begin{matrix} Δ; Γ ⊢ u : Sum (ρ) \\ Δ ⊢ d : ρ \ ℓ \end{matrix}}{Δ; Γ ⊢ widen d u : Sum ({ℓ : α ∣ ρ})} T - Widen \\ \frac{\begin{matrix} Δ; Γ ⊢ u : Sum ({ℓ : α ∣ ρ}) \\ Δ; Γ ⊢ f : α \to β \\ Δ; Γ ⊢ g : Sum (ρ) \to β \\ Δ ⊢ d : ρ \ ℓ \end{matrix}}{Δ; Γ ⊢ split d u f g : β} T - Split . \end{matrix}$ Each displayed primitive rule includes its evidence premise. There is therefore no term such as a half-applied $lookup d$ : it is neither syntax nor a possible stuck state.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Definition 7.51 — Target dynamics and canonical values ¶

Ground arrays use increasing label order. For $A = [a_{0}, \dots, a_{n - 1}]$ , write $A [i]$ for zero-based indexing when $0 \leq i < n$ , and write $A ∖ i$ for deletion at such an index. For $0 \leq i \leq n$ , define the length-increasing insertion operation ${ins}_{i} (v, A) = [a_{0}, \dots, a_{i - 1}, v, a_{i}, \dots, a_{n - 1}],$ with the empty prefix understood at $i = 0$ and the empty suffix at $i = n$ . The primitive reductions are $\begin{aligned} lookup i A & ⟶ A [i], \\ delete i A & ⟶ A ∖ i, \\ insert i v A & ⟶ {ins}_{i} (v, A), \\ tag i v & ⟶ ⟨ i, v ⟩, \\ widen i ⟨ j, v ⟩ & ⟶ {\begin{cases} ⟨ j, v ⟩ & j < i, \\ ⟨ j + 1, v ⟩ & i \leq j, \end{cases} \end{aligned}$ and $split i ⟨ j, v ⟩ f g ⟶ {\begin{cases} f v & j = i, \\ g ⟨ j, v ⟩ & j < i, \\ g ⟨ j - 1, v ⟩ & i < j . \end{cases}$ The compatible closure is left-to-right call by value. Besides the ordinary application and let contexts it evaluates the head of $t [T] \bar{n}$ , the single data argument of lookup, delete, tag, and widen, the two arguments of insert in their printed order, and the scrutinee and two branch functions of split in their printed order. These contexts contain only saturated primitive forms. Evidence expressions are stored in the canonical affine form $d_{ξ, ℓ} + n$ or $n$ ; after a ground assignment they are numerals. Rule T-Empty types the empty array. A ground canonical array has type $Array (ρ)$ exactly when its entries, in increasing label order, have the field types of $ρ$ . Likewise $⟨ i, v ⟩ : Sum (ρ)$ exactly when position $i$ of the sorted row $ρ$ carries the type of $v$ . These clauses type every target value produced by the reductions above.

Referenced from 4 locations

At row ${host : String}$ , two primitive rules compute immediately: $lookup 0 ["db"] \overset{l o o k u p}{⟶} "db", tag 0 true \overset{t a g}{⟶} ⟨ 0, true ⟩ .$

Definition 4.39 — Canonical offset representation ¶

Translate rows and types simultaneously: $\begin{aligned} lay (ξ) & = ξ, & lay (ϵ_{ρ}) & = ϵ_{ρ}, \\ lay ({ℓ : τ ∣ ρ}) & = sort ({ℓ : lay (τ) ∣ lay (ρ)}), \\ lay (Rec (ρ)) & = Array (lay (ρ)), \\ lay (Var (ρ)) & = Sum (lay (ρ)), \\ lay (τ \to υ) & = lay (τ) \to lay (υ) . \end{aligned}$ Base types and variables are unchanged. Thus every row output of $lay$ is canonical even when the source display is not, and row-equal displays have literally the same layout. An entailment derivation $P ⊩ ρ \ ℓ$ determines, by definition 4.36, a target evidence term from the variables for $P$ . Write it $d_{P, ρ, ℓ}$ . Send a source declaration $x : \forall X . P \Rightarrow τ$ to $x : \forall X . Off (P) \Rightarrow lay (τ)$ .

For example, $lay (Rec ({port : Nat, host : String})) = Array ({host : String, port : Nat}),$ where the last row is in canonical label order.

The canonicalization function $can (t)$ identifies target terms that differ only by row order or affine presentation: it sorts every strict row in a target type or static argument and reduces each offset expression to affine normal form. This is meta-level normalization of annotations and evidence, not an additional run-time reduction. Its type component is exactly $canTy$ , so the only typing equality it uses is the displayed T-Conv rule.

Referenced from 5 locations

Definition 7.53 — Unambiguous evidence interface ¶

An open qualified judgment is unambiguous when $ftv (P) \subseteq ftv (Γ, τ) .$ For a closed scheme $\forall X . P \Rightarrow τ$ , this specializes to $ftv (P) \subseteq ftv (τ)$ . The evidence-passing compiler accepts a principal inference result only when this condition holds. An ambiguous result remains a valid source typing and is covered by source safety, but it does not determine its evidence interface from the visible environment and result type.

Referenced from 4 locations

For instance, the closed scheme $\forall ξ . ξ \ ℓ \Rightarrow Nat$ is ambiguous: its result contains no occurrence of $ξ$ , so two ground instances may require different offsets although the visible result type is the same. The compiler rejects this evidence interface rather than choosing one offset invisibly.

Definition 4.40 — Evidence elaboration ¶

The elaboration is defined on a typing derivation. At a variable or constant leaf, instantiate its scheme and apply the selected evidence tuple. Lambda and application elaborate homomorphically. At a let, replace the bound expression by $Λ X . λ \bar{d} : Off (P_{1}) . e_{1}^{†},$ where $X$ is the generalized prefix; the body uses this scheme at each fresh instance. When $X = P_{1} = \emptyset$ , use $e_{1}^{†}$ itself, in accordance with the empty-scheme convention. Final row conversion emits no term. The empty constructor and the six evidence-carrying row forms become $\begin{array}{cc} source & target at evidence d \\ {} & [] \\ r . ℓ & lookup d r \\ r - ℓ & delete d r \\ {ℓ = v ∣ r} & insert d v r \\ ⟨ ℓ = v ⟩ & tag d v \\ {embed}_{ℓ} v & widen d v \\ {case}_{ℓ} v of {f; g} & split d v f g . \end{array}$ Here $d = d_{P, ρ, ℓ}$ is the evidence term of definition 4.39 for the final normalized predicate context at that source rule; it is well defined up to the equality used by the target through lemma 4.37. In the case translation, $f$ and $g$ are the elaborated branch lambdas. These seven clauses, together with the four pure-let clauses, are the complete translation.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Example 4.41 — Compiling field-preserving extension ¶

Keep the label order $host < port < secure$ . At the ground row $ρ = {host : String}$ , the evidence for $ρ \ secure$ is $1$ . The source calculation is $withSecure {host = "db" ∣ {}} ⟶^{*} {secure = true ∣ {host = "db" ∣ {}}} .$ Its elaborated generalized value is $Λ ξ . λ d : Off (ξ \ secure) . λ r . insert d true r .$ Instantiating the static row, supplying its certified offset, and applying the resulting function gives the complete target trace. In this display $[ρ]$ is static type application, whereas $["db"]$ is the array-value notation introduced in definition 7.50. $\begin{aligned} ((Λ ξ . λ d . λ r . insert d true r) [ρ] 1) ["db"] \\ \overset{s c h e m e - β}{⟶} (λ r . insert 1 true r) ["db"] \\ \overset{β}{⟶} insert 1 true ["db"] \overset{i n s e r t}{⟶} ["db", true] . \end{aligned}$ The last array is the sorted representation of the source result. The unmentioned $host$ field survives because the offset operation inserts rather than rebuilds the record from a closed list of labels.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

The tempting lockstep theorem is false. If the source bound expression steps as $e_{1} ⟶ e_{1}^{'}$ , then $let x = e_{1} in e_{2} ⟶ let x = e_{1}^{'} in e_{2},$ whereas its generalized target binding stores $let x = Λ X . λ \bar{d} . e_{1}^{†} in e_{2}^{†};$ the bound scheme abstraction is already a target value, so a step-for-step simulation is false. We instead relate final values and, at a scheme, quantify over every ground instance and its canonical evidence.

Definition 4.42 — Ground value relation ¶

Fix an admissible ground substitution. For each resulting ground type $τ$ , define a relation $R_{τ}$ on source and target values. Base constants relate only to themselves. At a record type, sort the source map by label; it relates to an array when matching entries relate. At a variant type, let the unique field at $ℓ$ have type $α$ . Then $⟨ ℓ = v ⟩$ relates to $⟨ i, w ⟩$ when $v R_{α} w$ and $i$ counts the row labels below $ℓ$ . Finally, $f R_{τ \to υ} g$ when, for every $a R_{τ} b$ , the two applications evaluate to values related by $R_{υ}$ .

A source value and a target scheme value are related at $\forall X . P \Rightarrow τ$ when, for every ground, formed instantiation of $X$ satisfying $P$ , application of the target value to its canonical evidence tuple evaluates to a value related to the source value at the instantiated type. Source and target environments are related when their values are related at every declaration. This last clause is the invariant needed at a polymorphic let.

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

The fundamental lemma proves that every closed grounded source term and its elaboration reach related values. Purity and absence of recursion make this total value relation sufficient; references or recursion would require a partial or step-indexed relation instead.

Lemma 4.43 — The six offset simulations ¶

Let $ρ$ be a strict ground row lacking $ℓ$ , and let $i$ be the number of labels of $ρ$ smaller than $ℓ$ . The source row operations and the target operations at offset $i$ preserve the ground value relation. More precisely:

the empty source record and the empty target array are related at $Rec (ϵ_{ρ})$ and $Array (ϵ_{ρ})$ , respectively;
related fields and records remain related after source extension and target insertion;
selection and lookup return related fields, while restriction and deletion return related residual records;
injection and tagging return related variants;
embedding and widening return related variants; and
suppose the distinguished and residual source branch functions are related to target functions $f$ and $g$ at $α \to β$ and $Var (ρ) \to β$ , respectively. Then source case analysis and target split evaluate to related results.

Referenced from 5 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.43 — The six offset simulations

Proof. The first clause is the empty-list instance of the record relation. Sort the labels of $ρ$ as $ℓ_{0} < \dots < ℓ_{n - 1}$ . By definition of the record relation, a source record $R = {ℓ_{0} = v_{0}, \dots, ℓ_{n - 1} = v_{n - 1}}$ relates to $A = [w_{0}, \dots, w_{n - 1}]$ precisely when $v_{j} R w_{j}$ at the field type carried by $ℓ_{j}$ . Inserting a related field $v R_{α} w$ at position $i$ gives the sorted lists ${ℓ = v ∣ R} R {ins}_{i} (w, A) .$ This proves the extension clause. In a record already containing $ℓ$ at position $i$ , source selection scans to the same field that $lookup i$ indexes, and source restriction removes the same entry that $delete i$ removes. This proves the three record-operation clauses.

Injection is immediate: the new label has position $i$ , so $⟨ ℓ = v ⟩$ relates to $⟨ i, w ⟩$ . For embedding, let an old label $m$ have position $j$ in $ρ$ . Its position in ${ℓ : α ∣ ρ}$ is $j$ when $m < ℓ$ , and $j + 1$ when $ℓ < m$ . These are exactly the two clauses of $widen$ .

It remains to check case analysis. Let the larger-row target value be $⟨ j, w ⟩$ . There are three possibilities. If $j = i$ , its source mate is $⟨ ℓ = v ⟩$ ; source case takes the distinguished branch and target split reduces to $f w$ . The arrow relation for the two distinguished branch functions gives related results. If $j < i$ , the carried source label is smaller than $ℓ$ and already has residual-row position $j$ ; split passes $⟨ j, w ⟩$ to $g$ . If $i < j$ , removing the inserted position lowers the residual tag to $j - 1$ ; split passes $⟨ j - 1, w ⟩$ to $g$ . In the last two cases this target value is precisely the mate of the whole residual source variant passed to the residual branch. Its arrow relation gives the required result. This exhausts the six operations. ◻

Lemma 4.44 — Typing of evidence elaboration ¶

Let $D$ derive $Γ ⊢_{q} e : P \Rightarrow τ$ , and let $Δ_{P}$ contain one evidence variable for every member of normalized $P$ . Then $Δ_{P}; lay (Γ) ⊢ D^{†} : lay (τ) .$

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.44 — Typing of evidence elaboration

Proof. Induct on $D$ . The Q-Empty case elaborates to ([ ]) and uses T-Empty. In Q-Var, translate each entailed instantiated predicate to its evidence expression; T-Var followed by T-Inst then has exactly the displayed result type when the scheme is genuine; for the empty scheme the convention in definition 4.38 uses T-Var alone. The nullary Q-Const instances use the target constant rule. Lambda and application use the ordinary target rules. Conversion emits no term: item 1 of lemma 7.49 makes the two layouts identical, and T-Conv transports the target typing.

For Q-Let, if the generalized prefix and $P_{1}$ are both empty, the two induction hypotheses and T-Let give the ordinary monomorphic let directly. Otherwise apply the first induction hypothesis under fresh evidence variables for all of $P_{1}$ and use T-Ev-Abs. This types $Λ X . λ \bar{d} : Off (P_{1}) . D_{1}^{†} : \forall X . Off (P_{1}) \Rightarrow lay (τ_{1}) .$ The evidence context for $nf (P_{1}^{r} \cup P_{2})$ projects the tuple needed by the body derivation. The second induction hypothesis and T-Let finish the case. The abstraction takes the whole $P_{1}$ tuple; its residual part also remains available outside the let.

For extension, the two induction hypotheses type the field value and record array. The normalized conclusion contains an evidence term for $ρ \ ℓ$ , so the type of $insert$ gives the translated result. Selection and restriction use lookup and delete with the same certificate. Injection and embedding use tag and widen. In the case rule, the two branch hypotheses type the lambdas $λ x . D_{1}^{†}$ and $λ y . D_{2}^{†}$ at the two argument types of split; T-Split then returns $lay (β)$ . ◻

Lemma 4.45 — Fundamental evidence lemma ¶

Let $D$ derive $Γ ⊢_{q} e : P \Rightarrow τ$ . Let $G : P \to \emptyset$ be an admissible ground substitution, let $\bar{n}$ be its canonical evidence tuple, and let source and target environments $γ, η$ be related at $Γ [G]$ . Then there are values $v, w$ with $e [γ] ⟶^{*} v, G (D^{†}) [\bar{n} / Δ_{P}, η] ⟶^{*} w, v R_{τ [G]} w .$

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

Proof of Lemma 4.45 — Fundamental evidence lemma

Proof. Induct on $D$ . The Q-Empty case evaluates to the empty source record and the empty target array; they are related by the first clause of lemma 4.43. At a variable leaf, the related-environment hypothesis relates the source value to the target scheme value. Applying the chosen ground instance and its canonical evidence tuple is exactly the scheme clause of definition 4.42. A constant evaluates to itself on both sides and is related at its declared base type.

For a lambda, take arbitrary related arguments $a$ and $b$ . Substitution extends the two environments by $x \mapsto a$ and $x \mapsto b$ ; the induction hypothesis for the body gives related results. Hence the two lambda values satisfy the arrow clause. In an application, the two induction hypotheses give $f R_{α \to β} g, a R_{α} b .$ The defining arrow clause, not a new operational argument, says that $f a$ and $g b$ evaluate to values related at $β$ .

At a let with empty generalized prefix and $P_{1} = \emptyset$ , the first induction hypothesis gives related source and target values for the bound expression; extend the two environments by those values and apply the body induction hypothesis. This is the ordinary monomorphic-let case.

Otherwise first extend the ground map to the generalized variables: send fresh type variables to $Nat$ and fresh row variables to the empty row. No row extension is required, because the empty row satisfies every normalized lacks predicate on those fresh variables. Together with the fixed ambient assignments, this is an admissible ground map for the first premise. Its induction hypothesis evaluates $e_{1} [γ]$ to a source value $v$ . Now take an arbitrary ground instantiation satisfying $P_{1}$ and apply the same induction hypothesis. It produces some source value $v_{T}$ and a target value obtained from $(Λ X . λ \bar{d} . D_{1}^{†}) [T] {\bar{n}}_{1} .$ The generalized variables are absent from the source environment and term, so both source evaluations start from the same expression. By lemma 7.28, $v_{T} = v$ . Since the ground instantiation was arbitrary, the fixed source value $v$ and the target abstraction satisfy the universally quantified scheme clause of definition 4.42. Extend $γ, η$ by them and apply the second induction hypothesis. The source evaluates $e_{1}$ once before substitution; the target abstraction may evaluate its pure body at each instance. The scheme relation makes these evaluations agree.

For extension, selection, restriction, injection, and embedding, apply the subterm induction hypotheses and the corresponding clause of lemma 4.43. In the case rule the scrutinee induction hypothesis proves that the two evaluated scrutinees are related variants. Apply the two branch induction hypotheses under arbitrary related values for $x$ , respectively $y$ ; by the lambda argument above, the elaborated branch lambdas are related to the two source branch functions. The case-analysis clause of lemma 4.43 now treats all three possible tag comparisons. In particular, the residual branch receives the unchanged tag below the inserted position and the decremented tag above it, exactly as the sorted residual row requires. Conversion changes only a row display, and lemma 4.5 leaves the relation unchanged. ◻

Theorem 4.46 — Preservation, adequacy, and coherence of evidence passing ¶

For every derivation $D$ of $Γ ⊢_{q} e : P \Rightarrow τ$ :

its elaboration has the target type stated in lemma 4.44;
if $Γ$ is empty and $G : P \to \emptyset$ is admissible and ground, then there are values $v, w$ such that $e ⟶^{*} v, G (D^{†}) [\bar{n} / Δ_{P}] ⟶^{*} w, v R_{τ [G]} w;$
if $D^{'}$ changes only the derivations of normalized lacks entailments or the display order of equal strict rows, then $can (D^{†}) = can ((D^{'})^{†})$ as literal target syntax.

Referenced from 4 locations

Row Polymorphism and Extensible Records and Variants

Proof of Theorem 4.46 — Preservation, adequacy, and coherence of evidence passing

Proof. Item 1 is lemma 4.44. For item 2, apply lemma 4.45 to the two empty environments. For item 3, induct on the common source rule tree. Variable and constant leaves select the same scheme instance; lambda and application follow from their induction hypotheses. At a let, the generalized variable set is unchanged because row display and lacks derivations do not change free variables; rename the two fresh static binders to the fixed quantifier order and apply both induction hypotheses. At Q-Conv, canonical target indices agree by lemma 7.49(1). For every record or variant rule, lemma 4.37 gives the same affine evidence expression, the induction hypotheses give the same operands, and lemma 4.5 gives the same canonical row index. These cases cover the rule tree, so the canonical target terms are literal syntactic equals. ◻

Corollary 7.61 — Coherent principal compilation ¶

Suppose qualified W returns an unambiguous principal result for $e$ . Run W with the fixed work-list, quantifier, label, and predicate orders of this chapter, then elaborate its induced typing derivation. The resulting canonical target term is unique up to renaming of freshly allocated static variables.

Referenced from 2 locations

Row Polymorphism and Extensible Records and Variants

Proof of Corollary 7.61 — Coherent principal compilation

Proof. The solver clauses are ordered, and lemma 7.38 gives determinism of W up to the unique fresh renaming that fixes the input. The unambiguity condition requires every residual evidence parameter to occur in the visible type interface. Finally, item 3 of theorem 4.46 removes the remaining choices of lacks derivation and row display order. ◻

Remark 7.62 — Scope of coherence ¶

Principal inference fixes the residual row and field-type choices; administrative coherence then removes the remaining choices of row display and lacks derivation. For a fixed source typing tree, the resulting target programs have the same canonical syntax. Predicate weakening can change the evidence tuple, so comparing arbitrary derivations additionally requires the principal-inference choice.

Referenced from 3 locations

Row Polymorphism and Extensible Records and Variants

One should not strengthen adequacy to the literal claim that every source step is simulated by one or more target steps. A generalized source let may reduce its bound expression, whereas its evidence-passing translation stores an evidence abstraction, already a target value. The logical relation permits these administrative steps to occur in a different order while still requiring the same ground result. For each primitive record or variant contraction, the proof above does give a direct target simulation; the weaker global statement is needed only because of qualified let generalization.

Exercise 4.7 ¶

★☆☆ Assume label order $error < host < ok < port$ . Compute the evidence for each of ${host : String, port : Nat} \ ok, {ok : α, error : String} \ host .$ Then trace the numeric tag changes when an $ok$ variant is embedded first past $host$ and then past $error$ .

Referenced from 3 locations

Three nearby designs

The completed calculus lets us compare alternatives without confusing their theorems.

Presence flags

Rémy represents each label by a presence descriptor: $pre (τ)$ when the field is present and $abs$ when absent, with row variables standing for the remaining descriptors. In that notation, strict extension changes the $ℓ$ descriptor from $abs$ to $pre (τ)$ . Our judgment $ξ \ ℓ$ carries the same negative fact separately from the positive row structure.

For a finite label universe, the translation is literal: send ${ℓ : τ ∣ ρ}$ to the flag map obtained from $ρ$ by setting $ℓ$ to $pre (τ)$ , and send every absent label to $abs$ . Lemma 4.5 shows that permutation does not change this map. With an unbounded label set, Rémy’s sorted record algebra is more economical than writing an infinite flag vector. Its unitary unification theorem—every solvable problem has one most general solution up to mutual instantiation—and the Gaster–Jones theorem reach the same principal-inference goal through different syntax; we do not combine their unification rules.

Scoped duplicate labels

If duplicate labels are retained, extension need not require a lacks predicate. Selection and restriction act on the first matching label, and row equality swaps adjacent fields only when their labels differ. Then $λ r . {scratch = zero ∣ r}$ has an unconstrained row-polymorphic type even when $r$ already contains $scratch$ ; the old field remains behind the new one. In our calculus, the same term requires $ξ \ scratch$ , while replacement is written explicitly as update.

Neither choice is a notational variant of the other. The duplicate-label calculus admits the row rejected after definition 4.3; our canonical-forms proof uses its impossibility. Its simpler unification does not prove theorem 4.35, and our insertion theorem does not prove principality for its equality. Leijen’s scoped-label calculus gives the alternative rules and proof boundary.

Width subtyping

For this comparison only, take the two rules $\frac{J \subseteq I}{{ℓ_{i} : τ_{i}}_{i \in I} <: {ℓ_{j} : τ_{j}}_{j \in J}} Width \frac{\begin{matrix} Γ ⊢ e : A \\ A <: B \end{matrix}}{Γ ⊢ e : B} Sub,$ where a shared label has the same field type on both sides. These rules are not part of the row calculus proved above; they define the small comparison system used in this paragraph and the following exercise. With width subtyping, one may declare ${port : Nat, host : String} <: {port : Nat}$ and type $λ r . r . port$ at the fixed function type ${port : Nat} \to Nat$ . Subsumption then accepts larger arguments. Row polymorphism instead gives a quantified tail and needs no subsumption judgment.

The difference appears in the result of extension. Subtyping can forget fields to view a large record as a smaller one, but the type ${port : Nat} \to {secure : Bool, port : Nat}$ does not say that an arbitrary input field survives. The row type $\forall ξ . (ξ \ secure) \Rightarrow Rec (ξ) \to Rec ({secure : Bool ∣ ξ})$ does. Row inclusion and subtyping can coexist, but they solve different typing problems.

Exercise 4.8 ¶

★★☆ First derive width subtyping for applying $portOf$ to a record with $host$ , $port$ , and $secure$ fields. Then give the row-polymorphic instantiation. Explain why width subtyping alone cannot recover the precise result type of adding a $timeout$ field while preserving all three inputs.

Referenced from 3 locations

First-class labels and generic traversal

The strict calculus fixes every operation label in the term syntax. To make a label a value, add a label sort, label variables $k$ , singleton types $Lab (k)$ , and lacks predicates with label-variable right sides. The judgment $P ⊩ ξ \ k$ says that the row assigned to $ξ$ has no field at the label denoted by $k$ . The selection rule is $\frac{\begin{matrix} P ⊩ ξ \ k \\ Γ ⊢ p : Lab (k) \\ Γ ⊢ r : Rec ({k : α ∣ ξ}) \end{matrix}}{Γ ⊢ selectAt p r : α} Label - Select .$ The singleton index connects the run-time label value to the row component selected by the operation. Consequently the generic selector has scheme $\forall k, α, ξ . (ξ \ k) \Rightarrow Lab (k) \to Rec ({k : α ∣ ξ}) \to α .$ A plain type $Label$ would not suffice: it would forget which row component the value denotes. An existential package $\exists k . Lab (k)$ hides its index, but two package openings alone do not prove that their witnesses differ: both packages may contain the same label. A generative allocator needs an operational freshness invariant. For example, let $W$ be the finite set of allocated labels; allocation chooses $k \notin W$ , returns a package hiding $k$ , and continues with $W \cup {k}$ . Two sequential allocations are distinct because the second choice excludes the first. This subsection uses only first-class selection and does not claim that generative calculus.

First-class labels still do not supply generic traversal. For a type operator $F$ , write $Map (F, ρ)$ for the row obtained by applying $F$ to every field type in $ρ$ . A generic dispatcher would have type $Rec (Map (λ α . α \to γ, ρ)) \to Var (ρ) \to γ .$ It must inspect whichever label the variant carries and select the matching function from the record. The strict calculus can eliminate one statically named label, but it has neither $Map$ on rows nor induction over an unknown row. Thus repeated uses of its case rule implement the dispatcher only after the finite labels are known. This obstruction separates first-class selection from genuinely generic programming over extensible data.

One concatenation program in two row theories

Consider symmetric concatenation $m ⋆ n$ , defined only when the input records have disjoint labels, and the program $λ m . λ n . (m ⋆ n) . x .$ The selected field may come from either input. This single term exposes a constraint that a lacks predicate on one named extension cannot express.

One constraint presentation regards a row as a label-indexed family of descriptors $Abs$ or $Pre (τ)$ . If $L$ is a finite or cofinite set of labels, write $L : C (φ_{1}, \dots, φ_{n})$ when the component constraint $C$ holds pointwise for every label in $L$ . Define $Merge (a, b, c)$ by the two successful cases $Merge (Pre (τ), Abs, Pre (τ)), Merge (Abs, Pre (τ), Pre (τ)),$ together with $Merge (Abs, Abs, Abs)$ ; there is no case with two present inputs. The filtered constraint $Labels : Merge (ρ_{1}, ρ_{2}, ρ_{3}), {x} : ρ_{3} = Pre (α)$ types (7.2). The singleton filter states the selection fact, while the all-label filter states disjoint concatenation.

An abstract row theory packages the same information as two predicates. Write $Combine (ρ_{1}, ρ_{2}, ρ_{3})$ when the first two rows combine to the third, and write $Contains ({x : α}, ρ_{3})$ when the third row contains the selected field. The program then has the qualified type $\begin{aligned} \forall ρ_{1}, ρ_{2}, ρ_{3}, α . (Combine (ρ_{1}, ρ_{2}, ρ_{3}), \\ Contains ({x : α}, ρ_{3})) \Rightarrow Rec (ρ_{1}) \to Rec (ρ_{2}) \to α . \end{aligned}$ This formulation can be interpreted by different row-combination algebras; the strict system developed in this chapter fixes only single-field insertion with a lacks side condition.

There is no direct encoding of this program that uses only strict selection from one fixed input and finitely many extensions at labels known in the program text. Instantiate once with $x$ present only in $ρ_{1}$ , and once with it present only in $ρ_{2}$ . Both instances satisfy the two displayed constraint accounts. A strict selection from a fixed input fails one of them, while selecting from the result would require the absent concatenation primitive. Expanding concatenation into extensions is possible for a known finite row, but not uniformly for two unknown row tails. Thus the two instances separate that direct-encoding class. They do not exclude arbitrary whole-program translations into a richer target. The comparison theories add a row-wide combination relation, not merely alternate notation for $ξ \ ℓ$ .

Bibliographic notes.

The qualified types, mutually recursive unification and insertion procedures, principal inference pattern, and offset-evidence idea follow Gaster and Jones [GJ96]. Their constructor syntax permits raw duplicate rows and relies on predicates at operation sites. Our normalized predicate contexts and strict formation are therefore an adaptation, not a verbatim reproduction. The constrained insertion theorem above proves the correspondence needed here: every admissible strict solution factors through the same fresh-tail exposure, and every generated residual predicate is precisely a strict-formation obligation. We proved termination, factorization, safety, and the restricted administrative coherence of remark 7.62 for this adapted presentation rather than importing those claims. Gaster and Jones give the two evidence-parameter rules and their offset-entailment rules in Section 5.1 and Figure 6, then explicitly omit the complete translation for reasons of space. We therefore define the target in definition 4.38 and the translation in definition 4.39, definition 4.40. The required properties are proved in theorem 4.46.

Rémy’s record algebra and transfer from unitary unification to principal ML typing are in [Ré91]. Scoped duplicate labels are compared from Leijen [Lei05]; those sections respectively give record operations and equality, variants, and the formation (there called kinding) and unification metatheory. That paper’s published proof is not used for the strict calculus. These sources make different choices about duplicates and predicates, so their theorems are not pooled.

The singleton label indices, row-equality predicates, and generativity boundary in subsection 7.8.4 follow the first-class-label calculus of Leijen [Lei04]. The row-mapping dispatcher isolates the additional generic traversal studied by Hubers and Morris [HM23a]. The filtered component account of subsection 7.8.5 is reconstructed from Pottier [Pot03]; the combination and containment predicates are the abstract row-theory interface of Morris and McKinna [MM19]. We use these works for comparison only. The strict safety, inference, and elaboration proofs do not import their metatheorems.

Boundary and further problems

The fields in this chapter have ordinary, nondependent types. If a later field type may mention the value of an earlier field, permutation is no longer a bare exchange: the type must be transported when the dependency crosses the exchange. Likewise, row unification would have to solve terms inside types, not just the sorted first-order equations of definition 4.23. We therefore make no dependent-row claim here. Any dependent extension must state its own substitution, equality, decidability, and inference theorems.

Suggested first pass.

Begin with exercise 4.10. It is a board-sized calculation that tests both admissible grounding and the exact point at which a bad instance fails. Then reconstruct the two factor maps in exercise 4.11; these two problems form the first pass. Use exercise 4.9 as the next synthesis problem and exercise 7.12 as the implementation project. The final two problems test the duplicate-label and evidence-ambiguity boundaries.

Exercise 4.10 ¶

★★☆ Let $G$ instantiate $ξ$ by ${host : String}$ in the principal type of $withSecure$ . Write the complete ground typing and reduce its application to ${host = "db" ∣ {}}$ . Repeat with an attempted instantiation containing $secure : Nat$ and identify the exact failed normalization step.

Referenced from 4 locations

Exercise 4.11 — Most-general rows (★ )¶

★★☆ Suppose $(U, Q_{U})$ and $(V, Q_{V})$ are principal solutions of the same row equation problem over $P$ . Use their two factorization properties to construct admissible maps $R : Q_{U} \to Q_{V}$ and $S : Q_{V} \to Q_{U}$ with $V \equiv_{Q_{V}} U; R$ and $U \equiv_{Q_{U}} V; S$ on the problem variables. Give a two-label example where the printed fresh tail names, residual predicate contexts, and field orders differ although this mutual instance conclusion holds.

Hint. Apply the factorization property of $U$ to the solution $V$ , then the factorization property of $V$ to $U$ . For the example, use the crossing equation of example 4.24 twice, with different fresh tail names and different legal exchange sequences.

Referenced from 4 locations

Exercise 4.9 ¶

★★★ Assume $ℓ \neq m$ and a tail $ξ$ lacking both labels. Infer the principal scheme of $λ a . λ b . λ r . {ℓ := a ∣ {m := b ∣ r}} .$ Show by row permutation that reversing the two updates gives the same result type. Does the operational result have the same finite map? Give the two restriction-and-extension calculations.

Referenced from 4 locations

Exercise 7.12 ¶

★★★ Practical project.row-inferencer Work in artifacts/ch7-rows/corpus.kp. Implement the four insertion and six solver clauses of definition 4.23 in their printed order, including U-Delete. Return the actual clause trace with every successful solver result; do not predict it by traversing the input a second time. Preserve the invariant that the returned substitution is admissible from the input predicate context to the normalized output context.

The accepted crossing run must return and print $U-Row -> I-Skip -> I-Var -> U-Var -> U-Done .$ Apply its substitution to both input rows, check that both substituted rows are strictly formed under the returned predicates, and then check contextual row equality. Also test syntactic identity deletion, principal factorization, termination within the input-derived bound, record and variant operations, fresh supply, qualified generalization at two instances, empty insertion, the occurs check, duplicate formation, and the nonprincipal closed-tail mutant. Run the four commands in Appendix F and require all eleven PASS lines, the printed summary, and audit output []. Finally apply mutant-accept-empty-insertion.patch to a disposable copy: it must still check and must fail the empty-insertion oracle. These finite runs are implementation evidence; they do not prove termination, factorization, principality, coherence, inference correctness, or safety.

Referenced from 6 locations

Exercise 4.12 — Scoped duplicate records (★ )¶

★★★ Design the record fragment of a scoped-duplicate calculus, rather than changing formation alone. Make the following four changes.

Delete the lacks premise from each extension rule: $R o w - E x t, Q - E x t e n d .$
Permit repeated labels in record values.
Let selection and restriction act on the first displayed occurrence.
Continue to swap only adjacent distinct labels.

Which sentence in the proof of lemma 4.21 now becomes false? Repair the canonical-forms statement for this calculus, and state why the repaired lemma does not justify the strict update equation without specifying which occurrence is removed.

Do not extend this answer to variants. A scoped-duplicate variant calculus must additionally change embedding, represent the nesting level of equal labels at run time, and give matching case rules; the label-only variant values of definition 4.17 cannot express that information.

Hint. Induct on the displayed record spine. Selection returns the first matching occurrence, whereas restriction removes that occurrence and leaves every later occurrence available.

Referenced from 3 locations

Exercise 4.13 — Ambiguous evidence (★ )¶

★★★ Consider the scheme $\forall ξ . (ξ \ ℓ) \Rightarrow Nat$ . Its result type does not determine which evidence is required. Show that all its ground instances have the same source type but may elaborate to functions expecting offsets for different rows. State the usual unambiguity condition for an open judgment and its closed-scheme specialization: $ftv (P) \subseteq ftv (Γ, τ), ftv (P) \subseteq ftv (τ) .$ Now run $W_{r}$ on ${case}_{ℓ} ⟨ ℓ = zero ⟩ of {⟨ ℓ = x ⟩ \mapsto zero; y \mapsto zero} .$ Show that its principal result contains a fresh predicate $ξ \ ℓ$ although its result type is $Nat$ . Thus unambiguity is an additional acceptance condition, not an invariant of the inference clauses. Give two possible repairs: reject such ambiguous principal results, or choose and document a default ground row when evidence is elaborated.

Hint. Give injection a fresh tail $ξ$ . The case result forgets that tail because both branches return $Nat$ , but the injection’s formation constraint $ξ \ ℓ$ remains in the normalized predicate set.

Referenced from 3 locations