appendix sectionrules

Top-free disjoint intersections and merge elaboration

The exact source and target signatures of chapter 21 are $\begin{array}{rcl} A & ::= & Int ∣ A \to A ∣ A \times A ∣ A & A, \\ e & ::= & n ∣ x ∣ λ x . e ∣ e e ∣ (e, e) ∣ π_{i} e ∣ e,, e ∣ (e : A), \\ T & ::= & Int ∣ T \to T ∣ T \times T, \\ M & ::= & n ∣ x ∣ λ x . M ∣ M M ∣ (M, M) ∣ π_{i} M, \\ V & ::= & n ∣ λ x . M ∣ (V, V), \\ E & ::= & [] ∣ E M ∣ V E ∣ (E, M) ∣ (V, E) ∣ π_{i} E . \end{array}$ The target typing family is

x : T \in Γ

Γ ⊢ x : T

DT-Var

Γ ⊢ n : Int

DT-Int

Γ, x : T ⊢ M : U

Γ ⊢ λ x . M : T \to U

DT-Lam

Γ ⊢ M : T \to U

Γ ⊢ N : T

Γ ⊢ M N : U

DT-App

Γ ⊢ M : T

Γ ⊢ N : U

Γ ⊢ (M, N) : T \times U

DT-Pair

Γ ⊢ M : T_{1} \times T_{2}

Γ ⊢ π_{i} M : T_{i}

DT-Proj

Its root contractions and compatible call-by-value step are $(λ x . M) V ⇝_{0} M [V / x], π_{i} (V_{1}, V_{2}) ⇝_{0} V_{i}, \frac{M ⇝_{0} N}{E [M] ⟼ E [N]} .$ There is no $Top$ . Intersections erase to target products. The elaborating subtyping judgment $A <: B ⇝ c$ is generated by

Int <: Int ⇝ λ x . x

S-Int

B_{1} <: A_{1} ⇝ c_{1}

A_{2} <: B_{2} ⇝ c_{2}

A_{1} \to A_{2} <: B_{1} \to B_{2} ⇝ λ f . λ x . c_{2} (f (c_{1} x))

S-Arr

A_{1} <: B_{1} ⇝ c_{1}

A_{2} <: B_{2} ⇝ c_{2}

A_{1} \times A_{2} <: B_{1} \times B_{2} ⇝ λ p . (c_{1} (π_{1} p), c_{2} (π_{2} p))

S-Prod

A <: B_{1} ⇝ c_{1}

A <: B_{2} ⇝ c_{2}

A <: B_{1} & B_{2} ⇝ λ x . (c_{1} x, c_{2} x)

S-&R

A_{1} <: B ⇝ c

B ordinary

A_{1} & A_{2} <: B ⇝ λ p . c (π_{1} p)

S-&L_1

A_{2} <: B ⇝ c

B ordinary

A_{1} & A_{2} <: B ⇝ λ p . c (π_{2} p)

S-&L_2

The projection rules require an ordinary target: $Int$ , an arrow, or a product. There is no general transitivity rule.

Simple disjointness is $A * B ⟺ \neg \exists C . A <: C \land B <: C .$ The witness $C$ ranges over every raw type in the displayed grammar, not only well-formed types. Well-formed intersection formation is

Γ ⊢ A type

Γ ⊢ B type

A * B

Γ ⊢ A & B type

WF-&

Algorithmic disjointness distributes through intersections, compares arrow results, accepts products when either coordinate is disjoint, and accepts distinct ordinary heads.

The bidirectional judgments are $Γ ⊢ e \Rightarrow A ⇝ M$ and $Γ ⊢ e \Leftarrow A ⇝ M$ . Their complete rules are

x : A \in Γ

Γ ⊢ x \Rightarrow A ⇝ x

I-Var

Γ ⊢ n \Rightarrow Int ⇝ n

I-Int

Γ ⊢ e_{1} \Rightarrow A ⇝ M_{1}

Γ ⊢ e_{2} \Rightarrow B ⇝ M_{2}

Γ ⊢ (e_{1}, e_{2}) \Rightarrow A \times B ⇝ (M_{1}, M_{2})

I-Pair

Γ ⊢ e_{1} \Rightarrow A \to B ⇝ M_{1}

Γ ⊢ e_{2} \Leftarrow A ⇝ M_{2}

Γ ⊢ e_{1} e_{2} \Rightarrow B ⇝ M_{1} M_{2}

I-App

Γ ⊢ e \Rightarrow A_{1} \times A_{2} ⇝ M

Γ ⊢ π_{i} e \Rightarrow A_{i} ⇝ π_{i} M

I-Proj

Γ ⊢ e_{1} \Rightarrow A ⇝ M_{1}

Γ ⊢ e_{2} \Rightarrow B ⇝ M_{2}

A * B

Γ ⊢ e_{1},, e_{2} \Rightarrow A & B ⇝ (M_{1}, M_{2})

I-Merge

Γ ⊢ e \Leftarrow A ⇝ M

Γ ⊢ (e : A) \Rightarrow A ⇝ M

I-Ann

Γ, x : A ⊢ e \Leftarrow B ⇝ M

Γ ⊢ λ x . e \Leftarrow A \to B ⇝ λ x . M

I-Lam

Γ ⊢ e \Rightarrow A ⇝ M

A <: B ⇝ c

Γ ⊢ e \Leftarrow B ⇝ c M

I-Sub

All types in a typing derivation are well formed.