Corrected Inference for Simple Objects

Prerequisites. Direct starred prerequisites: chapter 4, chapter 13. No later core chapter depends on this route.

Consider $$W:=\lambda f.\lambda x.f(x\mathsf{with}a=3)+f(\mathsf{null}\mathsf{with}a=3).$$ The second call passes the singleton integer record to $f$. The first does so exactly when $x$ is empty or consists of one $a$-field of arbitrary type: update overwrites that field, but it preserves every field at a label $b\ne a$. One type scheme must therefore describe the empty row and another the singleton-row family. A claim that every typable term has one principal type scheme fails on this term.

This is the correction made by Wand’s 1988 corrigendum to the 1987 simple- object inference system. The repaired result is an effectively generated finite complete set of typings. It is not a principal-type theorem under an unnamed restriction. The later record-concatenation calculus and Rémy’s unitary record calculus will be named separately when they enter.

Rows remember presence

Fix a countable set of labels. A semantic row is a finite partial map from labels to types. Write ${\varnothing }_{\mathsf{r}}$ for the empty row and $r[a\leftarrow \tau ]$ for right-biased update. Thus The record type with row $r$ is $\mathrm{\Pi }(r)$. Undefined fields are absent; $\mathrm{\Pi }(r)$ is not a product with a hidden arbitrary component.

The distinction between one most general unifier and a finite complete set is load bearing. A unitary problem has one most general solution. A finitary problem may require several incomparable most general branches.

The typing constraints for the record primitives are read directly from their operations. With $r$ fresh at each instantiation, their schemes are The row expression $r$ expresses the independent presence information at every label. Update overwrites the $a$-field instead of equating its old and new types.

Proof of Lemma 26.2 — Constraint characterization

Proof. Induct on the term. Variables equate an occurrence variable with its binder variable. Application generates $t_{e_1}=t_{e_2}\to t_{e_1{e}_2}$, and abstraction generates $t_{\lambda x.e}=t_x\to t_e$; these are the ordinary Hindley–Milner cases. Integer addition equates both operands and the result with $\mathsf{Int}$. The null, selection, and update cases instantiate the three displayed schemes. In the update case, the fresh input row $r$ is unconstrained at $a$, while the result is $r[a\leftarrow \tau ]$; this is exactly right-biased overwrite. Reading each equation from a derivation gives the forward direction, and applying the corresponding typing rule to a solution gives the reverse direction. ◻

The invalid decomposition

The original unification step treated update as an injective constructor: $$r_1[a\leftarrow {\tau }_1]=r_2[a\leftarrow {\tau }_2]⟹r_1=r_2\wedge {\tau }_1={\tau }_2.$$ The conclusion is too strong. Put $$r_1={\varnothing }_{\mathsf{r}},r_2={\varnothing }_{\mathsf{r}}[a\leftarrow \mathsf{Bool}],{\tau }_1={\tau }_2=\mathsf{Int}.$$ Both updated rows denote the singleton integer row, while $r_1\ne r_2$. The update constructor is not injective in its row argument because the old $a$-field is immediately overwritten.

The repair determines which of the two input rows already contains $a$. There are four, not two, possibilities.

Proof of Lemma 26.3 — Four-way overwrite decomposition

Proof. Suppose (26.3) holds. At label $a$, the two updates return ${\tau }_1$ and ${\tau }_2$, so extensional equality gives ${\tau }_1={\tau }_2$. Delete $a$ from both input rows. At every $b\ne a$, update leaves the old field unchanged; hence the two deletions are equal. Call their common row $r_0$. Each original row either lacks $a$ or has one field $u_i$ there, giving exactly the four table rows.

Conversely, in every table row the two inputs agree away from $a$. Updating both at $a$ with the common type ${\tau }_1={\tau }_2$ therefore makes the rows extensionally equal. Every semantic solution has one of the four presence patterns, so the branches cover all solutions; no two patterns can be merged without forgetting whether a field is present. ◻

The shared-variable termination case

Branching alone does not repair termination. If both sides contain the same row variable, repeated decomposition can reproduce a problem of the same size. The representative equation is $$\rho =\rho [a_1\leftarrow {\tau }_1]\cdots [a_n\leftarrow {\tau }_n].$$ It does not ask for an infinite row. It states that $\rho$ already contains the listed fields with the listed final types.

Proof of Lemma 26.5 — Shared-variable equivalence

Proof. Evaluate the update chain from left to right. At every listed label, the right side returns the type written by its last update. Equality with the left side therefore requires that $\rho$ already return that type. At an unlisted label the update chain returns $\rho$’s own field, so equality is automatic. These are precisely the recorded obligations. ◻

Proof of Lemma 26.6 — Termination measure for the corrected row phase

Proof. Ordinary decomposition removes one active type or row constructor and adds only its proper subexpressions, so the first component decreases. A four-way overwrite split removes the two compared update heads before solving a branch, which also decreases the first component. The shared-variable case removes its active equation and adds only atomic presence obligations; atomic obligations contribute no constructors to the first component. Discharging or rejecting an atomic obligation leaves the first component fixed and decreases the second. No rule adds an active equation after entering the atomic phase. Lexicographic order on pairs of natural numbers is well founded, so the row-specific phase has no infinite branch. Ordinary variable elimination is outside this phase and uses the original unification algorithm’s halting measure. ◻

The counterexample has two generators

Retain the full countable label universe of section 26.1. The program mentions only $a$, but that does not restrict substitutions for a row variable to rows over $\{a\}$. Put $r_a(\tau )={\varnothing }_{\mathsf{r}}[a\leftarrow \tau ]$. The two type schemes needed for (26.1) are For ${\sigma }_0$, $x$ begins empty. For ${\sigma }_1$, $x$ begins with an $a$-field of arbitrary type. Both updates overwrite that field with an integer before $f$ is called.

Proof of Proposition 26.7 — No principal scheme for W

Proof. Both displayed schemes type $W$ by the update rule. They are incomparable: substitution for the type variable in ${\sigma }_1$ cannot turn a present field into absence, while ${\sigma }_0$ has no field type to instantiate.

For completeness, consider any typing of $W$. The two calls to $f$ force the updated row of $x$ to equal $r_a(\mathsf{Int})$, the type of the updated null record. At every $b\ne a$, update preserves $x$’s old field while $r_a(\mathsf{Int})$ has none. Hence $x$ has no field away from $a$. It is therefore either empty, giving an instance of ${\sigma }_0$, or has the single field $a:\tau$, giving an instance of ${\sigma }_1$ at $\tau$.

It remains to exclude one generator. A row expression whose instances include both the empty row and a row with an $a$-field cannot contain an explicit update: an update fixes at least its final label as present. It must expose a row variable $\rho$. But the label universe contains some $b\ne a$, so the substitution $\rho \mapsto {\varnothing }_{\mathsf{r}}[b\leftarrow \mathsf{Int}]$ is also an instance. For that input, the first call passes the two-field row $\{a:\mathsf{Int},b:\mathsf{Int}\}$ while the second passes only $\{a:\mathsf{Int}\}$; the alleged scheme does not type $W$. Thus no valid scheme generates exactly both families, while the two displayed schemes are complete. ◻

The proposition is the smallest witness against the published principal- types claim. It is not a counterexample to decidable typability.

Proof of Theorem 26.8 — Corrigendum boundary: finite complete sets

Proof. This is the corrected result stated on page 132 of Wand’s one-page 1988 corrigendum [Wan88]: the published principal-type claim is withdrawn there, and the replacement is the effective finite complete set constructed by the corrected branching procedure. The imported algorithm replaces invalid decomposition (26.2) by the four cases of lemma 26.3, unions the unifier sets returned by those branches, and treats the shared-variable equations of definition 26.4 separately. By lemma 26.6, the row-specific repair introduces no new infinite branch. The corrigendum’s imported halting argument combines this special treatment with the original measure for the other unification steps. Each equation creates only finitely many branches. The resulting scheme family is finite, every returned scheme types the term, and every typing factors through one returned branch. Those are exactly the soundness and completeness clauses of definition 26.1. The source supplies no theorem selecting one branch as principal. ◻

A separately named successor calculus

Wand’s later record-concatenation calculus starts from a different operation. For semantic records $r,r^{\prime }$, right-biased concatenation is This section alone fixes a finite ordered label set $L=\{a_1,\dots ,a_n\}$. Its separately sorted field descriptors are $$d::=\varphi \mid \mathsf{absent}\mid \mathsf{present}(\tau ),$$ where $\varphi$ ranges over descriptor variables. A descriptor substitution maps $\varphi$ only to descriptors. Write ${\mathrm{\Pi }}_L(d_1,\dots ,d_n)$ for the resulting finite-label record type; this notation is not the row constructor $\mathrm{\Pi }(r)$ of the corrected 1987 system. A concatenation occurrence $M\Vert \Vert N$ generates fresh descriptor variables and the equations and, for each $i$, the disjunction $$(g_i=\mathsf{present}({\tau }_i)\wedge h_i=g_i)\vee (g_i=\mathsf{absent}\wedge h_i=f_i).$$ The disjunction records the same right-bias as the dynamic operation.

Proof of Lemma 26.9 — Concatenation constraints are exact

Proof. Fix $a_i$. If the right row is present there, the first disjunct makes the result equal to that field. If it is absent, the second disjunct copies the left descriptor. These cases are exhaustive and disjoint. Applying the calculation at every label gives equality of finite rows; the reverse direction selects the disjunct dictated by the right row at each label. ◻

Expanding the positive Boolean combination of equations into disjunctive normal form yields finitely many conjunctions. Ordinary unification returns a most general unifier for every solvable conjunction. Their union is a finite complete set, not a single principal solution.

Proof of Theorem 26.10 — Finite complete sets for record concatenation

Proof. This is Wand’s finite-label theorem for record concatenation. Constraint characterization reduces typing to a positive Boolean formula. Its atoms are ordinary equations and the cases in (26.7). Finite $L$ and finitely many syntax nodes give a finite formula. Expansion into disjunctive normal form gives finitely many unification problems. Unitary first-order unification supplies one most general unifier per solvable disjunct. By lemma 26.9, every returned branch is sound. Conversely, any typing selects one disjunct at each field, so it factors through a returned unifier. The returned set is empty exactly when the term is untypable. ◻

With an unbounded label set, the same paper replaces infinite enumeration by extension constraints and returns pairs consisting of a finite constraint set and a type scheme. That theorem belongs to the successor calculus; it is not a missing clause of the 1988 corrigendum.

Rémy’s theorem is not the corrigendum

Rémy assigns every label a presence descriptor in a sorted equational algebra. For record extension and selection, without Wand’s right-biased concatenation operation and without the incompletely formalized recursive object extensions, that algebra has decidable unitary unification. The ordinary Hindley–Milner reduction then gives principal typings.

Thus three claims have three signatures:

The last row cannot be used to replace either of the first two. Adding recursive objects or concatenation changes the equation theory on which unitarity depends.

The chapter exports lemma 26.3, lemma 26.5, the exact imported result theorem 26.8, and the separately named successor theorem theorem 26.10. It exports no unrestricted principal-type theorem for simple objects and no theorem that transfers Rémy’s unitary result to recursive objects or record concatenation.

Sources.

The counterexample, four overwrite cases, shared-variable termination repair, and finite-complete-set correction are from [Wan88]; the invalid claim being corrected is in [Wan87]. The finite-label concatenation theorem and its exact disjunctive constraints are from [Wan91]. Rémy’s separate unitary boundary is from [Ré91].

Suggested first pass.

Problems exercise 26.6, exercise 26.7, and exercise 26.10.

Exercise 26.6¶

★☆☆ Derive both ${\sigma }_0$ and ${\sigma }_1$ for $W$. At each update, write the input and output descriptor of label $a$. Identify the step that would be rejected by the invalid decomposition (26.2).

Referenced from 4 locations

• Corrected Inference for Simple Objects
• ch:simple-object-inference: ch:simple-object-inference

Exercise 26.7¶

★★☆ Let $E$ contain two overwrite equations at distinct labels $a,b$. Build the sixteen raw presence branches and give one concrete witness for each. Then add the equation that one selected old field is both absent and present, discard the resulting inconsistent branches, and show how every remaining semantic solution selects a branch. State why this is completeness of a set, not principality of one member.

Referenced from 4 locations

• Corrected Inference for Simple Objects
• ch:simple-object-inference: ch:simple-object-inference

Exercise 26.8¶

★★☆ Normalize $$\rho =\rho [a\leftarrow \alpha ][b\leftarrow \beta ][a\leftarrow \gamma ]$$ to presence obligations. Prove that the obligation for $a$ mentions $\gamma$, not $\alpha$, and that the equation is satisfiable.

Referenced from 3 locations

• Corrected Inference for Simple Objects
• ch:simple-object-inference: ch:simple-object-inference

Exercise 26.9¶

★★★ For $L=\{a,b\}$, generate and solve the constraints for a function that concatenates two records and selects both result fields. List the satisfiable origin choices and compress their unifiers into a finite complete set of type schemes.

Referenced from 3 locations

• Corrected Inference for Simple Objects
• ch:simple-object-inference: ch:simple-object-inference

Exercise 26.10¶

★★★ Practical project.corrected-row-unifier Implement the finite one-label overwrite step, including all four presence branches and the shared-variable special case. Maintain the invariant that every returned branch denotes only solutions of the input equation and that every concrete solution selects a returned branch. Run the exact counterexample boundary from proposition 26.7 on a bounded two-label corpus: accept empty and $a$-only inputs for $x$, reject inputs that retain a foreign $b$-field, report that the naive decomposition rejects a valid row equation, and terminate on $\rho =\rho [a\leftarrow \mathsf{Int}]$. Acceptance is the six named PASS lines and final summary in appendix E.

Referenced from 5 locations

• Corrected Inference for Simple Objects
• Object calculus checker and evaluator
• ch:simple-object-inference: ch:simple-object-inference