ch:simple-object-inference: ch:simple-object-inference

Give $r$ the fresh semantic row $ρ$ . Updating generates $ρ [a \leftarrow Int]$ ; selection reads its $a$ -field and hence returns $Int$ . Thus $λ r . (r with a = 3) . a : Π (ρ) \to Int .$ The input row $ρ$ remains unconstrained: its $a$ -field may be absent or present at any type, and it may contain finitely many other fields.

Let $r_{0} = {b : Bool}$ , with $b \neq a$ , and update both sides with $a : Int$ . For the four rows choose old $a$ -fields respectively $(Int, Bool)$ , $(-, -)$ , $(-, Bool)$ , and $(Bool, -)$ . In every case both updated rows return $Int$ at $a$ and $Bool$ at $b$ . The four old presence pairs are distinct even though the results are equal.

Substituting the right side for $ρ$ reproduces an occurrence of $ρ$ under an update, so the active row-constructor count does not decrease and iteration grows the chain. Use the measure $(active constructors, unresolved obligations) .$ The special step changes the representative equation from $(1, 0)$ to $(0, 1)$ . Lexicographic order decreases at the first coordinate.

At label $a$ , either the right input supplies the demanded integer or it is absent and the left input supplies it. With descriptor variables $f, g$ , the two scheme shapes are $\begin{aligned} σ_{r} & = Π_{L} (f) \to Π_{L} (present (Int)) \to Int, \\ σ_{l} & = Π_{L} (present (Int)) \to Π_{L} (absent) \to Int . \end{aligned}$ The first permits the right field and the second requires its absence, so neither presence pattern is an instance of the other.

One most general row unifier and principal typing for extension and selection belong to Rémy’s sorted calculus. The four-way overwrite split belongs to the 1987 system as corrected in 1988. One disjunction per concatenated field belongs to Wand’s 1991 concatenation calculus. Finite complete type sets belong to both corrected Wand systems, with their separately stated signatures; they are not a claim about Rémy’s unitary system.

For $σ_{0}$ , $x$ ’s input descriptor is absent and its output descriptor is present integer. The null argument follows the same absent-to-present transition. For $σ_{1}$ , $x$ ’s input descriptor is $present (α)$ , but its output is again present integer; null still goes absent to present. The invalid decomposition rejects the equality between the two updated inputs by demanding equality of their old row arguments. Correct overwrite equality ignores those old $a$ -descriptors. At every $b \neq a$ , however, the first update retains $x$ ’s descriptor and the updated null record remains absent. The common argument type for $f$ therefore forces $x$ to have no foreign field. This is why the two schemes cover the full-label counterexample without making an unconstrained row variable a valid single generator.

For each label independently choose $PP, AA, AP, PA$ ; their Cartesian product has sixteen members. A concrete witness is obtained by taking one common row with neither label and inserting arbitrary old field types exactly where its two shape letters say present. Thus all sixteen raw branches are satisfiable before the extra equation. If that equation requires, for example, the first old $a$ -field to be both absent and present, discard precisely the eight branches whose first $a$ -letter conflicts with the selected requirement. Every remaining semantic solution has one presence pair at each label and therefore selects one remaining branch. Coverage chooses a member of a set; it does not make that member more general than the others.

The last update at a repeated label wins, so normalization gives $has (ρ, a, γ), has (ρ, b, β) .$ The earlier $a : α$ is overwritten. The row ${a : γ, b : β}$ , together with any fields at other labels, satisfies the original equation, proving satisfiability.

For each of $a, b$ , the selected result field comes either from a present right descriptor or from the left descriptor when the right is absent. The four satisfiable origin pairs are $(R, R), (R, L), (L, R), (L, L)$ . For result types $α, β$ , their schemes require respectively $\begin{array}{ccc} x & y \\ R R & (-, -) & (a : α, b : β) \\ R L & (-, b : β) & (a : α, b : -) \\ L R & (a : α, -) & (a : -, b : β) \\ L L & (a : α, b : β) & (a : -, b : -) . \end{array}$ A dash in $x$ is unconstrained when the right field wins and denotes absence in $y$ when the left field wins. Generalizing $α, β$ gives a four-member finite complete set.