appendix sectionrules

Polar algebraic subtyping and biunification

Let $b \in {Unit, Bool, Int, String}$ . The ambient local algebra and its positive and negative sublanguages are $\begin{aligned} 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}$ The four atoms are primitive nullary heads. A general lambda-lifted scheme is $[Δ] T$ ; a polar scheme is $[Δ^{-}] P^{+}$ , with negative environment entries. For some type substitution $ρ$ , scheme subsumption is $\begin{aligned} [Δ] T \leq_{\forall} [Δ^{'}] T^{'} ⟺ & dom (Δ) \subseteq dom (Δ^{'}), \\ Δ^{'} (x) \leq_{a} ρ (Δ (x)), \\ ρ (T) \leq_{a} T^{'}, \end{aligned}$ where the middle condition ranges over $x \in dom (Δ)$ . The declarative rules are

Π (\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

No record encoding transfers a theorem to this calculus. The decisive decomposer equations are $\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} ((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} (b^{+} \leq_{a} b^{-}) & = \emptyset . \end{aligned}$ The two $μ$ -cases unfold one side; unequal rigid heads are undefined. Atomic rules apply $[N \land α / α^{-}, α / α^{+}] to α \leq_{a} N, [α / α^{-}, P \lor α / α^{+}] to P \leq_{a} α,$ with the guarded recursive actions (19.3). The recursive work list is $\begin{aligned} B_{0} (H; \emptyset) & = id, \\ B_{0} (H; c, C) & = B_{0} (H; C) & c \in H, \\ 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) defined . \end{aligned}$ The reflexive atomic case is deleted before the two elimination equations. The syntax-tree function is partial. The finite local automaton procedure ${\hat{B}}_{0}$ visits positive–negative state pairs, realizes atomic actions by graph merging, and is the terminating solver used by theorem 19.13. Equations (19.8)–(19.12) give the complete structural definition of $P_{0}$ . Nonrecursive atomic instance preservation is lemma 19.6; guarded recursive preservation is lemma 19.7.