appendix sectionrules

Operation trees, CBPV, and deep handlers

For a finite signature $Σ (op) = P_{op} ⇝ R_{op}$ , well-founded operation trees, return, bind, and the handler fold are $\begin{array}{rcl} t & ::= & Ret (a) ∣ {Op}_{op} (p, k), k : R_{op} \to T_{Σ} A, \\ return a & = & Ret (a), \\ Ret (a) ≫ = f & = & f (a), \\ {Op}_{op} (p, k) ≫ = f & = & {Op}_{op} (p, λ r . k (r) ≫ = f), \\ {fold}_{r, h} (Ret (a)) & = & r (a), \\ {fold}_{r, h} ({Op}_{op} (p, k)) & = & h_{op} (p, λ q . {fold}_{r, h} (k (q))) . \end{array}$ Here $h_{op} : P_{op} \to (R_{op} \to C) \to C$ . A fold descends through a quotient by an effect theory exactly when it equalizes every generating equation under every tree-valued instantiation. It is sufficient, but stronger, for the entire $Σ$ -algebra to satisfy every generating equation under every carrier-valued assignment.

The source calculus used by the call-by-value and call-by-name translations has the complete typing rules

x : τ \in Γ

Γ ⊢ x : τ

S-Var

c : b is declared

Γ ⊢ c : b

S-Const

Γ, x : τ ⊢ e : σ

Γ ⊢ λ x . e : τ \to σ

S-Lam

Γ ⊢ e_{1} : τ \to σ

Γ ⊢ e_{2} : τ

Γ ⊢ e_{1} e_{2} : σ

S-App

Writing (w) for a source constant or lambda, the two big-step relations are

w ⇓_{v} w

V-Val

e_{1} ⇓_{v} λ x . e

e_{2} ⇓_{v} w_{2}

e [w_{2} / x] ⇓_{v} w

e_{1} e_{2} ⇓_{v} w

V-App

w ⇓_{n} w

N-Val

e_{1} ⇓_{n} λ x . e

e [e_{2} / x] ⇓_{n} w

e_{1} e_{2} ⇓_{n} w

N-App

The effect-free calculus ${CBPV}_{0}$ has $\begin{aligned} A & ::= b ∣ U C, & C & ::= F A ∣ A \Rightarrow C, \\ V & ::= x ∣ c ∣ thunk M, \\ M & ::= return V ∣ M to x . N ∣ force V \\ ∣ λ x . M ∣ M V . \end{aligned}$ Its complete typing rules are

x : A \in Γ

Γ ⊢_{v} x : A

V-Var

c : b declared

Γ ⊢_{v} c : b

V-Const

Γ ⊢_{c} M : C

Γ ⊢_{v} thunk M : U C

V-Thunk

Γ ⊢_{v} V : A

Γ ⊢_{c} return V : F A

C-Return

Γ ⊢_{c} M : F A

Γ, x : A ⊢_{c} N : C

Γ ⊢_{c} M to x . N : C

C-To

Γ ⊢_{v} V : U C

Γ ⊢_{c} force V : C

C-Force

Γ, x : A ⊢_{c} M : C

Γ ⊢_{c} λ x . M : A \Rightarrow C

C-Lam

Γ ⊢_{c} M : A \Rightarrow C

Γ ⊢_{v} V : A

Γ ⊢_{c} M V : C

C-App

Weak evaluation uses $K ::= [] ∣ K to x . N ∣ K V$ and the named roots $\begin{array}{rclcl} (return V) to x . N & ⟶ & N [V / x], & T o \\ force (thunk M) & ⟶ & M, & F o r c e \\ (λ x . M) V & ⟶ & M [V / x], & B e t a \\ K [M] & ⟶ & K [M^{'}] (M ⟶ M^{'}) . & F r a m e \end{array}$

For the annotated extension, $\begin{matrix} A ::= b ∣ U_{E} C, C ::= F A ∣ A \Rightarrow^{E} C, \\ Γ ⊢_{c} M : C! E . \end{matrix}$ The variable and constant rules remain unchanged. The complete replacement rules are

Γ ⊢_{c} M : C! E

Γ ⊢_{v} thunk M : U_{E} C

V-Thunk^Σ

Γ ⊢_{v} V : A

Γ ⊢_{c} return V : F A! \emptyset

C-Return^Σ

Γ ⊢_{c} M : F A! E_{1}

Γ, x : A ⊢_{c} N : C! E_{2}

Γ ⊢_{c} M to x . N : C! (E_{1} \cup E_{2})

C-To^Σ

Γ ⊢_{v} V : U_{E} C

Γ ⊢_{c} force V : C! E

C-Force^Σ

Γ, x : A ⊢_{c} M : C! E

Γ ⊢_{c} λ x . M : A \Rightarrow^{E} C! \emptyset

C-Lam^Σ

Γ ⊢_{c} M : A \Rightarrow^{E_{1}} C! E_{0}

Γ ⊢_{v} V : A

Γ ⊢_{c} M V : C! (E_{0} \cup E_{1})

C-App^Σ

Σ (op) = P ⇝ R

Γ ⊢_{v} V : P

Γ, x : R ⊢_{c} M : F A! E

Γ ⊢_{c} op V (x . M) : F A! ({op} \cup E)

C-Op

Γ ⊢_{c} M : C! E

E \subseteq E^{'}

Γ ⊢_{c} M : C! E^{'}

C-Weaken

The fixed pure state update used by the worked transaction is typed by

Γ ⊢_{v} V : S

Γ ⊢_{v} V^{+} : S

V-Next

A handler is $H = {return x \mapsto N_{r}; {op}_{i} (p_{i}; k_{i}) \mapsto N_{i}}_{i \in I}$ , with distinct operation names and $H = handled (H)$ . The judgment $Γ ⊢_{h} H : A [E_{in}] ⟹ B [E_{out}]$ means all of the following premises hold: $\begin{matrix} E_{in} ∖ H \subseteq E_{out}, \\ Γ, x : A ⊢_{c} N_{r} : F B! E_{out}, \\ Γ, p_{i} : P_{i}, k_{i} : U_{\emptyset} (R_{i} \Rightarrow^{E_{out}} F B) ⊢_{c} N_{i} : F B! E_{out} \end{matrix}$ for every handled ${op}_{i}$ with $Σ ({op}_{i}) = P_{i} ⇝ R_{i}$ . Its elimination rule is

Γ ⊢_{c} M : F A! E_{in}

Γ ⊢_{h} H : A [E_{in}] ⟹ B [E_{out}]

Γ ⊢_{c} handle M with H : F B! E_{out}

C-Handle

For an $op$ -open evaluation context $X_{op}$ , let $\hat{k} = thunk (λ y . handle X_{op} [M [y / x]] with H) .$ The exact deep-handler roots are $\begin{array}{rcl} handle (return V) with H & ⟶ & N_{r} [V / x], H a n d l e - R e t u r n, \\ handle X_{op} [op V (x . M)] with H & ⟶ & N_{op} [V / p, \hat{k} / k], H a n d l e - O p \end{array}$ when $H$ contains the displayed operation clause. If it does not, the Handle-Forward rule is $\begin{aligned} handle X_{op} [op V (x . M)] with H \\ ⟶ op V (y . handle X_{op} [M [y / x]] with H) . \end{aligned}$ In the first-order agreement fragment, $X ::= [] ∣ X to x . L ∣ handle X with G, op \notin handled (G),$ and general application is excluded; only administrative resumed continuations are admitted.