Chapter 19Optional

Algebraic Subtyping and Principal Inference

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

One variable needs an upper and a lower face

Subsumption breaks the equality equations used by Algorithm W. For $apply : = λ f . λ x . f x$ equality-based inference identifies the type expected by $f$ with the type produced by $x$ . Subtyping needs only a directed constraint $α_{x} \leq_{a} α_{f}$ . Replacing that constraint by equality forgets valid programs; retaining an external constraint set loses the compact principal type promised by ML inference.

Suppose first that $α \leq_{a} Int$ occurs in $α \to α$ . Replacing both occurrences by $α \land Int$ gives $(α \land Int) \to (α \land Int) .$ The result is needlessly restricted. The upper bound constrains values accepted by the function, not values returned by it. The compact solution is $(α \land Int) \to α .$ The two occurrences of $α$ therefore require different substitutions.

Definition 19.1 — The frozen MLsub fragment MLsub_0 ¶

Let $b$ range over the rigid base atoms $Unit, Bool, Int, String$ . The exact term and type grammars are $\begin{aligned} e & ::= x ∣ \hat{x} ∣ () ∣ true ∣ false ∣ λ x . e ∣ e e ∣ let \hat{x} = e in e ∣ if e then e else e, \\ T & ::= b ∣ α ∣ ⊥ ∣ ⊤ ∣ T \lor T ∣ T \land T ∣ T \to T ∣ μ α . T, \\ P & ::= ⊥ ∣ b^{+} ∣ α^{+} ∣ P \lor P ∣ N \to P ∣ μ α . P, \\ N & ::= ⊤ ∣ b^{-} ∣ α^{-} ∣ N \land N ∣ P \to N ∣ μ α . N . \end{aligned}$ In a recursive type, $α$ is covariant and every occurrence of it is guarded by an arrow. The $P, N$ grammars are the polar sublanguages of the ambient local algebra $T$ . A polar type records whether each variable occurrence is in an output position $(+)$ or an input position $(-)$ . Crossing an arrow reverses polarity in its domain and preserves polarity in its codomain. A polar scheme has the form $[Δ^{-}] P^{+}$ , where every entry $Δ (x)$ is a negative type. When an atom’s polarity is determined by its grammar position, its superscript is omitted. Distinct atoms are distinct rigid heads. The variable $x$ is lambda-bound; $\hat{x}$ is let-bound. Bound variables are renamed apart before inference.

Referenced from 4 locations

The superscripts are sorts, not variance assertions about arbitrary type expressions. In particular, this grammar is not a complemented Boolean type algebra.

Definition 19.2 — Algebraic subtype laws ¶

Let $A, B, C$ range over ambient types $T$ . The relation $\leq_{a}$ is the least preorder on those types, compatible with arrows and the lattice laws $\begin{matrix} ⊥ \leq_{a} A, A \leq_{a} ⊤, \\ A_{i} \leq_{a} A_{1} \lor A_{2}, (A_{1} \leq_{a} C \land A_{2} \leq_{a} C) ⟹ A_{1} \lor A_{2} \leq_{a} C, \\ A_{1} \land A_{2} \leq_{a} A_{i}, (C \leq_{a} A_{1} \land C \leq_{a} A_{2}) ⟹ C \leq_{a} A_{1} \land A_{2}, \\ A_{2} \leq_{a} A_{1} \land B_{1} \leq_{a} B_{2} ⟹ (A_{1} \to B_{1}) \leq_{a} (A_{2} \to B_{2}) . \end{matrix}$ Guarded $μ$ -types are identified with their unfoldings. For every base atom $b$ , reflexivity gives $b \leq_{a} b$ ; there is no primitive comparison between two distinct base atoms. Head inversion gives $b_{1} \leq_{a} b_{2}$ only when $b_{1} = b_{2}$ . The four atoms form a free finite set of nullary heads, rather than an encoding by record labels.

Referenced from 3 locations

The record encoding is tempting and wrong. In full MLsub, the join of two records retains only their common labels. Hence ${unit : bool} \lor {int : bool} = {},$ whereas $Unit \lor Int$ is not $⊤$ in ${MLsub}_{0}$ . The local calculus therefore receives its own declarative and algorithmic proof below; no record embedding transports the MLsub theorem.

Definition 19.3 — Lambda-lifted declarative typing ¶

A scheme is $[Δ] T$ , where $Δ$ is a finite map from lambda-bound term variables to ambient types. All type variables in a scheme are implicitly generalized. Let $ρ$ range over type substitutions. Define scheme subsumption by $[Δ] T \leq_{\forall} [Δ^{'}] T^{'} ⟺ {\begin{cases} dom (Δ) \subseteq dom (Δ^{'}), \\ Δ^{'} (x) \leq_{a} ρ (Δ (x)) & for every x \in dom (Δ), \\ ρ (T) \leq_{a} T^{'} \end{cases}$ for some $ρ$ . Write $Δ_{1} \land Δ_{2}$ for the finite map on the union of their domains that takes the meet where both maps are defined and the sole entry otherwise. Write $Δ_{x}$ for deletion of $x$ , and set $Δ (x) = ⊤$ when $x \notin dom (Δ)$ .

Let $Π$ map let-bound variables to schemes. The judgment $Π ⊢_{0} e : [Δ] T$ is generated by

Π (\hat{x}) = S

Π ⊢_{0} \hat{x} : S

Var-Let

α \notin FV (Π)

Π ⊢_{0} x : [x : α] α

Var-Lam

Π ⊢_{0} e : [Δ] T

Π ⊢_{0} λ x . e : [Δ_{x}] (Δ (x) \to T)

Abs

Π ⊢_{0} e_{1} : [Δ] (T_{1} \to T_{2})

Π ⊢_{0} e_{2} : [Δ] T_{1}

Π ⊢_{0} e_{1} e_{2} : [Δ] T_{2}

App

Π ⊢_{0} e_{1} : [Δ_{1}] T_{1}

Π, \hat{x} : [Δ_{1}] T_{1} ⊢_{0} e_{2} : [Δ_{2}] T_{2}

Π ⊢_{0} let \hat{x} = e_{1} in e_{2} : [Δ_{1} \land Δ_{2}] T_{2}

Let

Π ⊢_{0} () : [] Unit

Unit

q \in {true, false}

Π ⊢_{0} q : [] Bool

Bool

Π ⊢_{0} e_{0} : [Δ] Bool

Π ⊢_{0} e_{1} : [Δ] T

Π ⊢_{0} e_{2} : [Δ] T

Π ⊢_{0} if e_{0} then e_{1} else e_{2} : [Δ] T

Π ⊢_{0} e : S

S \leq_{\forall} S^{'}

Π ⊢_{0} e : S^{'}

Sub

A polar scheme is a derivable scheme $[Δ^{-}] P^{+}$ whose environment entries are negative and whose result is positive.

Referenced from 3 locations

For $apply$ , let the two faces of the argument variable be $α^{-}, α^{+}$ , and let the result faces be $β^{-}, β^{+}$ . Application compares the positive type supplied by $x$ with the negative domain demanded by $f$ . After eliminating that constraint, the closed polar scheme is $[] (α^{+} \to β^{-}) \to (α^{-} \to β^{+}) .$ The outer domain $α^{+} \to β^{-}$ is a negative arrow, while the result $α^{-} \to β^{+}$ is a positive arrow. The shared names record the two faces connected by biunification; an environment entry, when present during the derivation, is always negative.

Exercise 19.1 — Polarity calculation ¶

★☆☆ Mark every occurrence of $α$ in $(α \to Bool) \to (Unit \to α)$ . Then state which occurrences an upper-bound elimination may change.

Referenced from 3 locations

Biunification eliminates a directed constraint

Definition 19.4 — Bisubstitution ¶

A bisubstitution $ξ$ assigns a positive image $ξ^{+} (α)$ and a negative image $ξ^{-} (α)$ to each type variable. Its action on rigid heads, joins, meets, and guarded binders is homomorphic; its action on an arrow exchanges the actions in the domain: $ξ^{+} (N \to P) = ξ^{-} (N) \to ξ^{+} (P), ξ^{-} (P \to N) = ξ^{+} (P) \to ξ^{-} (N) .$ It acts pointwise on a constraint set or sequence: $ξ C = {ξ^{+} (P) \leq_{a} ξ^{-} (N) ∣ (P \leq_{a} N) \in C}$ , and the same convention defines $ξ H$ . The identity has ${id}^{\pm} (α) = α$ , and composition is defined on variable faces by $(ζ \circ ξ)^{+} (α) = ζ^{+} (ξ^{+} (α)), (ζ \circ ξ)^{-} (α) = ζ^{-} (ξ^{-} (α)) .$ It is stable when $ξ^{-} (α) \leq_{a} ξ^{+} (α)$ for every $α$ and $ξ \circ ξ = ξ$ .

Referenced from 4 locations

The ordering in stability says that the negative requirement is below the positive offer after the action, while idempotence makes reapplication inert.

Definition 19.5 — Atomic elimination ¶

If $α \notin FV (N)$ , eliminate an upper bound $α^{+} \leq_{a} N^{-}$ with $θ_{α \leq_{a} N} : = [N \land α / α^{-}, α / α^{+}] .$ If $P^{+} \leq_{a} α^{-}$ and $α \notin FV (P)$ , use $θ_{P \leq_{a} α} : = [α / α^{-}, P \lor α / α^{+}] .$ When the variable occurs in its bound, the exact guarded actions are $\begin{aligned} θ_{α \leq_{a} N} & = [μ β . (α \land N [β / α^{-}]) / α^{-}, α / α^{+}], \\ θ_{P \leq_{a} α} & = [α / α^{-}, μ β . (α \lor P [β / α^{+}]) / α^{+}], \end{aligned}$ where $β$ is fresh. Substitution across an arrow domain exchanges the positive and negative actions as in definition 19.4; the input guardedness condition ensures that the new recursive occurrence is guarded.

Referenced from 2 locations

Algebraic Subtyping and Principal Inference

Lemma 19.6 — Nonrecursive atomic elimination preserves instances ¶

For a finite constraint set $C$ , define $Inst (S ∣ C) : = ↑ {ρ (S) ∣ ρ (P) \leq_{a} ρ (N) for every (P \leq_{a} N) \in C},$ where upward closure uses $\leq_{\forall}$ . Let $α \notin FV (N)$ and $α \notin FV (P)$ . For every polar scheme $S$ , $\begin{aligned} Inst (S ∣ {α \leq_{a} N}) & = Inst (θ_{α \leq_{a} N} (S) ∣ \emptyset), \\ Inst (S ∣ {P \leq_{a} α}) & = Inst (θ_{P \leq_{a} α} (S) ∣ \emptyset) . \end{aligned}$

Referenced from 6 locations

Proof of Lemma 19.6 — Nonrecursive atomic elimination preserves instances

Proof. Fix a substitution $ρ$ . Suppose first that $ρ (α) \leq_{a} ρ (N)$ . Meet introduction and elimination give $ρ (α) \leq_{a} ρ (N) \land ρ (α) \leq_{a} ρ (α) .$ Replacing a negative occurrence of $α$ by $N \land α$ therefore preserves the scheme up to mutual subtyping. Structural induction on $S$ , with the comparison reversed in every arrow domain, puts the constrained instance in the right-hand upward closure. At a guarded $μ$ -binder, unfold once and close the same comparison by guarded coinduction; the recurrence has crossed an arrow.

Conversely, let $T = ρ (α)$ be the image used for an arbitrary instance of the eliminated scheme. Define $ρ^{'} (α) = T \land ρ (N)$ , and let $ρ^{'}$ agree with $ρ$ on every other variable. Since $α \notin FV (N)$ , $ρ^{'} (α) \leq_{a} ρ^{'} (N)$ . At each negative occurrence the two instances contain the same meet. At each positive occurrence, meet elimination gives $ρ^{'} (α) \leq_{a} T$ . Induction on the polar scheme gives $ρ^{'} (S) \leq_{\forall} ρ (θ_{α \leq_{a} N} (S))$ . Upward closure therefore gives the reverse inclusion in (19.4).

The lower-bound equality is dual. Under a satisfying instance $ρ (P) \leq_{a} ρ (α)$ , join introduction and elimination make $ρ (P) \lor ρ (α)$ mutually subtype $ρ (α)$ . Conversely, for an arbitrary eliminated image $T$ , set $ρ^{'} (α) = ρ (P) \lor T$ . The freshness assumption makes $ρ^{'} (P) = ρ (P)$ , so the lower bound holds. Structural induction, reversed in arrow domains and closed by guarded coinduction at a $μ$ -back edge, gives the second equality. ◻

Lemma 19.7 — Guarded recursive atomic elimination preserves instances ¶

Suppose every occurrence of $α$ in $N^{-}$ , respectively in $P^{+}$ , is guarded by an arrow. For every polar scheme $S$ , the recursive upper action, respectively lower action, of (19.3) satisfies $\begin{aligned} Inst (S ∣ {α \leq_{a} N}) & = Inst (θ_{α \leq_{a} N} (S) ∣ \emptyset), \\ Inst (S ∣ {P \leq_{a} α}) & = Inst (θ_{P \leq_{a} α} (S) ∣ \emptyset) . \end{aligned}$

Referenced from 5 locations

Proof of Lemma 19.7 — Guarded recursive atomic elimination preserves instances

Proof. Represent the guarded types by their finite polar automata. For the upper action, merge the negative face of $α$ with a meet state containing the old face and the root of $N$ ; for the lower action, merge the positive face with the corresponding join state for $P$ . These are exactly the two finite graphs denoted by (19.3).

For each finite head-and-edge path, induction on its length gives the same two inclusions as the nonrecursive proof: meet introduction and elimination handle an upper return, while join introduction and elimination handle a lower return. A path that returns to the merged face has crossed an arrow by guardedness, so the induction hypothesis applies after that constructor. Equality on all finite paths yields mutual subtyping of the regular unfoldings by guarded coinduction. Applying the argument at every occurrence in $S$ , and reversing it in arrow domains, gives both displayed equalities after upward closure. ◻

Exercise 19.2 — Lower-bound elimination ¶

★★☆ Reconstruct the lower-bound half of lemma 19.6 without citing order duality. State the two instantiations explicitly and identify where $P \lor T$ is used.

Referenced from 3 locations

Definition 19.8 — Biunification work list ¶

Constraints have the one sorted form $c = P^{+} \leq_{a} N^{-}$ . The partial decomposer ${subB}_{0}$ is $\begin{aligned} {subB}_{0} ((N_{1} \to P_{1}) \leq_{a} (P_{2} \to N_{2})) & = {P_{2} \leq_{a} N_{1}, P_{1} \leq_{a} N_{2}}, \\ {subB}_{0} (b^{+} \leq_{a} b^{-}) & = \emptyset, \\ {subB}_{0} ((P_{1} \lor P_{2}) \leq_{a} N) & = {P_{1} \leq_{a} N, P_{2} \leq_{a} N}, \\ {subB}_{0} (P \leq_{a} (N_{1} \land N_{2})) & = {P \leq_{a} N_{1}, P \leq_{a} N_{2}}, \\ {subB}_{0} (⊥ \leq_{a} N) & = \emptyset, {subB}_{0} (P \leq_{a} ⊤) = \emptyset, \\ {subB}_{0} ((μ α . P) \leq_{a} N) & = {P [μ α . P / α] \leq_{a} N}, \\ {subB}_{0} (P \leq_{a} μ α . N) & = {P \leq_{a} N [μ α . N / α]} . \end{aligned}$ It is undefined for unequal rigid atoms and for every other head mismatch. In particular, arrow decomposition compares the positive domain $P_{2}$ with the negative domain $N_{1}$ , and the positive codomain $P_{1}$ with the negative codomain $N_{2}$ .

Let $C$ be a finite work sequence and $H$ a finite set of visited constraints; commas concatenate work sequences. The syntactic algorithm $B_{0}$ is the following partial recursive function, where an omitted side condition falls through to the next equation: $\begin{aligned} B_{0} (H; \emptyset) & = id, \\ B_{0} (H; c, C) & = B_{0} (H; C) & c \in H, \\ B_{0} (H; α^{+} \leq_{a} α^{-}, C) & = B_{0} (H; C), \\ B_{0} (H; α^{+} \leq_{a} N, C) & = B_{0} (θ H; θ C) \circ θ & θ = θ_{α \leq_{a} N}, \\ B_{0} (H; P \leq_{a} α^{-}, C) & = B_{0} (θ H; θ C) \circ θ & θ = θ_{P \leq_{a} α}, \\ B_{0} (H; c, C) & = B_{0} (H \cup {c}; {subB}_{0} (c), C) & {subB}_{0} (c) is defined . \end{aligned}$ If no equation applies, $B_{0}$ fails. This syntax-tree presentation is partial: visited pairs stop direct recursive unfolding, but substitutions can still grow syntax. The terminating implementation below runs the same transitions on finite type automata.

Referenced from 3 locations

For example, the work list ${(α^{-} \to β^{+}) \leq_{a} ({Int}^{+} \to {Bool}^{-})}$ first becomes ${{Int}^{+} \leq_{a} α^{-}, β^{+} \leq_{a} {Bool}^{-}}$ . Lower-bound elimination changes only positive uses of $α$ ; upper-bound elimination changes only negative uses of $β$ .

Lemma 19.9 — One work-list step is equisatisfiable ¶

Every successful decomposition step preserves the solution set. Every atomic-elimination step preserves the upward-closed instance set of every attached polar scheme.

Referenced from 4 locations

Proof of Lemma 19.9 — One work-list step is equisatisfiable

Proof. Arrow inversion gives $(N_{1} \to P_{1}) \leq_{a} (P_{2} \to N_{2}) ⟺ P_{2} \leq_{a} N_{1} \land P_{1} \leq_{a} N_{2} .$ The lattice universal properties give the join-left and meet-right cases. Top and bottom cases follow from their bounds. Equal rigid heads discharge; unequal rigid heads have no solution in this frozen grammar. Nonrecursive atomic cases are lemma 19.6. Guarded recursive atomic cases are lemma 19.7. ◻

Inference, termination, and principality

Definition 19.10 — Finite polar type automata ¶

A local polar type automaton is a finite directed graph with a positive or negative polarity on each state, a finite head set at each state, and domain and range edges. The head alphabet is $H_{0} = {Unit, Bool, Int, String, arr} .$ An arrow state has one domain edge, which reverses polarity, and one range edge, which preserves it. A positive join and a negative meet take the union of the corresponding head sets and transitions. A guarded $μ$ -binder adds a back edge; guardedness ensures that every cycle crosses an arrow edge. Variables are distinguished states until an atomic elimination merges a variable face with a bound graph.

The procedure ${\hat{B}}_{0}$ starts from the automata for a finite constraint set and keeps a table of visited positive–negative state pairs. On an unvisited pair it performs exactly the transitions of (19.5)–(19.6): it follows reversed domain edges and aligned range edges, distributes a positive join or negative meet, discharges equal rigid heads, fails on unequal rigid heads, and realizes an atomic action by graph merging. A graph merge changes edges but creates no state. The returned quotient graph determines an idempotent bisubstitution. This finite graph procedure, not the partial syntax-tree recursion, is the total local solver.

Referenced from 2 locations

Algebraic Subtyping and Principal Inference

Theorem 19.11 — Local biunification ¶

Let $C$ be a finite set of sorted ${MLsub}_{0}$ constraints, and let its automata have $n$ states and $m$ transitions.

${\hat{B}}_{0} (C)$ terminates after visiting at most $n^{2}$ positive–negative state pairs, with worst-case work $O ((n + m)^{2})$ .
If it returns $ξ$ , then $ξ$ is stable and, for every polar scheme $S$ , $Inst (S ∣ C) = Inst (ξ (S) ∣ \emptyset) .$
It fails if and only if no substitution satisfies every constraint in $C$ .

Referenced from 5 locations

Proof of Theorem 19.11 — Local biunification

Proof. First compare a type with its graph. Induction on an acyclic unfolding shows that equal head languages give mutual subtyping: equal rigid letters use reflexivity; arrow letters use contravariance on domain edges and covariance on range edges; union at a positive state and union at a negative state use the join and meet universal properties, respectively. For a back edge, apply the same argument to one guarded unfolding. Every recurrence crosses an arrow, so guarded coinduction closes the comparison. Conversely, head inversion shows that mutual subtyping cannot change a rigid letter or exchange an arrow head with a rigid head. Thus two same-polarity local types mutually subtype exactly when their automata accept the same head-and-edge language.

Maintain the invariant that the unvisited state pairs are precisely the remaining positive-to-negative constraints. Arrow, join, meet, top, bottom, and rigid-head transitions preserve their solution set by lemma 19.9. An atomic graph merge applies (19.3). Thus lemma 19.6, lemma 19.7 preserve the instance set. Composition preserves (19.7); quotienting merged variable states makes the final action idempotent, and the merge orientation gives $ξ^{-} (α) \leq_{a} ξ^{+} (α)$ .

A failed transition exposes two unequal rigid heads or an arrow/rigid head mismatch. Head inversion makes either constraint unsatisfiable under every substitution. If no failure is exposed, the quotient action satisfies every visited pair by the invariant, so it is a solution. This proves both directions of clause 3. Finally, a merge creates no state and each recursive call marks a fresh pair. There are at most $n^{2}$ pairs; iterating over their incident transitions gives the stated quadratic bound. This is the finite-head instance of the automaton argument in [DM17]; the rigid-letter cases above are local and require no record encoding. ◻

Definition 19.12 — Polar inference ¶

Before combining subterms, rename their generalized type variables apart. A use of $\hat{x}$ takes a fresh copy of $Π (\hat{x})$ . The local partial algorithm $P_{0} (Π; e)$ has the following equations: $\begin{aligned} P_{0} (Π; \hat{x}) & = fresh (Π (\hat{x})), \\ P_{0} (Π; x) & = [x : α^{-}] α^{+}, & α \notin FV (Π), \\ P_{0} (Π; ()) & = [] {Unit}^{+}, \\ P_{0} (Π; q) & = [] {Bool}^{+}, & q \in {true, false} . \end{aligned}$ If $P_{0} (Π; e) = [Δ^{-}] P^{+}$ , then $P_{0} (Π; λ x . e) = [Δ_{x}^{-}] (Δ (x) \to P)^{+} .$ where $Δ (x) = ⊤$ when $x$ is absent. Let inference is $\begin{matrix} P_{0} (Π; e_{1}) = S_{1} = [Δ_{1}^{-}] P_{1}^{+}, P_{0} (Π, \hat{x} : S_{1}; e_{2}) = [Δ_{2}^{-}] P_{2}^{+}, \\ P_{0} (Π; let \hat{x} = e_{1} in e_{2}) = [Δ_{1}^{-} \land Δ_{2}^{-}] P_{2}^{+} . \end{matrix}$ For application, choose $β$ fresh for both subterm schemes and compute $\begin{matrix} P_{0} (Π; e_{i}) = [Δ_{i}^{-}] P_{i}^{+} (i = 1, 2), \\ ξ = {\hat{B}}_{0} ({P_{1}^{+} \leq_{a} (P_{2}^{+} \to β^{-})}), \\ P_{0} (Π; e_{1} e_{2}) = ξ ([Δ_{1}^{-} \land Δ_{2}^{-}] β^{+}) . \end{matrix}$ For a conditional, infer $[Δ_{i}^{-}] P_{i}^{+}$ for the condition and two branches, with index $i = 0, 1, 2$ , and compute $\begin{matrix} ξ = {\hat{B}}_{0} ({P_{0}^{+} \leq_{a} {Bool}^{-}}), \\ P_{0} (Π; if e_{0} then e_{1} else e_{2}) = ξ ([Δ_{0}^{-} \land Δ_{1}^{-} \land Δ_{2}^{-}] (P_{1}^{+} \lor P_{2}^{+})) . \end{matrix}$ If a solver call fails, the corresponding inference equation is undefined. Language-preserving automaton minimization may follow a successful call.

Referenced from 4 locations

The lambda-bound dependency matters. In $λ f . λ u . λ v . let \hat{g} = λ x . if f x then x else x in if true then \hat{g} u else \hat{g} v,$ the type of $\hat{g}$ depends on the type assigned to $f$ . Generalizing that dependency would allow the two uses of $\hat{g}$ to assume unrelated domains and would invalidate the enclosing typing.

Theorem 19.13 — Principal inference for MLsub_0 ¶

For every finite $Π$ and term $e$ , $P_{0} (Π; e)$ terminates. It fails exactly when no scheme $S$ satisfies $Π ⊢_{0} e : S$ . If it returns $S_{0}$ , then $Π ⊢_{0} e : S ⟺ S_{0} \leq_{\forall} S .$ Thus $S_{0}$ is sound, complete, and principal up to mutual scheme subsumption, not literal equality of type syntax.

Referenced from 4 locations

Proof of Theorem 19.13 — Principal inference for MLsub_0

Proof. Proceed by structural induction on $e$ . A lambda-bound variable introduces one fresh pair of faces, and a let-bound variable takes a renamed copy of its stored scheme, so (19.13) is exactly Var-Lam or Var-Let followed by Sub. Unit and Boolean constants use their corresponding rules.

For abstraction, the induction hypothesis factors every body typing through $[Δ^{-}] P^{+}$ . Deleting $x$ and placing $Δ (x)$ in the arrow domain turns the environment comparison in (19.1) into arrow contravariance. This is exactly the premise and conclusion of Abs; the convention $Δ (x) = ⊤$ handles an unused parameter.

For application, the two induction hypotheses factor the function and argument typings through their inferred schemes. Such instances form an App premise exactly when they satisfy $P_{1}^{+} \leq_{a} (P_{2}^{+} \to β^{-})$ for some result face $β^{-}$ . By theorem 19.11, applying $ξ$ in (19.11) replaces that constrained instance set by the equal unconstrained instance set. The pointwise meet records both lambda-bound environments. Hence the result is sound and every declarative application factors through it.

For a conditional, the same solver argument converts the condition constraint to an unconstrained scheme. Join is the least common result supertype, and the three-way environment meet records all dependencies, proving both directions of (19.13). For let, the induction hypothesis for $e_{1}$ gives the scheme stored for $\hat{x}$ ; the hypothesis for $e_{2}$ then factors every use of that fresh scheme. Rule Let combines exactly the two negative environments. These cases cover the term grammar. Each recursive inference call is on a proper subterm, and every solver call terminates by theorem 19.11, so $P_{0}$ terminates. Solver failure is unsatisfiability, which proves the failure clause. ◻

Theorem 19.14 — Richer MLsub inference boundary; exact import ¶

For the MLsub calculus, polar schemes, guarded equi-recursive types, and biunification algorithm of Dolan–Mycroft:

a returned bisubstitution is stable and solves the input constraints (Theorem 8), while failure implies unsatisfiability (Theorem 9);
the automaton implementation terminates; for $n$ states and $m$ transitions its worst-case work is $O ((n + m)^{2})$ ;
polar inference is sound, complete, and principal for that MLsub signature; and
equality of same-polarity types is equality of the languages accepted by their type automata (Theorem 10), so language-preserving minimization retains the inferred scheme’s instances.

Referenced from 4 locations

Algebraic Subtyping and Principal Inference

Proof of Theorem 19.14 — Richer MLsub inference boundary; exact import

Proof. Items 1, 2, and 4 are imported from [DM17]. The principality construction is the paper’s Section 4 inference development, with the complete principality statement and preorder equivalence given in [Dol17]. Its mechanism uses stable atomic actions on the two polar faces. The full source proof, not the local one-step lemma, establishes their most-generality and the induction that factors a declarative typing through the returned polar scheme. The let case retains the negative-environment dependencies named in definition 19.12. Termination is proved only after types are finite automata: every recursive call marks a previously unvisited pair of states, and there are at most $n^{2}$ pairs. ◻

Guardedness is substantive. Without it, a recursive type can contain an unguarded self-loop that contributes no constructor transition, so the finite-state descent used by both the semantic interpretation and the algorithm is not the stated one. Polarity is also substantive: replacing a variable on both faces reproduces the over-restricted type at the chapter’s opening.

Exercise 19.3 — A compact principal type ¶

★★☆ Infer a polar scheme for $λ b . λ x . λ y . if b then x else y$ . Show where the join occurs, and give two incomparable ordinary ML arrow types that are instances of the result.

Referenced from 3 locations

MLstruct is a separate Boolean system

Adding complement changes the semantic problem. A complement is not a negative face of an MLsub variable: it denotes the values outside a type. The 2022 MLstruct calculus has its own structural records, class tags, unions, intersections, complement, and inference judgment. Its soundness, completeness, and principality claims belong only to that frozen signature [PC22]; they are not instances of theorem 19.14.

Definition 19.15 — Boolean-algebraic comparison signature ¶

The comparison calculus ${BAS}_{0}$ has $T ::= 0 ∣ 1 ∣ α ∣ T \lor T ∣ T \land T ∣ \neg T ∣ T \to T ∣ μ α . T .$ Subtyping is semantic inclusion in the paper’s tagged-value model, and equi-recursive types satisfy the paper’s contractiveness condition. This is the MLstruct+ signature of Chau–Parreaux, not ${MLsub}_{0}$ , the 2022 MLstruct calculus, or Simple-sub.

Referenced from 3 locations

Algebraic Subtyping and Principal Inference

In ${BAS}_{0}$ , $T \land \neg T$ denotes $0$ and $T \lor \neg T$ denotes $1$ . Neither equation exists in ${MLsub}_{0}$ , whose meets and joins are polarity-indexed constructors rather than a single complemented Boolean algebra.

Theorem 19.16 — Boolean comparison boundary; exact import ¶

For the contractive MLstruct+ signature of definition 19.15, characteristic Boolean homomorphisms give the paper’s semantic-soundness characterization and terminating subtyping decision procedure. The theorem makes no claim about MLsub, the 2022 MLstruct calculus, or Simple-sub.

Referenced from 2 locations

Algebraic Subtyping and Principal Inference

Proof of Theorem 19.16 — Boolean comparison boundary; exact import

Proof. Import the characterization, soundness theorem, and decision procedure from [CP26]. Their domain, recursive-type contractiveness, and characteristic homomorphisms are hypotheses of this statement. No translation from MLsub polar schemes to that model has been given, so there is no premise by which theorem 19.14 could be transported. ◻

Simple-sub gives a shorter graph propagation algorithm and valuable implementation examples. Its randomized agreement tests are evidence about its implementation, not a proof that its calculus and MLsub have identical principal schemes [Par20].

Exercise 19.4 — Do not transfer the theorem ¶

★☆☆ Classify each phrase as belonging to ${MLsub}_{0}$ , ${BAS}_{0}$ , both, or neither: polar bisubstitution; Boolean complement; guarded equi-recursion; principal polar scheme; characteristic Boolean homomorphism. For every “both” answer, state the different role in each signature.

Referenced from 3 locations

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 19.5, then implement exercise 19.7.

Exercise 19.5 — Biunification trace ¶

★★☆ Trace $B_{0}$ on $(α^{-} \to β^{+}) \leq_{a} ((Int \lor Bool)^{+} \to (String \land γ)^{-}) .$ List the work set after arrow decomposition and give the positive and negative images of each variable after atomic elimination.

Referenced from 5 locations

Exercise 19.6 — Why equality loses programs ¶

★★☆ Give one satisfying assignment of the directed constraints from exercise 19.5 that ordinary equality unification rejects. Then give one equality solution and show that it is a special instance of the biunification result.

Referenced from 3 locations

Exercise 19.7 — Finite polar constraint solver ¶

★★★ Practical project.polar-biunification Implement the nonrecursive finite polar constraint fragment in Kappa: variables, top, bottom, arrows, joins, meets, constraint decomposition, and occurs-checking atomic elimination. Preserve the invariant that every queued constraint has positive left and negative right polarity. The finished program must solve an upper bound, solve a lower bound, decompose an arrow, reject a rigid mismatch, and reject a self-occurrence that this nonrecursive executable fragment does not solve with a guarded $μ$ -action. Its decidable acceptance test also rejects a constraint between distinct variables instead of silently discarding it. The exact five-case output is in appendix E; Kappa audit must return an empty list.

Referenced from 5 locations

Exercise 19.8 — A Boolean non-translation ¶

★★★ Assume a translation $t$ sends MLsub joins and meets to Boolean joins and meets. Prove that extending it by the equation $t (\neg T) = \neg t (T)$ is not yet a translation of typing schemes: identify the missing operation on negative environments and the missing preservation theorem for instantiation. Give a concrete Boolean equation whose source counterpart is not formed in ${MLsub}_{0}$ .

Referenced from 3 locations