ch:intersection-union: ch:intersection-union

Let $same : = λ^{(Nat \to Nat; Bool \to Bool)} x . x .$ The two body derivations are the variable trees $\frac{x : Nat \in x : Nat}{x : Nat ⊢ x : Nat} T - Var, \frac{x : Bool \in x : Bool}{x : Bool ⊢ x : Bool} T - Var .$ Therefore the single abstraction rule gives a derivation $D$ of $\frac{\begin{matrix} x : Nat ⊢ x : Nat \\ x : Bool ⊢ x : Bool \end{matrix}}{\cdot ⊢ same : (Nat \to Nat) \land (Bool \to Bool)} T - Abs .$ Let $I$ abbreviate the displayed intersection. Semantic intersection elimination gives $I \leq Nat \to Nat$ and $I \leq Bool \to Bool$ . Reuse the already constructed derivation $D$ in two subsumption steps, then intersect their conclusions: $\frac{\begin{matrix} \frac{\begin{matrix} D \\ I \leq Nat \to Nat \end{matrix}}{\cdot ⊢ same : Nat \to Nat} T - Sub \\ \frac{\begin{matrix} D \\ I \leq Bool \to Bool \end{matrix}}{\cdot ⊢ same : Bool \to Bool} T - Sub \end{matrix}}{\cdot ⊢ same : I} T - Inter .$ No second T-Abs instance and no pair constructor is introduced.

Use the single annotated abstraction $same = λ^{(Nat \to Nat; Bool \to Bool)} x . x .$ The two variable derivations under $x : Nat$ and $x : Bool$ , followed by T-Abs, give $\cdot ⊢ same : (Nat \to Nat) \land (Bool \to Bool) .$ It is a lambda value, not a pair. The intersection records two static specifications of this same value; subsumption selects either arrow and the value is applied directly.

Replacing $\land$ by $\times$ changes the type to a product type and therefore changes the canonical value to a pair, for example $(λ^{(Nat \to Nat)} x . x, λ^{(Bool \to Bool)} x . x) .$ Using it as a function now requires first choosing a component with $π_{1}$ or $π_{2}$ . Thus product formation packages two values and product elimination selects one; intersection introduction reuses one value and introduces no run-time constructor or projection.

Distribute intersection over the union and use absorption: $(A \lor B) \land A =_{D} A, (A \lor B) \land \neg A =_{D} B \land \neg A .$ Thus the positive branch receives all of $A$ , including the overlap $A \land B$ , while the negative branch receives precisely the part of $B$ outside $A$ .

For an empty negative branch, take $A = Nat \lor Bool$ and $B = Bool$ . Then $B \leq A$ , so $B \land \neg A =_{D} 0$ . For a proper refinement, take $A = Nat$ and $B = Nat \lor Bool$ . Disjointness of the two basic tags gives $B \land \neg A =_{D} Bool and Bool \leq Nat \lor Bool, Bool \neq_{D} Nat \lor Bool .$ Both examples use only the basic-tag algebra fixed in the chapter.

A sum value carries an injection tag: it is explicitly $inl v$ or $inr v$ . The corresponding root reduction inspects that tag, chooses a branch, and substitutes the stored payload.

A value of $A \lor B$ carries no additional constructor. It is the same underlying value that was assigned $A$ , $B$ , or both, and the two denotations may overlap. Consequently there is no left/right tag for an ordinary sum-case reduction to inspect and no distinguished payload to substitute. The chapter’s typecase is a different operation: it applies a decidable structural test $v ⊩ U$ to the existing value and refines its binder type. Treating $A \lor B$ as $A + B$ would invent run-time data that semantic union deliberately does not contain.

Let a finite graph $R$ belong to both $A \to C$ and $B \to D$ . For any edge $(d, r) \in R$ whose input lies in $[[A \lor B]]$ , at least one of the following holds. If $d \in [[A]]$ , membership in $A \to C$ gives $r \in [[C]]$ ; if $d \in [[B]]$ , membership in $B \to D$ gives $r \in [[D]]$ . In either case $r \in [[C \lor D]]$ , and in particular $r \neq Ω$ . Hence $(A \to C) \land (B \to D) \leq (A \lor B) \to (C \lor D) .$

For the converse, choose pairwise-disjoint nonempty $A, B, C, D$ , an element $a \in [[A]]$ , and $d \in [[D]]$ . The one-edge graph $R = {(a, d)}$ belongs to $(A \lor B) \to (C \lor D)$ , because its input is in the domain union and its output is in $D \leq C \lor D$ . It does not belong to $A \to C$ , since $a \in A$ but $d \notin C$ . Therefore it is not in the intersection on the left, disproving the converse inclusion.

Choose any $d \in D$ and take the one-edge graph $R = {(d, Ω)} .$ It belongs to $0 \to 1$ : no input lies in $[[0]] = \emptyset$ , so the arrow condition is vacuous. It does not belong to $1 \to 1$ : now $d \in [[1]] = D$ , but the required output would have to lie in $D$ , whereas $Ω \in D_{Ω} ∖ D$ .

Thus $0 \to 1$ recognizes every finite graph, including graphs that fail on some inputs, while $1 \to 1$ requires a successful $D$ -valued output on every represented input edge. The extra marker $Ω$ is precisely what makes those two types different.

Expand the derived meet and then use the two mutually recursive clauses: $a_{1} \land (a_{2} \lor \neg a_{3}) = \neg (\neg a_{1} \lor \neg (a_{2} \lor \neg a_{3})) .$ Now $\overset{―}{N} (\neg a_{1}) = N (a_{1}) = {({a_{1}}, \emptyset)},$ whereas $\overset{―}{N} (\neg (a_{2} \lor \neg a_{3})) = N (a_{2} \lor \neg a_{3}) = {({a_{2}}, \emptyset), (\emptyset, {a_{3}})} .$ The negative-union clause takes pairwise unions of the positive and negative sets. Therefore $N (a_{1} \land (a_{2} \lor \neg a_{3})) = {({a_{1}, a_{2}}, \emptyset), ({a_{1}}, {a_{3}})} .$ Its two clauses denote respectively $a_{1} \land a_{2}$ and $a_{1} \land \neg a_{3}$ , as distributivity predicts.

For $P = {A \times B}$ and $N = {C \times D}$ , there are two choices of $N^{'} \subseteq N$ . If $N^{'} = \emptyset$ , then $L (P, N^{'}) = A, R (P, N, N^{'}) = B \land \neg D,$ so this component is empty exactly when $A =_{D} 0$ or $B \leq D$ . If $N^{'} = N$ , then $L (P, N^{'}) = A \land \neg C, R (P, N, N^{'}) = B,$ so it is empty exactly when $A \leq C$ or $B =_{D} 0$ . By the product-empty condition, the original type is empty exactly when $(A =_{D} 0 \lor B \leq D) \land (A \leq C \lor B =_{D} 0) .$ If $A =_{D} 0$ or $B =_{D} 0$ , this conjunction holds immediately. Otherwise the two clauses force $B \leq D$ and $A \leq C$ . Conversely those two inclusions close the respective components. Hence the condition is exactly $A =_{D} 0 or B =_{D} 0 or (A \leq C and B \leq D) .$

Apply lemma 9.12 to the two positive atoms and the negative atom $A \to B$ . The four choices of $P^{'}$ give, respectively, $\begin{array}{cl} P^{'} & required alternative \\ \emptyset & A =_{D} 0 or B_{1} \land B_{2} \leq B, \\ {1} & A \leq A_{1} or B_{2} \leq B, \\ {2} & A \leq A_{2} or B_{1} \leq B, \\ {1, 2} & A \leq A_{1} \lor A_{2} . \end{array}$ For example, the second row rewrites $A \land \neg A_{1} =_{D} 0$ as $A \leq A_{1}$ and $B_{2} \land \neg B =_{D} 0$ as $B_{2} \leq B$ . In the last row the codomain alternative is unavailable because $P^{'} = P$ ; the $Ω$ output is the witness that forces domain coverage. The conjunction of these four alternatives is therefore necessary and sufficient.

Put $N_{t} = Nat$ , $B_{t} = Bool$ , and $S_{t} = N_{t} \lor B_{t}$ . For the negative arrow $S_{t} \to N_{t}$ , the first two subsets of $P = {N_{t} \to N_{t}, B_{t} \to B_{t}}$ give $\begin{array}{ccc} P^{'} & DomOb (P^{'}) & CodOb (P^{'}) \\ \emptyset & S_{t} & \neg N_{t} \land N_{t} \land B_{t} =_{D} 0 \\ {N_{t} \to N_{t}} & B_{t} & \neg N_{t} \land B_{t} =_{D} B_{t} . \end{array}$ The empty-subset row closes on its codomain component. In the next row, both $B_{t}$ components are nonempty, so this is the first row that fails.

The failed row exposes the one-edge counterexample $R = {(true, true)} .$ It belongs to $N_{t} \to N_{t}$ vacuously and to $B_{t} \to B_{t}$ directly, so it inhabits their intersection. It does not inhabit $S_{t} \to N_{t}$ , because its input belongs to $S_{t}$ but its output is a Boolean rather than a natural. The requested inclusion is therefore false.

Put $A = 0 \to 1$ and $X = (A \to 1) \land A$ . The empty graph is an element of $A$ , since every graph inhabits $0 \to 1$ , and it is an element of $A \to 1$ because it has no edge violating that arrow. Hence $X \neq_{D} 0$ .

Under $x : X$ , both occurrences synthesize $X$ . Intersection elimination gives $X \leq A = 0 \to 1$ and $X \leq A \to 1$ . Since $X \leq A$ , arrow contravariance gives $A \to 1 \leq X \to 1$ ; transitivity yields $X \leq X \to 1$ . These intermediate inclusions establish the sole callability premise of T-App. For the positive arrows $A \to 1$ and $0 \to 1$ , the $K^{'} = \emptyset$ output obligation contributes $1$ because nonempty $X$ is not below $0$ ; all other contributions are at most $1$ . Therefore $X \circ X =_{D} 1$ , and $\frac{\begin{matrix} x : X ⊢ x : X \\ x : X ⊢ x : X \\ X \leq X \to 1 \end{matrix}}{x : X ⊢ x x : 1} T - App .$ The enclosing one-arrow interface then gives $\cdot ⊢ λ^{(X \to 1)} x . x x : X \to 1$ .

For the variable case, substituting for the distinguished variable uses the supplied derivation $Γ ⊢ v : A$ ; every other lookup is unchanged. For the abstraction case, alpha-rename its binder $y$ away from $x$ and every free variable of $v$ . Each premise has the form $Γ, x : A, y : C_{i} ⊢ e : D_{i} .$ Fresh-variable weakening gives $Γ, y : C_{i} ⊢ v : A$ , and the induction hypothesis gives $Γ, y : C_{i} ⊢ e [v / x] : D_{i} .$ Reapplying T-Abs preserves the written interface. Consequently, at a beta root, lemma 9.31 selects the required body premises, applies this substitution case, intersects the resulting typings, and subsumes to the application output. This is exactly the beta case of theorem 9.32.

Suppose the positive root fires: $caseType v as x in U \Rightarrow e_{+} ∣ e_{-} ⟶ e_{+} [v / x], v ⊩ U .$ Inversion of T-Case gives $Γ ⊢ v : S$ . Value refinement gives both $Γ ⊢ v : S \land U$ and $S \land U \neq_{D} 0$ . The latter fact makes the conditional positive premise of T-Case active, so inversion also gives $Γ, x : S \land U ⊢ e_{+} : B_{+}$ . Substitution yields $Γ ⊢ e_{+} [v / x] : B_{+}$ , and $B_{+} \leq B_{+} \lor B_{-}$ followed by T-Sub restores the type of the whole case.

For the negative root, $v ⊮ U$ . Value refinement instead gives $Γ ⊢ v : S \land \neg U$ and $S \land \neg U \neq_{D} 0$ . Thus the negative conditional premise is active, substitution gives $Γ ⊢ e_{-} [v / x] : B_{-}$ , and union introduction by subsumption gives $Γ ⊢ e_{-} [v / x] : B_{+} \lor B_{-}$ .

Nonemptiness is load bearing in both cases: it turns the selected implication inside T-Case into an available typing premise. An actually selected branch cannot be one of the empty branches whose body was deliberately not typechecked.

Write $I = (Nat \to Nat) \land (Bool \to Bool) .$ The two successful body checks make $syn (same) = I$ . For an argument synthesized at $Nat$ , the subsets of the two positive arrows contribute $0$ or $Nat$ to (9.13), so $I \circ Nat =_{D} Nat$ . Symmetrically, $I \circ Bool =_{D} Bool$ .

For $S = Nat \lor Bool$ , neither singleton domain covers $S$ . The two proper singleton subsets therefore contribute the opposite codomains, and $I \circ S =_{D} Nat \lor Bool .$ Callability follows from (9.2). Thus all three applications synthesize, and the union application retains both input–output alternatives rather than choosing one branch prematurely.

Let $A = 0 \to 1$ and $X = (A \to 1) \land A$ , as in the chapter. Under $x : X$ , both variable calls synthesize $X$ . For $x x$ , the checker therefore sets $F = S = X$ . Intersection elimination gives $X \leq A = 0 \to 1$ . It also gives $X \leq A \to 1$ ; since $X \leq A$ , arrow contravariance yields $A \to 1 \leq X \to 1$ , hence $X \leq X \to 1$ . Both algorithmic callability tests succeed and the least-output calculation returns ${syn}_{x : X} (x x) = X \circ X =_{D} 1.$

The annotated abstraction has the one-arrow interface $X \to 1$ . Its body check succeeds because the synthesized body type is $1 \leq 1$ ; the interface is automatically well shaped when it has one arrow. Hence ${syn}_{\cdot} (λ^{(X \to 1)} x . x x) = X \to 1.$ This trace uses the written interface; it performs no search for an unannotated principal type.

For completeness, suppose the declarative last rule is $\frac{\begin{matrix} Γ ⊢ e_{1} : F \\ Γ ⊢ e_{2} : S \\ F \leq S \to B \end{matrix}}{Γ ⊢ e_{1} e_{2} : B} T - App,$ and the recursive checker calls return $F_{0} \leq F$ and $S_{0} \leq S$ . Transitivity, domain contravariance, and codomain covariance give $F_{0} \leq F \leq S \to B \leq S_{0} \to B \leq S_{0} \to 1.$ Here $S \to B \leq S_{0} \to B$ is the contravariant domain step, while $S_{0} \to B \leq S_{0} \to 1$ is the covariant codomain step using $B \leq 1$ . The chain through $S \to B \leq 0 \to 1$ uses both variances: $0 \leq S$ in the domain and $B \leq 1$ in the codomain. Thus $F_{0} \leq 0 \to 1$ , so both algorithmic callability tests succeed. The least-output characterization in lemma 9.23 then yields $F_{0} \circ S_{0} \leq B$ .

Conversely, a successful application call has recursive declarative typings $Γ ⊢ e_{1} : F_{0}$ and $Γ ⊢ e_{2} : S_{0}$ , together with $F_{0} \leq 0 \to 1$ and $F_{0} \leq S_{0} \to 1$ . The existence part of lemma 9.23 strengthens the latter fact to $F_{0} \leq S_{0} \to (F_{0} \circ S_{0}) .$ Rule T-App therefore reconstructs $Γ ⊢ e_{1} e_{2} : F_{0} \circ S_{0}$ , exactly the type returned by the synthesizer. These are the two directions of the application case.

Let $S = Nat \lor Bool$ and test $Bool$ . Boolean algebra gives $S \land Bool =_{D} Bool, S \land \neg Bool =_{D} Nat .$ Both are nonempty. In the then context, T-Var followed by T-Sub types $x : Bool$ ; in the else context the same two rules type $x : Nat$ . Rule T-Case, with the two scope premises and the scrutinee lookup $z : S ⊢ z : S$ , concludes $z : S ⊢ caseType z as x in Bool \Rightarrow x ∣ x : Bool \lor Nat .$ The order of the union records then before else; semantic equivalence makes it immaterial to subtyping.

Take $(a, i) = (⟨ 4, 5 ⟩, 1), (a^{'}, i^{'}) = (⟨ 4, 5 ⟩, 2) .$ Both arrays have the same unary type $Array Nat$ , and both indices have type $Nat$ . The first pair satisfies $0 \leq 1 < len (⟨ 4, 5 ⟩) = 2$ ; the second violates the strict upper bound because $2 < 2$ is false.

Unions, intersections, and complements of the two unary types can record only membership properties of the array value by itself or of the index value by itself. They cannot relate the chosen index to the length of the chosen array. Since the two pairs have identical component types, every such unary Boolean combination classifies them alike. Distinguishing them needs the binary refinement $i < len (a)$ , which is the next chapter’s proof obligation.