Intersection, Union, and Semantic Subtyping

Suppose one function returns its argument unchanged. The same function satisfies both typings $$\mathsf{Nat}\to \mathsf{Nat}\text{and}\mathsf{Bool}\to \mathsf{Bool}.$$ An intersection type records several typings of one value. A single arrow with domain $\mathsf{Nat}\vee \mathsf{Bool}$ is also too weak if it forgets which result corresponds to which input. The useful type is therefore $$(\mathsf{Nat}\to \mathsf{Nat})\wedge (\mathsf{Bool}\to \mathsf{Bool}).$$ The same obstruction appears after control flow. If one branch returns a natural and another a Boolean, neither branch type is above the other. Their least set-theoretic join is the union type $\mathsf{Nat}\vee \mathsf{Bool}$, whose values may come from either branch.

Chapter 8 ordered the types built from the ordinary constructors, using a declarative relation ; joins and meets were properties of that order, not syntax. Here we change the language: $\vee ,\wedge ,\mathrm{\neg }$ are type constructors. Its semantic order is literal inclusion of type interpretations. The two orders obey familiar laws, but no unstated identification between them is used.

The notation suggests sets, but that suggestion is not yet a definition. For products, unions, and complements, ordinary sets suffice. For arrows, “the set of all functions between two sets” creates two problems. Write $D$ for the set of values we are trying to build. A function value would then be a set of input-output pairs drawn from $D$ itself, so the defining equation contains $D$ on both sides; Cantor’s theorem also forbids the resulting full-powerset equation. The required domain must therefore admit finite observable graphs without containing its full powerset, and its definition must be stratified so that every graph mentions only values from smaller ranks.

One value, two specifications

Fix three nonempty, pairwise disjoint sets of constants, with basic types $\mathsf{Nat}$, $\mathsf{Bool}$, and $\mathsf{Unit}$. We use constants $\mathsf{zero},\mathsf{succ}(\mathsf{zero}),\dots$, $\mathsf{true},\mathsf{false}$, and $\mathsf{unit}$.

Call the finite annotated calculus developed in this chapter ${\lambda }_{\mathsf{FG}}$, for “finite graphs.”

This spelling keeps term constants distinct from the empty type $0$ and universal type $1:=\mathrm{\neg }0$.

An overloaded abstraction carries a nonempty interface: $${\lambda }^{(A_1\to B_1;\dots ;A_n\to B_n)}x.e.$$ The annotation says that the same body must meet every arrow specification. The immediate obligation is to state when all of these arrow specifications may be assigned to one abstraction.

Take $e=x$. The complete abstraction derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{x:\mathsf{Nat}\in x:\mathsf{Nat}}{x:\mathsf{Nat}⊢x:\mathsf{Nat}}}\mathrm{T}-\mathrm{Var}\\ {\displaystyle \frac{x:\mathsf{Bool}\in x:\mathsf{Bool}}{x:\mathsf{Bool}⊢x:\mathsf{Bool}}}\mathrm{T}-\mathrm{Var}\end{array}}{\cdot ⊢{\lambda }^{(\mathsf{Nat}\to \mathsf{Nat};\mathsf{Bool}\to \mathsf{Bool})}x.x:(\mathsf{Nat}\to \mathsf{Nat})\wedge (\mathsf{Bool}\to \mathsf{Bool})}\mathrm{T}-\mathrm{Abs}.$$ Define the one-body overloaded identity in this derivation as $\mathsf{same}$; it has type (9.1) without relying on an undeclared primitive operation.

An intersection is not a product. A value of $A\times B$ is a pair, and projection selects a component. A value of $A\wedge B$ is one value accepted at both types. There is no intersection constructor and no projection from an intersection. Rule T-Inter reuses both the expression and its context.

The finite set-theoretic model

The finite model interprets the type grammar of definition 9.4: $\wedge ,\vee$, and $\mathrm{\neg }$ become Boolean operations on sets, while arrows become finite graphs.

For any candidate carrier $D$, put $D_{\mathrm{\Omega }}=D\cup \{\mathrm{\Omega }\}$, where $\mathrm{\Omega }\notin D$. Trying to solve $D=C+D^2+\mathcal{P}(D\times D_{\mathrm{\Omega }})$ is impossible: the full powerset is strictly larger than $D$. Finite graphs remove that obstruction.

Omitting $\mathrm{\Omega }$ creates a different failure. If graphs contained only edges in $D\times D$, then the empty graph would vacuously satisfy every arrow atom and there would be no finite witness that a graph is undefined on one chosen input. In particular the counterexample edge $$\{(d,\mathrm{\Omega })\}$$ needed to refute an arrow membership could not be formed. The extra output marker records precisely this finite failure observation.

Equivalently, rank a constant and the empty graph by zero, rank a pair one above the maximum rank of its components, and rank a nonempty graph one above the maximum rank of every input and non-$\mathrm{\Omega }$ output occurring in it. If $D_n$ is the set of terms of rank at most $n$, then $D=\bigcup _{n\in \mathbb{N}}{D}_n$. This cumulative presentation is the well-founded construction meant by “initial solution”; no cardinal fixed-point assumption is hidden in the notation.

The symbol $\mathrm{\Omega }$ records that a graph may fail on an input. It is not a denotation of the empty type and belongs to no subset of $D$.

The interpretation $[[-]]$ is defined only for types. Term typing and reduction remain syntactic, and the typecase test inspects the exact finite shape of a value. No adequacy theorem relating abstractions to graph elements is assumed.

Consequently, this chapter does not identify $A\le B$ with the coarser claim that every closed value typable at $A$ is typable at $B$. The graph order deliberately contains failure edges $(d,\mathrm{\Omega })$ used by arrow inversion and callability; a value-only order would erase those witnesses and would require a different completeness argument. No agreement between the two orders is needed for the syntactic safety theorem.

No recursion on $d$ is needed for these finite types: every denotation clause mentions only strict type subtrees. The rank recursion constructs the nested graph elements of the ambient domain $D$, while type denotation is structural recursion on finite types. The definition also shows why $1\to 1$ is not the type of every graph: an edge $(d,\mathrm{\Omega })$ violates it. Every graph does inhabit $0\to 1$, since there is no input in $[[0]]$ on which it can fail.

Proof of Proposition 9.7 — Boolean laws and variance

Proof. The Boolean and product claims are the corresponding set identities. For variance, a graph constrained on every $A$ input is constrained on the smaller set $A^{\prime }$, and every permitted $B$ output is a $B^{\prime }$ output. For (9.4), an entry whose input is in $A\vee B$ satisfies at least one arrow constraint, so its output lies in $C\vee D$. Formula (9.5) follows twice by variance. ◻

Neither inclusion is generally an equality. With disjoint nonempty $A,B,C,D$, a graph mapping an $A$ input to a $D$ output inhabits $(A\vee B)\to (C\vee D)$ but not $A\to C$, disproving the converse of (9.4). A graph mapping an $A$ input to $C$ and a $B$ input to $D$ inhabits $(A\to C)\wedge (B\to D)$ but not $(A\vee B)\to (C\wedge D)$, disproving the converse of (9.5). The empty graph inhabits every arrow; cardinality arguments about total mathematical functions therefore do not describe this model.

Proof of Corollary 9.8 — Subtyping is emptiness

Proof. $[[A\wedge \mathrm{\neg }B]]=[[A]]\setminus [[B]]$. ◻

Deciding emptiness

Set inclusion is transitive, but deciding $A\le B$ requires a finite procedure on type syntax. We reduce the query to emptiness of $A\wedge \mathrm{\neg }B$.

Proof of Lemma 9.10 — DNF correctness

Proof. Simultaneous induction on $A$. For $A=0$, take the empty family of clauses; for an atom, the singleton clause has exactly the atom’s denotation. Union on the positive side is set union. On the negative side, clause pairing is justified by the explicit identity $$(\bigcap P_1\setminus \bigcup N_1)\cap (\bigcap P_2\setminus \bigcup N_2)=\bigcap (P_1\cup P_2)\setminus \bigcup (N_1\cup N_2).$$ Taking the union over all pairs of clauses gives the required complement of a union. Complement exchanges the two simultaneous induction hypotheses. ◻

It remains to decide whether a single clause is empty. If its positive atoms have two different shapes, it is empty because the three summands of $D$ are disjoint. Otherwise each possible runtime shape yields one obligation.

For fixed finite sets $P,N$ of product atoms and $N^{\prime }\subseteq N$, write

Proof of Lemma 9.11 — Product decomposition

Proof. For sets $X_i,Y_i$ use $$\bigcap _{i\in P}(X_i\times Y_i)\setminus \bigcup _{i\in N}(X_i\times Y_i)=\bigcup _{N^{\prime }\subseteq N}(\bigcap _P{X}_i\setminus \bigcup _{N^{\prime }}{X}_i)\times (\bigcap _P{Y}_i\setminus \bigcup _{N\setminus N^{\prime }}{Y}_i).$$ A finite union of products is empty exactly when every product has an empty component. Interpreting the two components gives (9.7). ◻

For a concrete trace, normalize $$(\mathsf{Nat}\times \mathsf{Bool})\wedge \mathrm{\neg }(\mathsf{Nat}\times \mathsf{Nat}).$$ Here $P=\{\mathsf{Nat}\times \mathsf{Bool}\}$ and $N=\{\mathsf{Nat}\times \mathsf{Nat}\}$. For $N^{\prime }=\varnothing$ the two components are $\mathsf{Nat}$ and $\mathsf{Bool}\wedge \mathrm{\neg }\mathsf{Nat}{=}_{\mathcal{D}}\mathsf{Bool}$, so neither is empty. For $N^{\prime }=N$ the left component is $\mathsf{Nat}\wedge \mathrm{\neg }\mathsf{Nat}{=}_{\mathcal{D}}0$. Because the condition of lemma 9.11 fails at the first subset, the whole type is nonempty; $(\mathsf{zero},\mathsf{true})$ is a witness. This is the complete product calculation before the additional failure edge $\mathrm{\Omega }$ enters the arrow case.

For arrows, let $P$ and $N$ be finite sets of arrow atoms. Fix a negative arrow $A_0\to B_0\in N$. For $P^{\prime }\subseteq P$ put $$\mathrm{DomOb}(P^{\prime })=A_0\wedge \underset{A\to B\in P^{\prime }}{\bigwedge }\mathrm{\neg }A,\mathrm{CodOb}(P^{\prime })=\mathrm{\neg }{B}_0\wedge \underset{A\to B\in P\setminus P^{\prime }}{\bigwedge }B.$$

Proof of Lemma 9.12 — Arrow decomposition

Proof. An arrow denotes the finite powerset of the complement, taken inside $D\times D_{\mathrm{\Omega }}$, of $[[A]]\times (D_{\mathrm{\Omega }}\setminus [[B]])$. For finite families, $$\bigcap _{i\in P}{\mathcal{P}}_f(X_i)\subseteq \bigcup _{j\in N}{\mathcal{P}}_f(X_j)⟺\text{some }j\in N\text{ satisfies }\bigcap _{i\in P}{X}_i\subseteq X_j.$$ If some $j$ works, the right-hand inclusion immediately implies the left. Conversely, if no $j$ works, choose one witness outside each $X_j$; the finite set of witnesses belongs to every ${\mathcal{P}}_f(X_i)$ but to none of the ${\mathcal{P}}_f(X_j)$, contradicting the left-hand inclusion. Expanding the chosen inclusion says that every bad edge for $A_0\to B_0$ must be bad for some positive arrow: $$[[A_0]]\times (D_{\mathrm{\Omega }}\setminus [[B_0]])\subseteq \bigcup _{A_i\to B_i\in P}[[A_i]]\times (D_{\mathrm{\Omega }}\setminus [[B_i]]).$$ Suppose an edge $(d,\delta )$ is uncovered, and define its exact miss set $$M=\{A_i\to B_i\in P\mid d\notin [[A_i]]\}.$$ Then $d\in [[\mathrm{DomOb}(M)]]$. If $M\ne P$, the uncoveredness condition forces $\delta$ to be an ordinary output in every $B_i$ with $i\notin M$, so $\delta \in [[\mathrm{CodOb}(M)]]$. If $M=P$, the obligation at $P^{\prime }=P$ is only $\mathrm{DomOb}(P){=}_{\mathcal{D}}0$, and $d$ refutes it; no codomain witness is required. Equivalently, pairing $d$ with $\mathrm{\Omega }$ supplies an uncovered edge because $\mathrm{\Omega }$ belongs to no positive codomain.

Conversely, fix any $P^{\prime }\subseteq P$. A witness $d$ for its domain obligation misses every positive arrow in $P^{\prime }$. When $P^{\prime }\ne P$, an ordinary witness $\delta$ for its codomain obligation belongs to every remaining positive codomain. Hence no positive arrow covers $(d,\delta )$. For $P^{\prime }=P$, pair $d$ with $\mathrm{\Omega }$, which belongs to no positive codomain. In either case the edge violates (9.11). Thus the cover holds exactly when every $P^{\prime }$ has empty $\mathrm{DomOb}(P^{\prime })$, or has $P^{\prime }\ne P$ and empty $\mathrm{CodOb}(P^{\prime })$, which is (9.9). ◻

Proof of Lemma 20.11 — Basic-shape emptiness

Proof. Intersecting the positive basic denotations and removing the union of the negative ones is empty exactly when the displayed inclusion holds. The fixed family of basic tags is finite and pairwise disjoint, so the inclusion reduces to a finite tag-membership test. ◻

Proof of Theorem 9.16 — Emptiness and semantic subtyping are decidable

Proof. Compute $\tau =\mathcal{N}(A)$ and use the following memoized recursive test on its clauses. A clause is empty when it is empty at every runtime shape. For a candidate shape $k$, the clause is immediately empty at $k$ if it contains a positive atom whose shape is not $k$. At basic shape, apply lemma 20.11, restricting negative atoms to the basic shape and using $C$ for an empty positive family. At product shape, enumerate $N^{\prime }\subseteq N$ and recursively test whether $\mathcal{N}(L(P,N^{\prime }))$ or $\mathcal{N}(R(P,N,N^{\prime }))$ is empty. At function shape, try each negative arrow and, for every $P^{\prime }\subseteq P$, recursively test the domain obligation or the permitted codomain obligation from (9.9). A normal form is empty exactly when all of its clauses are empty. Cache answers by normalized syntax.

Every recursive obligation strictly decreases the multiset of depths of its nested product or arrow atoms, so this is a total procedure on finite type trees. Basic coverage and the exact product and arrow decomposition lemmas prove its soundness and completeness by induction on that multiset. Equivalently, its accepted memo table is contained in a finite simulation by lemma 9.14, lemma 9.15. Decide $A\le B$ by testing $A\wedge \mathrm{\neg }B$ and using corollary 9.8. ◻

If $q=|Q|$, there are at most $4^q$ clauses and $2^{4^q}$ normal forms over $Q$. Materializing the whole greatest- simulation table therefore gives only a finite decision proof, not a practical implementation. The memoized downward test above visits only obligations reached from the query, although its subset branching can still be exponential.

The overload inclusion from the opening can now be decided without guessing a graph. The following trace exhibits every recursive obligation made by the arrow clause.

The call-by-value calculus

The semantic relation can safely drive application, but only with an explicit callability premise. The function-shape top $0\to 1$ alone is not enough: it contains graphs that fail with $\mathrm{\Omega }$ on every nonempty domain.

The phrase “the value passes the test” must not hide a semantic oracle. Tests inspect only the finite value already obtained.

For example, $\mathsf{zero}\in B_{\mathsf{Nat}}$ and $\mathsf{true}\in B_{\mathsf{Bool}}$, so the membership derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{\mathsf{zero}\in B_{\mathsf{Nat}}}{\mathsf{zero}⊩\mathsf{Nat}}}\mathrm{M}-\mathrm{Basic}\\ {\displaystyle \frac{\mathsf{true}\in B_{\mathsf{Bool}}}{\mathsf{true}⊩\mathsf{Bool}}}\mathrm{M}-\mathrm{Basic}\end{array}}{(\mathsf{zero},\mathsf{true})⊩\mathsf{Nat}\times \mathsf{Bool}}\mathrm{M}-\mathrm{Pair}.$$ The labels M-Basic and M-Pair name the basic-constant and pair instances of the structural equations; they are decision clauses, not typing rules.

Consequently the selected branch is determined before substitution, and the complete root trace is No typing derivation is consulted by either step.

The role of $\mathrm{\Omega }$ is exact. An edge $(d,\mathrm{\Omega })$ records failure on $d$ and excludes its graph from $A\to B$ when $d\in [[A]]$. On $\mathrm{\Omega }$-free graphs every $A\to 1$ constraint permits every result; on all graphs, $0\to 1$ is the function-shape top. We therefore define a function type $F$ to be callable on a static argument type $S$ when $$F\le S\to 1.$$ Callability determines whether application is safe. Its least result type requires a separate calculation from the DNF clauses of $F$. For example, $0\to 1\nleqq S\to 1$ when $S$ is nonempty.

The application calculation needs one closure fact about negative arrows.

Proof of Lemma 9.21 — Strong disjunction for a function clause

Proof. The right-to-left implication is subsumption because $K\le K^{+}$. Conversely, suppose $K\le S\to R$ but choose a finite graph $G\in [[K^{+}]]\setminus [[S\to R]]$. Since $K$ is nonempty, choose $H\in [[K]]$. The union $G\cup H$ still satisfies every positive arrow: those conditions are universal over edges. For each negative arrow in the clause, $H$ already has an edge that violates it, and adjoining edges cannot remove that witness. Thus $G\cup H\in [[K]]$. The edge by which $G$ violates $S\to R$ also remains, so $G\cup H\notin [[S\to R]]$, a contradiction. ◻

Proof of Lemma 9.23 — Application-output characterization

Proof. Fix a nonempty clause $c$. By lemma 9.21, its negative arrows may be discarded when checking the supertype $S\to B$. Apply lemma 9.12 to the remaining positive arrows and the one negative arrow $S\to B$. At a subset $K^{\prime }\subseteq K_c$, its two emptiness tests translate exactly as For $K^{\prime }=K_c$, arrow decomposition permits only the first test; this is $S\le {\mathrm{Dom}}_c(P_c)$. The proper subsets give precisely the pairs in ${\rho }_c(P_c)$. Finally, $F\le S\to B$ holds exactly when every nonempty clause has this property. Intersecting their domain types and uniting their proper-subset pairs therefore gives $$F\le S\to B⟺S\le {\mathrm{Dom}}^{\ast }(F)\wedge \mathrm{\forall }(U,V)\in {\rho }^{\ast }(F).S\le U\vee V\le B.$$ The callability premise is precisely the domain conjunct. The remaining finite family says that every $V$ whose $U$ fails to cover $S$ is below $B$, which is equivalent to their union (9.13) being below $B$. DNF, emptiness, and every comparison are computable by theorem 9.16. ◻

Let $$I=(\mathsf{Nat}\to \mathsf{Nat})\wedge (\mathsf{Bool}\to \mathsf{Bool}).$$ Because $I\le 0\to 1$, the normalized conjunct $I\wedge (0\to 1)$ is equivalent to $I$; we use this simplified representative. Its one positive-arrow clause has index set $K_c=\{N,B\}$. The three proper subsets of $K_c$ give $${\rho }^{\ast }(I)=\{(0,\mathsf{Nat}\wedge \mathsf{Bool}),(\mathsf{Nat},\mathsf{Bool}),(\mathsf{Bool},\mathsf{Nat})\}.$$ The basic tags are disjoint, so the first output is $0$. Applying (9.13) three times yields Thus a precise argument retains its corresponding promise, while an imprecise argument returns exactly the union of the two results.

Projection has a simpler clausewise definition. Normalize $A_{\times }\wedge (1\times 1)$ and consider one nonempty product-shape clause with positive product atoms $P_c$ and negative product atoms $N_c$. Using (9.6), we make the construction explicit.

Proof of Lemma 9.25 — Projection-output characterization

Proof. The product decomposition writes each clause as the union, over $N^{\prime }\subseteq N_c$, of the rectangles $L(P_c,N^{\prime })\times R(P_c,N_c,N^{\prime })$. Its first-coordinate image is therefore the union of the left components whose right component is nonempty, exactly ${\mathrm{out}}_1$; the second-coordinate statement is symmetric. Inclusion of that finite union in $A$ is equivalent to inclusion of the whole clause in $A\times 1$. Taking the union over clauses proves both equivalences. Every emptiness test and finite union is computable by theorem 9.16. ◻

For $I=(A_1\to B_1;\dots ;A_n\to B_n)$, rule T-Abs concludes exactly $\underset{i}{\bigwedge }(A_i\to B_i)$; no negative arrow occurs in its conclusion. Thus intersection introduction and least-type synthesis use the same positive interface. By lemma 9.23, the least conclusion of T-App is $F\circ S$: its premise $F\le S\to B$ implies both $F\le 0\to 1$ and $F\le S\to 1$, and the characterization then gives $F\circ S\le B$. Every other conclusion follows from the least one by subsumption.

Proof of Lemma 9.27 — Structural rules

Proof. Each clause is an induction on its typing derivation.

For narrowing, the induction hypothesis says that each immediate typing premise remains derivable after replacing the outer context by its pointwise smaller context. In the variable case, if $y:C\in \mathrm{\Gamma }$ and ${\mathrm{\Gamma }}^{\prime }(y)=C^{\prime }\le C$, then T-Var gives ${\mathrm{\Gamma }}^{\prime }⊢y:C^{\prime }$ and T-Sub gives ${\mathrm{\Gamma }}^{\prime }⊢y:C$. Constants have no typing premise. Pair, projection, application, intersection, and subsumption reapply their rule to the induction hypotheses; their semantic side conditions mention types, not the context. For T-Abs, extend both contexts by the same $x:A_i$ and apply the induction hypothesis separately to each body derivation. For T-Case, extend both contexts by the same $x:S\wedge U$ or $x:S\wedge \mathrm{\neg }U$. The nonemptiness tests and the two scope premises are unchanged because the domains of $\mathrm{\Gamma }$ and ${\mathrm{\Gamma }}^{\prime }$ agree. Thus narrowing preserves both branch derivations of T-Case, including their nonemptiness and scope premises.

For weakening, induct again on the last rule. Constants and variables reapply their rules in the extended context, and each nonbinding constructor uses the induction hypotheses for its immediate subterms. Before an abstraction or typecase case, alpha-rename its binder away from the fresh variable $y$; then apply the induction hypothesis under the extended binder. The scope premise for a typecase remains true because its permitted domain has only grown.

For substitution, the induction hypothesis is the exact assertion $$\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢e:C,\mathrm{\Gamma }⊢v:A⟹\mathrm{\Gamma },\mathrm{\Delta }⊢e[v/x]:C,$$ where all types are unchanged because this calculus has no type variables. If $e=x$, use the assumed derivation $\mathrm{\Gamma }⊢v:A$; if $e=y\ne x$, reapply T-Var to the unchanged declaration of $y$. Constants are unchanged. Pair, projection, application, intersection, and subsumption apply the induction hypothesis to each term premise and then reapply the same rule.

For an abstraction with binder $z$, alpha-rename so that $z\ne x$ and $z\notin \mathrm{fv}(v)$. Apply the induction hypothesis directly with suffix $\mathrm{\Delta },z:A_i$; its value premise remains the assumed $\mathrm{\Gamma }⊢v:A$, and its conclusion has context $\mathrm{\Gamma },\mathrm{\Delta },z:A_i$. Then T-Abs rebuilds the abstraction. The typecase binder is handled identically, once under $z:S\wedge U$ and once under $z:S\wedge \mathrm{\neg }U$. Its conditional branch premises are unchanged because substitution does not alter $S$ or $U$. Finally, the elementary scope-substitution fact $$\mathrm{fv}(e)\subseteq \mathrm{dom}(\mathrm{\Gamma })\cup \{x\}⟹\mathrm{fv}(e[v/x])\subseteq \mathrm{dom}(\mathrm{\Gamma })$$ preserves both explicit branch-scope premises. Thus $\mathrm{\Gamma },x:A,\mathrm{\Delta }⊢e:C$ and $\mathrm{\Gamma }⊢v:A$ imply $\mathrm{\Gamma },\mathrm{\Delta }⊢e[v/x]:C$. ◻

For preservation we need to recover what a value’s outer constructor actually introduced, before subsumption obscured it.

Proof of Lemma 9.29 — Exact value typing

Proof. Induct on the typing derivation. Rules T-Const, T-Pair, and T-Abs give the three exact types and the displayed inversion data. For T-Sub, compose the induction-hypothesis inclusion with its subtype premise. For T-Inter, the two induction hypotheses have the same value syntax and hence the same exact type; combine their inclusions into the intersection. No other typing rule concludes with value syntax.

Nonemptiness is by value shape. The actual constant $c$ inhabits its tag; the pair of witnesses inhabits the product; and the empty finite graph inhabits every arrow in a nonempty interface, hence their intersection. ◻

Proof of Lemma 9.30 — Value refinement and canonical forms

Proof. Induct simultaneously on the value and test type to prove $\mathrm{vt}(v)\le U$ when $v⊩U$, and $\mathrm{vt}(v)\le \mathrm{\neg }U$ otherwise. Basic tags use disjointness; product tests use the two component hypotheses; and the $\mathsf{Fun}$ test uses the annotated-abstraction shape. Boolean cases are the corresponding set identities. Combine either inclusion with lemma 9.29 and subsume to the required intersection.

If $\mathrm{\Gamma }⊢v:0$, exact value typing would put the nonempty $\mathrm{vt}(v)$ below $0$, a contradiction. Finally, the three principal value shapes occupy disjoint summands of $D$; exact value typing therefore proves the pair and abstraction canonical forms. ◻

Union is a control-flow join

Subtyping introduces a union without changing the value. The following two rules are derived instances of T-Sub, using $A\le A\vee B$ and $B\le A\vee B$:

$\mathrm{\Gamma }⊢e:A$

$\mathrm{\Gamma }⊢e:A\vee B$

$\mathrm{\Gamma }⊢e:B$

$\mathrm{\Gamma }⊢e:A\vee B$

Unlike $A+B$, the type $A\vee B$ adds no injection tag. The runtime must test a property already possessed by the value.

For the binder typecase of definition 9.18, if $e:S$, the then branch receives $x:S\wedge U$ and the else branch receives $x:S\wedge \mathrm{\neg }U$. In particular, if $S=A\vee B$ and the test is $A$, the else type is $$(A\vee B)\wedge \mathrm{\neg }A{=}_{\mathcal{D}}B\wedge \mathrm{\neg }A$$ and is not generally $B$. If $B\le A$, the else refinement is $0$, so rule T-Case has no typing premise for that branch. A value selecting the else branch would have type $0$ by lemma 9.30, which is impossible. If $A$ and $B$ overlap, the refinement contains only the part of $B$ outside $A$.

The binder matters. Refining a freely repeated expression would require a proof that every occurrence denotes the same runtime result. The binder names the already evaluated value once and makes that equality syntactic.

Proof of Lemma 9.31 — Interface application

Proof. If the interface has one arrow $A_1\to B_1$, the value derivation $\mathrm{\Gamma }⊢v:S$ and the no-$0$-value clause of lemma 9.30 imply $S{\ne }_{\mathcal{D}}0$. If some $d$ lay in $[[S\setminus A_1]]$, the graph $\{(d,\mathrm{\Omega })\}$ would inhabit $A_1\to B_1$ but not $S\to R$; hence $S\le A_1$. Choose $d\in [[S]]$. If some $r\in [[B_1\setminus R]]$, the ordinary-output graph $\{(d,r)\}$ would again inhabit $A_1\to B_1$ but not $S\to R$; hence $B_1\le R$. Substitution therefore types the body at $B_1$, followed by subsumption.

Otherwise every $A_i$ is a test type. Arrow decomposition gives $S\le \underset{i}{\bigvee }{A}_i$. Put $J=\{i\mid v⊩A_i\}$. This set is nonempty: otherwise exact value refinement would put the nonempty $\mathrm{vt}(v)$ below the complement of every $A_i$, contradicting $\mathrm{vt}(v)\le S$. In the ${\rho }^{\ast }(I)$ obligation of definition 9.22, take $K^{\prime }=K_c\setminus J$. The exact value type is disjoint from $\underset{i\in K^{\prime }}{\bigvee }{A}_i$, so $S\nleqq \underset{i\in K^{\prime }}{\bigvee }{A}_i$; the other half of that obligation is therefore $\underset{i\in J}{\bigwedge }{B}_i\le R$. For each $i\in J$, (9.16) and subsumption type $\mathrm{\Gamma }⊢v:A_i$; the corresponding T-Abs premise and substitution type the body at $B_i$. Rule T-Inter combines the derivations, and subsumption gives $R$. ◻

The value-shape step in this lemma is the local restriction inherited from the finite calculus: annotated values admit the finite Boolean split needed by an interface. It is not a claim of occurrence completeness for arbitrary open expressions.

Proof of Theorem 9.32 — Preservation

Proof. Induct on the final typing rule. The induction hypothesis for an immediate premise $\mathrm{\Gamma }⊢e_0:C$ says that every step $e_0⟶e_0^{\prime }$ preserves exactly $C$.

First consider contextual steps. From $\mathrm{\Gamma }⊢(e_1,e_2):A_1\times A_2$, the last-rule premises type both components. If $e_1⟶e_1^{\prime }$, the induction hypothesis and T-Pair type $⟨e_1^{\prime },e_2⟩$; if $e_1$ is a value and $e_2⟶e_2^{\prime }$, they type $⟨e_1,e_2^{\prime }⟩$. Rules T-Proj and T-Case use the induction hypothesis for their scrutinee. Rule T-App uses it first for the function and then, when the function is a value, for the argument. In every case the semantic side conditions are unchanged. A step below T-Sub is followed by the same subsumption. A step below T-Inter is preserved by both induction hypotheses, after which T-Inter is reapplied. Constants, variables, and abstractions have no contextual step under the weak reduction of definition 9.20.

There remain four root families. For ${\pi }_1(v_1,v_2)⟶v_1$, lemma 9.29 gives $\mathrm{\Gamma }⊢v_i:A_i$ and $A_1\times A_2\le P$, with both $A_i$ nonempty. Equation (9.15) gives $P\le {\mathrm{proj}}_1(P)\times 1$. For every $a_1\in [[A_1]]$, choose $a_2\in [[A_2]]$; the two product inclusions put $(a_1,a_2)$ in $[[{\mathrm{proj}}_1(P)\times 1]]$. Hence $A_1\le {\mathrm{proj}}_1(P)$, and subsumption types the reduct. The second projection is symmetric.

For $({\lambda }^{I}x.e)v⟶e[v/x]$, inversion by lemma 9.29 recovers every premise $\mathrm{\Gamma },x:A_i⊢e:B_i$ and the inclusion $I\le F$. Inversion of T-App gives $F\le S\to B$; composing with $I\le F$ gives $I\le S\to B$. The result is exactly lemma 9.31 with $R=B$.

For the then typecase root, (9.16) derives $\mathrm{\Gamma }⊢v:S\wedge U$. Exact value typing shows that this refinement is nonempty, so the conditional then premise of T-Case is derivable. Substitution gives $\mathrm{\Gamma }⊢e_{+}[v/x]:B_{+}$, followed by subsumption to $B_{+}\vee B_{-}$. If the test fails, (9.16) gives $\mathrm{\Gamma }⊢v:S\wedge \mathrm{\neg }U$; substitution gives $\mathrm{\Gamma }⊢e_{-}[v/x]:B_{-}$, followed by subsumption to the same union. ◻

Proof of Theorem 9.33 — Progress and safety

Proof. Induct on the final typing rule, with induction hypothesis “the premise term is a value or it takes a step.” Constants and abstractions are values; a closed variable judgment is impossible. Subsumption does not change the term, so it uses its sole induction hypothesis. Intersection uses either premise, whose term is the same.

For a pair, step the left component if possible; if it is a value, step the right component; if both are values, the pair is a value. For a projection, first use the scrutinee induction hypothesis. If the scrutinee is a value, canonical forms from lemma 9.30 show that it is a pair, so one of the two projection roots applies.

For an application, first step its function, then its argument. If both are values, exact value typing gives a nonempty $V=\mathrm{vt}(v)$ with $V\le F\le 0\to 1$. Canonical forms therefore show that the function value is an annotated abstraction. The beta root therefore applies. For typecase, first step the scrutinee. Once it is a value, the exhaustive clauses of definition 9.19 decide exactly one of $v⊩U$ and $v⊮U$, so exactly one typecase root applies.

For safety, induct on the length of a reduction sequence. Preservation types the first reduct at $A$; progress applies again to it. Thus no finite prefix can end in a closed stuck nonvalue. ◻

The theorem applies exactly to the weak call-by-value relation of definition 9.20. To see why, consider a hypothetical extension $\mathsf{rnd}(A\vee B)$ that nondeterministically returns either an $A$-value or a $B$-value. If beta reduction duplicated this expression before evaluating it, the two copies in $(\lambda x.(x,x))\mathsf{rnd}(A\vee B)$ could choose differently, so the result would no longer have the promised correlation type $(A\times A)\vee (B\times B)$. Likewise, if a pair $(v_A,e_0):A\times 0$ could be formed while $e_0$ diverged and projection reduced before the second component became a value, ${\pi }_1(v_A,e_0)$ would produce an $A$-value from a product type with no values. These counterexamples require nondeterminism or divergence, neither of which belongs to the local calculus.

Least synthesis for annotated terms

All recursion is on a strict term subexpression and all side conditions call the terminating subtype decider, so synthesis terminates.

Proof of Lemma 20.37 — Synthesis soundness

Proof. Suppose ${\mathrm{syn}}_{\mathrm{\Gamma }}(e)=S$ and induct on $e$. Constants and variables use T-Const and T-Var; a pair uses the two induction hypotheses and T-Pair. For a projection, the recursive call gives $\mathrm{\Gamma }⊢e_0:P$, and the successful side condition gives $P\le 1\times 1$, so T-Proj returns the stated output. For an abstraction, success entails nonemptiness and well-shapedness of the interface. For every arrow $A_i\to B_i$, the body induction returns $C_i\le B_i$; subsumption checks that branch at $B_i$. Thus T-Abs returns exactly the written interface $I$.

For application, the recursive calls give $\mathrm{\Gamma }⊢e_1:F$ and $\mathrm{\Gamma }⊢e_2:S_0$. The two successful side conditions meet the hypotheses of lemma 9.23, whose right-to-left direction gives $F\le S_0\to (F\circ S_0)$. Rule T-App therefore derives the returned type. For typecase, a nonempty refinement has a recursively synthesized branch, which the induction hypothesis types at its returned type. An empty refinement contributes $0$ and activates no branch-typing premise. The scope checks and these two alternatives are exactly the premises of T-Case, so that rule derives the returned union. This proves $${\mathrm{syn}}_{\mathrm{\Gamma }}(e)=S⟹\mathrm{\Gamma }⊢e:S.$$ ◻

Proof of Lemma 20.38 — Synthesis leastness

Proof. Induct on a derivation of $\mathrm{\Gamma }⊢e:A$. The constant, variable, and pair cases follow directly from the induction hypotheses. Under T-Sub, a synthesized $S\le A_0$ is below the new conclusion by transitivity. The two T-Inter premises concern the same syntax; the deterministic recursive function therefore returns the same $S$ for both, and $S\le A$ and $S\le B$ imply $S\le A\wedge B$.

For T-Proj, let $A_{\times ,0}$ be the synthesized scrutinee type. The induction hypothesis gives $A_{\times ,0}\le A_{\times }$, hence $A_{\times ,0}\le 1\times 1$. From $A_{\times }\le {\mathrm{proj}}_i(A_{\times })\times 1$ (with the factors exchanged for $i=2$) and $A_{\times ,0}\le A_{\times }$, the projection characterization yields ${\mathrm{proj}}_i(A_{\times ,0})\le {\mathrm{proj}}_i(A_{\times })$. Thus the synthesized projection type is below the declarative conclusion. In T-Abs, the declarative rule guarantees that the written interface is well shaped. Each body induction returns a subtype of its declared $B_i$, so synthesis returns exactly that interface $I$, with $I\le I$.

For T-App, let the recursive calls return $F_0\le F$ and $S_0\le S$. The premise $F\le S\to B$, arrow variance, and transitivity give Thus both algorithmic callability checks succeed, and lemma 9.23 gives $F_0\circ S_0\le B$.

For T-Case, if the synthesized scrutinee type is $S_0\le S$, context narrowing changes a branch premise under $x:S\wedge U$ to one under $x:S_0\wedge U$. Replacing $U$ by $\mathrm{\neg }U$ gives the corresponding else-branch narrowing. If the new refinement is nonempty, the old one is also nonempty; the branch induction hypothesis therefore returns a subtype of $B_{+}$ or $B_{-}$. If the new refinement is empty, synthesis contributes $0$, already below the corresponding branch type. The explicit scope premises ensure that its preliminary scope checks succeed. Hence the returned union is below $B_{+}\vee B_{-}$. Therefore $$\mathrm{\Gamma }⊢e:A⟹{\mathrm{syn}}_{\mathrm{\Gamma }}(e)=S\text{ for some }S\le A.$$ ◻

Proof of Theorem 9.35 — Checker characterization

Proof. Apply lemma 20.38 for the forward implication. Conversely, lemma 20.37 types $e$ at $S$. Rule T-Sub then uses $S\le A$. The final claim is the quantified leastness conclusion. ◻

The qualification “with fixed annotations” is essential. The procedure checks a written interface; it neither infers one nor proves a principal-type theorem for an unannotated intersection language.

Occurrence typing and its boundary

Let $z:\mathsf{Nat}\vee \mathsf{Bool}$. The term $$\mathsf{caseType}z\mathsf{as}x\mathsf{in}\mathsf{Nat}\Rightarrow x\mid x$$ has type $\mathsf{Nat}\vee \mathsf{Bool}$. In the then branch, $$x:(\mathsf{Nat}\vee \mathsf{Bool})\wedge \mathsf{Nat}{=}_{\mathcal{D}}\mathsf{Nat};$$ in the else branch, $$x:(\mathsf{Nat}\vee \mathsf{Bool})\wedge \mathrm{\neg }\mathsf{Nat}{=}_{\mathcal{D}}\mathsf{Bool}.$$ Here is the complete derivation. Put $S=\mathsf{Nat}\vee \mathsf{Bool}$. The two subtype equalities above give $$\frac{\begin{array}{c}{\displaystyle \frac{x:S\wedge \mathsf{Nat}\in x:S\wedge \mathsf{Nat}}{x:S\wedge \mathsf{Nat}⊢x:S\wedge \mathsf{Nat}}}\mathrm{T}-\mathrm{Var}\\ S\wedge \mathsf{Nat}\le \mathsf{Nat}\end{array}}{x:S\wedge \mathsf{Nat}⊢x:\mathsf{Nat}}\mathrm{T}-\mathrm{Sub}.$$ $$\frac{\begin{array}{c}{\displaystyle \frac{x:S\wedge \mathrm{\neg }\mathsf{Nat}\in x:S\wedge \mathrm{\neg }\mathsf{Nat}}{x:S\wedge \mathrm{\neg }\mathsf{Nat}⊢x:S\wedge \mathrm{\neg }\mathsf{Nat}}}\mathrm{T}-\mathrm{Var}\\ S\wedge \mathrm{\neg }\mathsf{Nat}\le \mathsf{Bool}\end{array}}{x:S\wedge \mathrm{\neg }\mathsf{Nat}⊢x:\mathsf{Bool}}\mathrm{T}-\mathrm{Sub}.$$ Let ${\mathcal{D}}_{+}$ be the T-Sub derivation of $x:S\wedge \mathsf{Nat}⊢x:\mathsf{Nat}$, and let ${\mathcal{D}}_{-}$ be the T-Sub derivation of $x:S\wedge \mathrm{\neg }\mathsf{Nat}⊢x:\mathsf{Bool}$. Both refinements are nonempty, so the empty-branch implications are vacuous and the remaining instance is $$\frac{\begin{array}{c}{\displaystyle \frac{z:S\in z:S}{z:S⊢z:S}}\mathrm{T}-\mathrm{Var}\\ x\ne z\\ \mathrm{fv}(x)\subseteq \{z,x\}\\ {\mathcal{D}}_{+}\\ {\mathcal{D}}_{-}\end{array}}{z:S⊢\mathsf{caseType}z\mathsf{as}x\mathsf{in}\mathsf{Nat}\Rightarrow x\mid x:\mathsf{Nat}\vee \mathsf{Bool}}\mathrm{T}-\mathrm{Case}.$$

This is occurrence typing for one evaluated value named by a binder. General occurrence systems also refine repeated expressions, projections, and paths, and must prove that evaluation does not invalidate those refinements. No such claim is made here.

For array access, both $$(a,i)=([10,20],1)\text{and}(a^{\prime },i^{\prime })=([10,20],7)$$ have the same unary types $a,a^{\prime }:\mathsf{Array}\mathsf{Nat}$ and $i,i^{\prime }:\mathsf{Nat}$. Only the first array access satisfies Unary Boolean combinations cannot express a constraint relating an array value $a$, an index $i$, and $\mathsf{len}(a)$. Such a constraint requires dependent refinements, not another semantic-subtyping connective.

Results and signature boundaries

For ${\lambda }_{\mathsf{FG}}$ as defined in definition 9.4, definition 9.18, definition 9.19, definition 9.20 the development establishes Boolean semantic subtyping, a terminating and complete subtype decision procedure including arrows and negation, decidable checking of annotated terms, preservation, progress, and safety. The characteristic result is theorem 9.35: synthesis returns a least type for a term with fixed annotations and context.

The signatures separate the following constructions:

• $A\wedge B$ and $A\vee B$ classify one value by Boolean operations; $A\times B$ classifies a pair and $A+B$ a tagged value.

• The arrow laws (9.4) and (9.5) are inclusions; their reverse directions would require graph-membership conditions absent from the hypotheses.

• The checker decides a term with a written interface. Principal inference would also have to construct that interface.

• The safety theorem uses the weak call-by-value contexts of definition 9.20; call by name, strong reduction, nondeterminism, recursion, and effects define different step relations.

• The typecase rule refines its bound variable by $S\wedge U$ or $S\wedge \mathrm{\neg }U$. It introduces no path predicate for an arbitrary subexpression.

• The finite-graph interpretation maps types to subsets of $D$. Term typing and reduction remain syntactic, so no denotational adequacy claim for program phrases enters the safety proof.

• Dependent and non-idempotent intersections have different formation and elimination rules from the idempotent semantic intersection used here.

Sources.

The finite-graph model, Boolean normalization, and decomposition method follow Frisch, Castagna, and Benzaken [FCB08]; the chapter specializes their regular setting to finite type trees. For the binder/typecase boundary, see Castagna et al. [CLNL22]. The optional non-idempotent comparison follows Bernadet and Graham-Lengrand [BGL13].

Suggested first pass.

None of these problems is a prerequisite for later chapters. Begin with exercise 9.16; it reconstructs the chapter’s principal binder-refinement mechanism. Then use exercise 9.17 to check the exact handoff to refinements.

Exercise 9.16¶

★★☆ Repeat the complete occurrence derivation with the test $\mathsf{Bool}$. State both semantic subtype equalities and the order of the two branch types in the concluding union.

Referenced from 4 locations

• Intersection, Union, and Semantic Subtyping
• ch:intersection-union: ch:intersection-union

Exercise 9.17¶

★☆☆ Give two further same-typed array/index pairs, one satisfying (9.17) and one violating it. Explain why adding more unions and intersections of $\mathsf{Array}\mathsf{Nat}$ and $\mathsf{Nat}$ cannot distinguish them.

Referenced from 4 locations

• Intersection, Union, and Semantic Subtyping
• ch:intersection-union: ch:intersection-union

Exercise 20.19¶

★★★ Practical project.semantic-subtyping-counterexample Build and run a finite-graph inclusion checker. Maintain the invariant that every negative inclusion result carries a graph admitted by the left normal form and excluded by the right. The eight-case run must end with All 8 semantic-subtyping corpus cases passed., and the audit must be empty. Test three deliberately unsound variants: remove the $\mathrm{\Omega }$ guard, change universal arrow decomposition to existential choice, and bypass a typecase scope check. The named eight cases must reject each variant. Passing these finite witnesses is not a proof of the simulation or safety theorems.

Referenced from 4 locations

• Intersection, Union, and Semantic Subtyping
• Available supplements
• ch:intersection-union: ch:intersection-union

---

1. The semantic-subtyping literature writes $A\simeq B$ for equality of denotations. This book reserves $\simeq$ for equivalence of types in the homotopy-theoretic sense, where the coherence data is part of the definition, and writes ${=}_{\mathcal{D}}$ here. The relation is unchanged; only the glyph differs.↩︎