2.1 Profunctors

Arrows can be seen as strong monads in the bicategory $\mathbf{Prof}$ of categories and profunctors (Heunen and Jacobs, Reference Heunen and Jacobs2006; Jacobs et al., Reference Jacobs, Heunen and Hasuo2009; Asada, Reference Asada2010). We review profunctors and strong monads in $\mathbf{Prof}$ .

In the following definition of profunctors, we use coends, which are defined and gave an informal description in Appendix A. For more detailed explanation of coends, see also Mac Lane (Reference Mac Lane1971, Section 9) or Loregian (Reference Loregian2021, Section 1).

Definition 2.2 (profunctor, Bénabou, Reference Bénabou2000). Let $\mathbb{C}$ and $\mathbb{D}$ be categories. A profunctor from $\mathbb{C}$ to $\mathbb{D}$ is a functor $F \colon \mathbb{D}^{\mathrm{op}} \times \mathbb{C} \to \mathbf{Set}$ . For profunctors and , their composite is defined by taking the coend:

(2.1) \begin{equation} (G \circ F)(E , C) = \int^{D \in \mathbb{D}} G(E, D) \times F(D, C) \end{equation}

for $E \in \mathrm{Ob}(\mathbb{E})$ and $C \in \mathrm{Ob}(\mathbb{C})$ . The identity profunctor is defined by

\begin{equation*} \mathrm{I}_{\mathbb{C}}(C, D) = \mathbb{C}(C, D) \end{equation*}

for $C, D \in \mathrm{Ob}(\mathbb{C})$ . A 2-cell $\alpha \colon F \Rightarrow G$ between profunctors is a natural transformation.

A profunctor is an analogue of a binary relation $r \subseteq C \times D$ between two sets C and D. We identify the binary relation r with its characteristic function $D \times C \to 2$ . A composition $s \circ r \subseteq C \times E$ of two relations $r \subseteq C \times D$ and $s \subseteq D \times E$ is defined as follows:

\begin{equation*} (s \circ r)(e,c) \iff \exists d \in D.\, s(e, d) \land r(d, c).\end{equation*}

This definition of compositions is similar to the definition of compositions of profunctors (2.1) because the coend operator $\int^{D \in \mathbb{D}}({-})$ is an analogue of an existential quantifier $\exists D \in \mathbb{D}.\,({-})$ as described in Appendix A. The correspondence between profunctors and binary relations is summarised in Table 2.

Table 2. Analogy between profunctors and binary relations

A profunctor is a presheaf $G \colon \mathbb{C}^{\mathrm{op}} \to \mathbf{Set}$ on $\mathbb{C}$ . We have $(H \circ G) \circ F \cong H \circ (G \circ F)$ and $\mathrm{I}_{\mathbb{D}} \circ F \cong F \cong F \circ \mathrm{I}_{\mathbb{C}}$ . That is, associativity and unitality hold up to natural isomorphism, not strictly. Moreover, the class of small categories and profunctors forms a bicategory. Roughly speaking, a bicategory is a “category” whose hom-sets have a category structure and whose composition and identity are associative and unital up to isomorphism. See Appendix B.2 or (1994, Section 7.7) for the definition of bicategories. We write the bicategory of profunctors as $\mathbf{Prof}$ .

From a functor $F \colon \mathbb{C} \to \mathbb{D}$ , we can obtain two profunctors and which are defined by

\begin{equation*} {F}_{*}(D, C) = \mathbb{D}(D , FC), \qquad {F}^{*}(C, D) = \mathbb{D}(FC, D)\end{equation*}

on objects $C \in \mathrm{Ob}(\mathbb{C})$ and $D \in \mathrm{Ob}(\mathbb{D})$ . For morphisms f in $\mathbb{C}$ and g in $\mathbb{D}$ , ${F}_{*}(g, f)$ and ${F}^{*}(f, g)$ are also defined appropriately.

2.2 Monads in the bicategory of profunctors

To capture notions of computations, strong monads have been used in functional programming (Moggi, Reference Moggi1989, Reference Moggi1991). In this paper, to capture notions of computation, we use monads in the bicategory $\mathbf{Prof}$ instead of ordinary monads, that is monads in the 2-category $\mathbf{Cat}$ . For the definition of monads in 2-categories and bicategories, see Appendices B.1 and B.2.

We call a monad in $\mathbf{Prof}$ a promonad. A strong promonad is a promonad with a strength.

satisfying the axioms shown in Figure 1.

Fig. 1. Axioms for a strong promonad.

Hughes (Reference Hughes2000), Jacobs et al. (Reference Jacobs, Heunen and Hasuo2009), Asada (Reference Asada2010) showed that a promonad corresponds to an arrow type in Haskell. The unit $\eta \colon \mathrm{I}_{\mathbb{C}} \Rightarrow \mathcal{A}$ of a promonad $\mathcal{A}$ corresponds to $\mathtt{arr}$ : (x -> y) -> A x y:

The multiplication $\mu \colon \mathcal{A} \circ \mathcal{A} \Rightarrow \mathcal{A}$ of the promonad $\mathcal{A}$ corresponds to $\mathtt{(\mathrel{>\!\!>\!\!>})}$ : A x y -> A y z -> A x z:

The strength of the promonad $\mathcal{A}$ corresponds to $\mathtt{first}$ : A x y -> A (x, z) (y, z). The proof of the correspondence is complicated, see Asada (Reference Asada2010, Theorem 14):

From a monad, we can obtain a promonad:

Note that the profunctor is a functor $\mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbf{Set}$ , and we have ${\mathcal{T}}_{*}(C, D) = \mathbb{C}(C, \mathcal{T} D) = \mathop{\mathcal{K}\!\!\ell}(\mathcal{T})(C, D)$ where $\mathop{\mathcal{K}\!\!\ell}(\mathcal{T})$ is the Kleisli category for the monad $\mathcal{T}$ . Hence, each monad can be regarded as a promonad. In this sense, arrows are a generalisation of monads.

For a monad $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ in $\mathbf{Cat}$ , there exists a category $\mathop{\mathcal{E\!\!M}}(\mathcal{T})$ called the Eilenberg–Moore category of $\mathcal{T}$ . It satisfies the following property (Street, Reference Street1972):

(2.2) \begin{equation} \mathbf{Cat}(\mathbb{D}, \mathop{\mathcal{E\!\!M}}(\mathcal{T})) \cong \mathop{\mathcal{E\!\!M}}(\mathbf{Cat}(\mathbb{D}, \mathcal{T}))\end{equation}

where $\mathbf{Cat}(\mathbb{D}, \mathcal{T}) \colon \mathbf{Cat}(\mathbb{D}, \mathbb{C}) \to \mathbf{Cat}(\mathbb{D}, \mathbb{C})$ on the right-hand side is a monad on the functor category $\mathbf{Cat}(\mathbb{D}, \mathbb{C})$ defined by $\mathbf{Cat}(\mathbb{D}, \mathcal{T})(F) = \mathcal{T} \circ F$ . The category $\mathop{\mathcal{E\!\!M}}(\mathbf{Cat}(\mathbb{D}, \mathcal{T}))$ is the Eilenberg–Moore category of the monad $\mathbf{Cat}(\mathbb{D}, \mathcal{T})$ .

For a promonad in $\mathbf{Prof}$ , there exists a category $\mathop{\mathcal{E\!\!M}}(\mathcal{A})$ (Wood, Reference Wood1985) that satisfies

(2.3) \begin{equation} \mathbf{Prof}(\mathbb{D}, \mathop{\mathcal{E\!\!M}}(\mathcal{A})) \simeq \mathop{\mathcal{E\!\!M}}(\mathbf{Prof}(\mathbb{D}, \mathcal{A}))\end{equation}

where $\mathbf{Prof}(\mathbb{D}, \mathcal{A}) \colon \mathbf{Prof}(\mathbb{D}, \mathbb{C}) \to \mathbf{Prof}(\mathbb{D}, \mathbb{C})$ on the right-hand side is a monad on the profunctor category $\mathbf{Prof}(\mathbb{D}, \mathbb{C})$ defined by $\mathbf{Prof}(\mathbb{D}, \mathcal{A})(F) = \mathcal{A} \circ F$ .

• • $\mathrm{Ob}(\mathop{\mathcal{E\!\!M}}(\mathcal{A})) = \mathrm{Ob}(\mathbb{C})$ .

• • For $A, B \in \mathrm{Ob}(\mathop{\mathcal{E\!\!M}}(\mathcal{A}))$ , $\mathop{\mathcal{E\!\!M}}(\mathcal{A})(A, B) = \mathcal{A}(A, B)$ .

• • For $A \in \mathrm{Ob}(\mathop{\mathcal{E\!\!M}}(\mathcal{A}))$ , the identity on A is $\eta^{\mathcal{A}}_{A,A}(\mathrm{id}_A) \in \mathcal{A}(A, A)$ .

• • For $a \in \mathop{\mathcal{E\!\!M}}(\mathcal{A})(A, B)$ and $b \in \mathop{\mathcal{E\!\!M}}(\mathcal{A})(B, C)$ , the composition $b \circ a$ is $\mu^{\mathcal{A}}_{A, B, C}(a, b)$ .

There is an identity-on-objects functor $J \colon \mathbb{C} \to \mathop{\mathcal{E\!\!M}}(\mathcal{A})$ defined by $\eta^{\mathcal{A}}_{A, B} \colon \mathbb{C}(A, B) \to \mathcal{A}(A, B)$ . The functor J induces an adjunction ${J}_{*} \dashv {J}^{*}$ in $\mathbf{Prof}$ :

The promonad $\mathcal{A}$ coincides with the composition of ${J}_{*}$ and ${J}^{*}$ i.e., $\mathcal{A} \cong {J}^{*} \circ {J}_{*}$ .

2.3 Size issues

An arrow corresponds to a strong promonad, but when trying to interpret a programming language with, for example, $\mathbf{Set}$ , one faces size problems because the natural interpretation is not a set. That is, an endoprofunctor must be a functor $\mathcal{A} \colon \mathbf{Set}^{\mathrm{op}} \times \mathbf{Set} \to \mathbf{Ens}$ , not a functor $\mathbf{Set}^{\mathrm{op}} \times \mathbf{Set} \to \mathbf{Set}$ , because the composition of profunctors is defined by a coend. Hence, the interpretation $\mathcal{A}(\mathord{\left[\![{A}\right]\!]}, \mathord{\left[\![{B}\right]\!]})$ of an arrow type $A \rightsquigarrow B$ (in a Haskell-like notation, $\mathtt{Ar}\ A\ B$ , where $\mathtt{Ar}$ is an instance of the class $\mathtt{Arrow}$ ) is a class, not a set. Asada (Reference Asada2010) introduced $\mathbb{V}$ -small profunctors in . The size problem is solved using $\mathbf{Set}$ -small profunctors in .

Readers who are not concerned about size issues may skip the rest of this section. For the definition of enriched categorical notions such as $\mathbb{V}$ -categories and $\mathbb{V}$ -functors, see Appendix B.3 and Kelly (Reference Kelly1982, Section 1).

Definition 2.6 ( $\mathbb{V}$ -profunctors). Let $\mathbb{V}$ be a sufficiently cocomplete symmetric monoidal category and $\mathbb{C}$ and $\mathbb{D}$ be $\mathbb{V}$ -categories. A $\mathbb{V}$ -profunctor F from $\mathbb{C}$ to $\mathbb{D}$ , written , is a $\mathbb{V}$ -functor $F \colon \mathbb{D}^{\mathrm{op}} \otimes \mathbb{C} \to \mathbb{V}$ . A 2-cell $\alpha$ from $\mathbb{V}$ -profunctors to , written $\alpha \colon F \Rightarrow G$ is a $\mathbb{V}$ -natural transformation between the $\mathbb{V}$ -functors. For two $\mathbb{V}$ -profunctors and , their composite is defined by the following coend in $\mathbb{V}$ :

\begin{equation*} (G \circ F)(E, C) = \int^{D \in \mathbb{D}} G(E, D) \otimes F(D, C). \end{equation*}

The identity $\mathbb{V}$ -profunctor is defined by

\begin{equation*} \mathrm{I}_{\mathbb{C}}(C, D) = \mathbb{C}(C, D). \end{equation*}

The collection of small $\mathbb{V}$ -categories, $\mathbb{V}$ -profunctors and 2-cells, forms a bicategory . The bicategory $\mathbf{Prof}$ is the special case of where $\mathbb{V} = (\mathbf{Set}, \times, 1)$ .

Let $J \colon \mathbf{Set} \to \mathbf{Ens}$ be the embedding. A $\mathbf{Set}$ -small strong $\mathbf{Ens}$ -promonad is an $\mathbf{Ens}$ -functor $\mathcal{A} \colon \mathbf{Set}^{\mathrm{op}} \times \mathbf{Set} \to \mathbf{Ens}$ with 2-cells $\eta$ , $\mu$ and $\sigma$ which make $\mathcal{A}$ a strong $\mathbf{Ens}$ -promonad, and an $\mathbf{Ens}$ -functor $\mathcal{A}^{\circ} \colon \mathbf{Set}^{\mathrm{op}} \times \mathbf{Set} \to \mathbf{Set}$ satisfying

If a suitable $\mathbf{Set}$ -small strong $\mathbf{Ens}$ -promonad exists, then we can define the interpretation of an arrow type $A \rightsquigarrow B$ (which will be introduced in Section 4.1) by $\mathord{\left[\![{A \rightsquigarrow B}\right]\!]} = \mathcal{A}^{\circ}(\mathord{\left[\![{A}\right]\!]}, \mathord{\left[\![{B}\right]\!]})$ .

We will introduce an arrow calculus with operations and handlers in Section 4.1 and define models of the calculus as appropriate small promonads (Definition 5.1). As a concrete model, we will construct a $\mathbf{Set}$ -small strong $\mathbf{Ens}$ -promonad $\mathcal{A}$ which has sufficient structure to interpret the arrow calculus in Section 5.2.

3.1 Algebras of promonads

Let $\mathbf{1}$ be the category with a single object and a single morphism (the identity). For a monad $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ , a $\mathcal{T}$ -algebra is a functor $\mathbf{1} \to \mathop{\mathcal{E\!\!M}}(\mathcal{T})$ in $\mathbf{Cat}$ . Similarly, for a promonad , we call a profunctor in $\mathbf{Prof}$ an $\mathcal{A}$ -algebra where $\mathop{\mathcal{E\!\!M}}(\mathcal{A})$ is the Eilenberg–Moore category of $\mathcal{A}$ (Definition 2.5).

By (2.2), a $\mathcal{T}$ -algebra $a \colon \mathbf{1} \to \mathop{\mathcal{E\!\!M}}(\mathcal{T})$ corresponds to a $\mathbf{Cat}(\mathbf{1}, \mathcal{T})$ -algebra $\alpha$ , that is the following equation holds:

where $A \in \mathbb{C}$ , $\ulcorner {A} \urcorner \colon \mathbf{1} \to \mathbb{C}$ is the constant functor, and the 2-cell $\xi$ is defined by $\xi_{f} = f \colon \mathcal{T} U (f) \to Uf$ for a $\mathcal{T}$ -algebra $f \colon \mathcal{T} A \to A$ . Hence, specifying a $\mathcal{T}$ -algebra $a \colon \mathbf{1} \to \mathop{\mathcal{E\!\!M}}(\mathcal{T})$ is equivalent to specifying a morphism $\alpha \colon \mathcal{T} A \to A$ satisfying ordinary equations for a $\mathcal{T}$ -algebra.

Similarly, by (2.3), a $\mathcal{A}$ -algebra corresponds to a $\mathbf{Prof}(\mathbf{1}, \mathcal{A})$ -algebra $\alpha$ up to isomorphism, that is

The $\mathbf{Prof}(\mathbf{1}, \mathcal{A})$ -algebra $\alpha$ satisfies the following equations.

(3.1)

(3.2)

Note that (3.1) is equivalent to $\alpha_{X,Y}(\eta_{X,Y}(f), k) = (Gf)(k)$ for any $X, Y \in \mathbb{C}$ , $f \in \mathbb{C}(X, Y)$ and $k \in GY$ , and (3.2) is equivalent to $\alpha_{X,Z}(\mu_{X,Y,Z}(a, b), k) = \alpha_{X,Y}(a, \alpha_{Y,Z}(b, k))$ for any $X, Y, Z \in \mathbb{C}$ , $a \in \mathcal{A}(X, Y)$ , $b \in \mathcal{A}(Y, Z)$ and $k \in GZ$ .

Hence, specifying an $\mathcal{A}$ -algebra is equivalent to specifying a presheaf $G \colon \mathbb{C}^{\mathrm{op}} \to \mathbf{Set}$ and a 2-cell $\alpha \colon \mathcal{A} \circ G \Rightarrow G$ in $\mathbf{Prof}$ satisfying (3.1) and (3.2). We call such a pair $\langle G, \alpha \rangle$ also an algebra.

In other words, a homomorphism $h \colon \langle G, \alpha \rangle \to \langle H, \beta \rangle$ is a natural transformation from G to H that makes the following diagram commute:

for any $X, Y \in \mathbb{C}$ .

3.2 Arrow handlers as homomorphisms between algebras

A free $\mathcal{A}$ -algebra for a promonad $\mathcal{A}$ has a universal property, which is similar to the universal property for a free $\mathcal{T}$ -algebra for an ordinary monad $\mathcal{T}$ . Theorem 3.3 shows the universality of a free $\mathcal{A}$ -algebra. An effect handler for arrows is interpreted by the homomorphism induced by the universality.

Theorem 3.3. Let $\mathcal{A}$ be a promonad on $\mathbb{C}$ , $C \in \mathbb{C}$ , be a profunctor, that is a presheaf on $\mathbb{C}$ , and $\langle G, \alpha \colon \mathcal{A} \circ G \Rightarrow G \rangle$ be an $\mathcal{A}$ -algebra. If $\phi \colon \mathbb{C}({-}, C) \to G$ is a morphism between presheaves, then there exists a unique homomorphism

\begin{equation*} \phi^{\dagger} \colon \left\langle \mathcal{A} ({-}, C), \mu^{\mathcal{A}}_{{-}, C} \colon \mathcal{A} \circ \mathcal{A} ({-}, C) \Rightarrow \mathcal{A} ({-}, C) \right\rangle \to \left\langle G , \alpha \colon \mathcal{A} \circ G \Rightarrow G \right\rangle \end{equation*}

between $\mathcal{A}$ -algebras that makes the following diagram commute up to isomorphism:

(3.3)

(3.4)

We check that $\phi^{\dagger}$ makes the diagram (3.3) commute. In the following diagram, the bottom triangle commutes by (3.1).

To show that the above square commutes, it suffices to show the commutativity of the following diagram for each object A of $\mathbb{C}$ :

where [x, y] denotes the equivalence class of a pair (x, y), see the proof of Proposition A.3 in Appendix A. By chasing the diagram, it is enough to show $[\eta^{\mathcal{A}}_{A,A}(\mathrm{id}_A), \phi_A(f)] = [\eta^{\mathcal{A}}_{A,C}(f), \phi_C(\mathrm{id}_C)]$ in $\displaystyle \int^{B \in \mathbb{C}} \mathcal{A}(A, B) \times GB$ for each $A \in \mathbb{C}$ and $f \colon A \to C$ . Consider the following commutative diagram.

For $\langle \eta(\mathrm{id}_A) , \phi_C(\mathrm{id}_C) \rangle \in \mathcal{A}(A,A) \times GC$ , we have

\begin{align*} & \omega_A( (\mathcal{A}(A,A) \times G(f)) \langle \eta(\mathrm{id}_A) , \phi_C(\mathrm{id}_C) \rangle) \\ & = \omega_A(\langle \eta(\mathrm{id}_A) , (Gf)(\phi_C(\mathrm{id}_C)) \rangle) \\ & = \omega_A(\langle \eta(\mathrm{id}_A) , \phi_C(f) \rangle) & \text{(by the naturality of $\phi$)}\\ & = [\eta(\mathrm{id}_A) , \phi_C(f) ] \end{align*}

and

\begin{align*} & \omega_C( (\mathcal{A}(A,f) \times G(C)) \langle \eta(\mathrm{id}_A) , \phi_C(\mathrm{id}_C) \rangle) \\ & = \omega_C( \langle \mathcal{A}(A,f)(\eta(\mathrm{id}_A)) , \phi_C(\mathrm{id}_C) \rangle) \\ & = \omega_C( \langle \eta(f) , \phi_C(\mathrm{id}_C) \rangle) & \text{(by the naturality of $\eta_{A,{-}}$)} \\ & = [\eta(f) , \phi_C(\mathrm{id}_C)]. \end{align*}

Hence, we have $[\eta(\mathrm{id}_A), \phi(f)] = [\eta(f), \phi(\mathrm{id}_C)]$ .

Next, we show that $\phi^{\dagger}$ is a homomorphism $\mu^{\mathcal{A}}_{{-}, C} \to \alpha$ of $\mathcal{A}$ -algebras. It suffices to show the commutativity of the left and right square in the following diagram. The right square commutes because $\alpha$ is an $\mathcal{A}$ -algebra (3.2), and the left square commutes by the naturality of $\mu$ and $\phi$ and some calculation similar to the above argument.

By the Yoneda lemma, giving a morphism $\phi \colon \mathbb{C}({-}, C) \to G$ between presheaves is equivalent to giving an element $p \in GC$ . In the proof of Theorem 3.3, $\phi^{\dagger}$ is defined by (3.4). Hence, for $a \in \mathcal{A}(A, C)$ , $\phi^{\dagger}(a)$ is calculated to be $\alpha([a, p])$ . In summary, we obtain the following corollary.

Corollary 3.4. Let $\mathcal{A}$ be a promonad on $\mathbb{C}$ , $C \in \mathbb{C}$ , G be a presheaf on $\mathbb{C}$ , and $\langle G, \alpha \rangle$ be an $\mathcal{A}$ -algebra. For an element $p \in GC$ , there is a homomorphism

\begin{equation*} h \colon \left\langle \mathcal{A} ({-}, C), \mu^{\mathcal{A}}_{{-}, C} \colon \mathcal{A} \circ \mathcal{A} ({-}, C) \Rightarrow \mathcal{A}({-}, C) \right\rangle \to \left\langle G, \alpha \colon \mathcal{A} \circ G \Rightarrow G \right\rangle \end{equation*}

satisfying $h_{A}(a) = \alpha([a, p])$ for any $A \in \mathbb{C}$ and $a \in \mathcal{A}(A , C)$ , and $h(\eta^{\mathcal{A}}_{A,C}(f)) = (Gf)(p)$ for any $A \in \mathbb{C}$ and $f \colon A \to C$ in $\mathbb{C}$ .

When G in Corollary 3.4 is a presheaf $\mathcal{A}'({-}, D)$ for another promonad and an object $D \in \mathbb{C}$ , we obtain the following corollary.

Corollary 3.5. Let $\mathcal{A}$ and $\mathcal{A}'$ be promonads on $\mathbb{C}$ , $D \in \mathbb{C}$ , and $\alpha$ be a family $(\alpha_{A, B} \colon \mathcal{A}(A, B) \times \mathcal{A}'(B, D) \to \mathcal{A}'(A, D))_{A, B \in \mathbb{C}}$ of maps which is natural in A and extranatural in B and satisfies (3.1) and (3.2) for $G = \mathcal{A}'({-}, D)$ . For an element $p \in \mathcal{A}'(C,D)$ , there is a homomorphism

\begin{equation*} h \colon \left\langle \mathcal{A}({-}, C), \mu^{\mathcal{A}} \right\rangle \to \left\langle \mathcal{A}'({-}, D), \alpha \right\rangle \end{equation*}

such that $h(a) = \alpha_{A,C}(a, p)$ for any $A \in \mathbb{C}$ and $a \in \mathcal{A}(A,C)$ , and $h_A(\eta^{\mathcal{A}}_{A,C}(f)) = \mathcal{A}'(f, D)(p)$ for any $A \in \mathbb{C}$ and $f \colon A \to C$ in $\mathbb{C}$ .

We use Corollary 3.5 to interpret handlers for arrows.

Remark 3.6. Note that we can prove Theorem 3.3 in another way. From the promonad , we can obtain a cocontinuous monad $\widetilde{\mathcal{A}} \colon [\mathbb{C}^{\mathrm{op}},\mathbf{Set}] \to [\mathbb{C}^{\mathrm{op}}, \mathbf{Set}]$ by the following construction. Then, using the universality of free $\widetilde{\mathcal{A}}$ -algebra, Theorem 3.3 is proved.

4.1 Syntax and typing rules

Let $\mathord{BType}$ be a set of base types, and $\Sigma$ be a set of operations. We assume that two base types $\gamma$ (coarity) and $\delta$ (arity) are assigned for each operation $\mathsf{op} \in \Sigma$ . We write when the coarity and arity of $\mathsf{op}$ are $\gamma$ and $\delta$ , respectively. The syntax is shown in Figure 2. The difference from the original arrow calculus (Lindley et al., Reference Lindley, Wadler and Yallop2010, Reference Lindley, Wadler and Yallop2011) is the addition of $\mathsf{op}(M)$ , $\mathop{\mathbf{handle}} R \mathop{\mathbf{with}} H$ to the commands and handlers H.

Fig. 2. The syntax of the arrow calculus with operations and handlers.

We call a type A primitive (written $\Phi(A)$ ) if A is constructed only by $\beta$ , $\times$ and $\to$ . Formally, $\Phi(A)$ is defined as follows.

The typing rules for the arrow calculus are shown in Figure 3. The notion of primitive types is used in the rule .

Fig. 3. Typing rules for the arrow calculus with operations and handlers.

A type $A \rightsquigarrow B$ is that of an effectful computation such that the type of its inputs is A and the type of its outputs is B.

As we described in Section 1.2.3, a term M is a pure function and a command P is an effectful computation. The command $\lfloor{M}\rfloor$ is a pure computation, which corresponds to $\mathtt{arr}$ in Haskell. The command $L \bullet M$ is a command that invokes an arrow L with an input M. It corresponds to $(\mathrel{>\!\!>\!\!>})$ and $\mathtt{arr}$ in Haskell. The command $\mathop{\mathbf{let}} x \Leftarrow P \mathop{\mathbf{in}} Q$ is a sequential composition of commands P and Q, which corresponds to $(\mathrel{>\!\!>\!\!>})$ and $\mathtt{first}$ in Haskell. The command $\mathsf{op}(M)$ is an operation invocation with an input M.

A judgement $\Gamma \vdash M : A$ for a term means that the term M is a pure function from $\Gamma$ to A. A judgement for a command means that the command P is a computation such that the type of its inputs is $\Delta$ and the type of its outputs is A under the context $\Gamma$ .

In the construction of handlers:

(4.1)

the command P corresponds to the $p \in \mathcal{A}'(C,D)$ in Corollary 3.5, and the family $\{ Q_{\mathsf{op}} \}_{\mathsf{op} \in \Sigma}$ of commands determines an algebraic structure $\alpha$ in Corollary 3.5.

Handlers for arrows are very similar to handlers for ordinary monads. The difference is that, in the handler (4.1), $x : C$ and $z : \gamma$ are not ordinary contexts, but inputs of the effectful computation P and $Q_{\mathsf{op}}$ , respectively.

4.2 Operational semantics

We present the reduction rules for closed terms $\diamond \vdash M : A$ and closed commands . We define two kinds of evaluation contexts as follows.

\begin{align*} \mathcal{E} & ::= [{-}] \mid \mathcal{E} N \mid V \mathcal{E} \mid \mathcal{E} \bullet N \mid (\lambda^{\bullet} x . P) \bullet \mathcal{E} \mid \lfloor{\mathcal{E}}\rfloor \mid \mathsf{op}(\mathcal{E}) \mid \mathop{\mathbf{fst}} \mathcal{E} \mid \mathop{\mathbf{snd}} \mathcal{E} \mid \langle {\mathcal{E}}, {M} \rangle \mid \langle {V}, {\mathcal{E}} \rangle \\ \mathcal{F} & ::= [{-}] \mid \mathop{\mathbf{let}} x \Leftarrow \mathcal{F} \mathop{\mathbf{in}} Q\end{align*}

We put a term in the hole of a context $\mathcal{E}[{-}]$ and a command in the hole of a context $\mathcal{F}[{-}]$ . The reduction relation is shown in Figure 4.

Fig. 4. Operational semantics.

Type preservation (Proposition 4.3) and progress (Proposition 4.1) hold for the arrow calculus with operations and handlers.

1. 1. If $\Gamma, x : A \vdash M : B$ and $\Gamma \vdash N : A$ are derivable, then $\Gamma \vdash M[N / x] : B$ is derivable.

2. 2. If and $\Gamma \vdash N : A$ are derivable, then is derivable.

3. 3. If and $\Gamma, \Delta \vdash N : A$ are derivable, then is derivable.

4.3 Example

In the description of handlers, clauses that just forward their input shall be omitted. For example, let $\Sigma = \{ \mathsf{op}_1, \mathsf{op}_2 \}$ , we write

for .

4.3.1 Logic circuit simulation

We explain the details of the example of logic circuit simulation in Section 1.2.3. Let $\mathord{BType} = \{ \mathrm{Bool} \}$ . The base type Bool is a type for boolean values. We add the following constants to the arrow calculus.

\begin{gather*} \mathtt{true} : \mathrm{Bool}, \quad \mathtt{false} : \mathrm{Bool}.\end{gather*}

Let ${\Sigma_{\mathrm{LC}}}$ be the signature of logic circuits defined in Section 1.2. We extend the arrow calculus by adding $\mathop{\mathbf{if}} M \mathop{\mathbf{then}} N_1 \mathop{\mathbf{else}} N_2$ to terms with the following typing rule:

The operational semantics is extended by adding the following evaluation context and reduction relations.

\begin{equation*} \mathcal{E} ::= \cdots \mid \mathop{\mathbf{if}} \mathcal{E} \mathop{\mathbf{then}} N_1 \mathop{\mathbf{else}} N_2,\end{equation*}

\begin{align*} \mathop{\mathbf{if}} \mathtt{true} \mathop{\mathbf{then}} N_1 \mathop{\mathbf{else}} N_2 & \to N_1, \\ \mathop{\mathbf{if}} \mathtt{false} \mathop{\mathbf{then}} N_1 \mathop{\mathbf{else}} N_2 & \to N_2.\end{align*}

Let $Q_{\mathsf{NAND}}$ be $\mathop{\mathbf{let}} u \Leftarrow \mathsf{AND}(z) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(u) \mathop{\mathbf{in}} k \bullet v$ and $Q_{\mathsf{OR}}$ be $\mathop{\mathbf{let}} u \Leftarrow \mathsf{NOT}(\mathop{\mathbf{fst}} z) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(\mathop{\mathbf{snd}} z) \mathop{\mathbf{in}} \mathop{\mathbf{let}} w \Leftarrow \mathsf{AND}(\langle {u}, {v} \rangle) \mathop{\mathbf{in}} k \bullet w$ . The handler and $H'_2$ defined in Section 1.2.3 is well-typed: $\vdash H'_1 : \mathrm{Bool} \Rightarrow \mathrm{Bool}$ and $\vdash H'_2 : \mathrm{Bool} \Rightarrow \mathrm{Bool}$ .

We check the derivation of $\vdash H'_1 : \mathrm{Bool} \Rightarrow \mathrm{Bool}$ . Let $\Gamma = k : \mathrm{Bool} \rightsquigarrow \mathrm{Bool}$ , $\Delta = z : \mathrm{Bool} \times \mathrm{Bool}$ and $\Delta' = (\Delta, u : \mathrm{Bool})$ . The derivation of is as follows.

Similarly, we can derive . Hence, the derivation of $\vdash H'_1 : \mathrm{Bool} \Rightarrow \mathrm{Bool}$ is as follows:

where $Q_{\mathsf{AND}} = \mathop{\mathbf{let}} u \Leftarrow \mathsf{AND}(z) \mathop{\mathbf{in}} k \bullet u$ and $Q_{\mathsf{NOT}} = \mathop{\mathbf{let}} u \Leftarrow \mathsf{NOT}(z) \mathop{\mathbf{in}} k \bullet u$ .

The evaluation of $\mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} \mathsf{NAND}(\langle {\mathtt{true}}, {\mathtt{false}} \rangle) \mathop{\mathbf{with}} H'_1) \mathop{\mathbf{with}} H'_2$ is shown in Figure 5.

Fig. 5. The evaluation of $\mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} \mathsf{NAND}(\langle {\mathtt{true}}, {\mathtt{false}} \rangle) \mathop{\mathbf{with}} H'_1) \mathop{\mathbf{with}} H'_2$ .

4.3.2 Read only state

Let $\mathord{BType} = \{ \mathrm{Unit}, \mathrm{Bool} \}$ and . The operation $\mathsf{get}$ is expected to read a state of type Bool and return the stored value. We can implement $\mathsf{get}$ using a handler.

The following judgements are derivable:

Hence, we can construct a handler and derive $\vdash H : \mathrm{Bool} \Rightarrow \mathrm{Bool}$ . This handler H implements $\mathsf{get}$ so that the stored value is $\mathtt{true}$ . For example, the reduction of a program $\mathop{\mathbf{handle}} \mathsf{get}(\mathtt{\langle\rangle}) \mathop{\mathbf{with}} H$ is as follows.

\begin{align*} \mathop{\mathbf{handle}} \mathsf{get}(\mathtt{\langle\rangle}) \mathop{\mathbf{with}} H & \to (\lambda^{\bullet} y . \mathop{\mathbf{handle}} \lfloor{y}\rfloor \mathop{\mathbf{with}} H) \bullet \mathtt{true} \\ & \to (\mathop{\mathbf{handle}} \lfloor{y}\rfloor \mathop{\mathbf{with}} H)[\mathtt{true} / y] \\ & = \mathop{\mathbf{handle}} \lfloor{\mathtt{true}}\rfloor \mathop{\mathbf{with}} H \\ & \to \lfloor{x}\rfloor[\mathtt{true} / x] \\ & = \lfloor{\mathtt{true}}\rfloor\end{align*}

5.1 Models of arrow calculus

We define models of the arrow calculus, in which the arrow calculus with operations is interpreted.

• • A cartesian closed category (ccc) $\mathbb{C}$ .

• • A cocomplete cartesian closed category $\mathbb{C}'$ .

• • A cartesian fully faithful functor $J \colon \mathbb{C} \to \mathbb{C}'$ .

• • A $\mathbb{C}$ -small strong promonad on $\mathbb{C}$ in $\mathbb{C}'$ - $\mathbf{Prof}$ (Definitions 2.3 and 2.7).

For a ccc $\mathbb{C}$ , a cocomplete ccc $\mathbb{C}'$ and a cartesian fully faithful functor $J \colon \mathbb{C} \to \mathbb{C}'$ , the identity $\mathbb{C}'$ -profunctor on $\mathbb{C}$ defined by $\mathrm{I}_{\mathbb{C}}(A, B) = (JA \Rightarrow JB) = J(A \Rightarrow B)$ is a $\mathbb{C}$ -small strong promonad on $\mathbb{C}$ in $\mathbb{C}'$ - $\mathbf{Prof}$ . We have $\mathrm{I}_{\mathbb{C}}^{\circ}(A, B) = (A \Rightarrow B)$ and $J \circ \mathrm{I}_{\mathbb{C}}^{\circ} = \mathrm{I}_{\mathbb{C}}$ :

Definition 5.2 (interpretation.) Given a model of arrow calculus $(\mathbb{C}, \mathbb{C}', J, \mathcal{A})$ , interpretation $\mathord{\left[\![{\beta}\right]\!]} \in \mathbb{C}$ of each base type $\beta \in \mathord{BType}$ and interpretation $\mathord{\left[\![{\mathrm{op}}\right]\!]} \colon \mathcal{A}(\mathord{\left[\![{\delta}\right]\!]}, {-}) \Rightarrow \mathcal{A}(\mathord{\left[\![{\gamma}\right]\!]}, {-})$ of each operation , we define interpretation of the arrow calculus with operations (without handlers). The interpretation $\mathord{\left[\![{A}\right]\!]}$ of a type A is defined as a natural extension of $\mathord{\left[\![{\beta}\right]\!]}$ with $\mathord{\left[\![{A \rightsquigarrow B}\right]\!]} = \mathcal{A}^{\circ}(\mathord{\left[\![{A}\right]\!]}, \mathord{\left[\![{B}\right]\!]})$ . For a term $\Gamma \vdash M : A$ and a command , their interpretation $\mathord{\left[\![{M}\right]\!]} \colon \mathord{\left[\![{\Gamma}\right]\!]} \to \mathord{\left[\![{A}\right]\!]}$ in $\mathbb{C}$ and $\mathord{\left[\![{P}\right]\!]} \colon \mathord{\left[\![{\Gamma}\right]\!]} \to \mathcal{A}^{\circ}(\mathord{\left[\![{\Delta}\right]\!]}, \mathord{\left[\![{A}\right]\!]})$ in $\mathbb{C}$ are defined as in Figure 6.

Fig. 6. The categorical semantics.

We discuss interpretation of handlers in Section 5.3.

5.2 Construction of a model of the arrow calculus

We give a semantics of the arrow calculus with operations and handlers using a $\mathbf{Set}$ -small strong $\mathbf{Ens}$ -promonad $\mathcal{A}$ on $\mathbf{Set}$ . We fix an interpretation of the base types $\mathord{\left[\![{{-}}\right]\!]} \colon \mathord{BType} \to \mathbf{Set}$ . Here $\mathord{BType}$ is regarded as a discrete category.

First, we construct a map $\mathrm{Arr}_{\Sigma} \colon \mathrm{Ob}(\mathbf{Set}^{\mathrm{op}}) \times \mathrm{Ob}(\mathbf{Set}) \to \mathrm{Ob}(\mathbf{Ens})$ .

Definition 5.3 (arrow term). For sets A and B, $\mathrm{Arr}_{\Sigma}(A, B)$ is defined to be the smallest class satisfying the rules in Figure 7. We call an element in $\mathrm{Arr}_{\Sigma}(A, B)$ an arrow term. An equation is a pair of arrow terms (t, t’) where $t, t' \in \mathrm{Arr}_{\Sigma}(A, B)$ for some sets A and B. A theory is a pair $(\Sigma, E)$ of a signature $\Sigma$ and a set E of equations.

Fig. 7. Construction of $\mathrm{Arr}_{\Sigma}(A, B) \in \mathbf{Ens}$ for $A, B \in \mathbf{Set}$ .

In the following, we consider only the case $E = \emptyset$ .

Unfortunately, $\mathrm{Arr}_{\Sigma}(A, B)$ is a proper class because it contains $a \mathrel{>\!\!>\!\!>} b$ for any $X \in \mathbf{Set}$ , $a \in \mathrm{Arr}_{\Sigma}(A, X)$ and $b \in \mathrm{Arr}_{\Sigma}(X, B)$ . However, we can define an equivalence relation $\sim$ on $\mathrm{Arr}_{\Sigma}(A, B)$ and obtain $\mathbf{Set}$ -small strong $\mathbf{Ens}$ -promonad .

The equivalence relation $\sim$ is defined as the smallest congruence relation satisfying the following axioms (5.1)–(5.9), which correspond to the arrow laws (1.1)–(1.9).

(5.1) \begin{align} (a \mathrel{>\!\!>\!\!>} b) \mathrel{>\!\!>\!\!>} c & \sim a \mathrel{>\!\!>\!\!>} (b \mathrel{>\!\!>\!\!>} c)\end{align}

(5.2) \begin{align}\mathop{\mathrm{arr}}\nolimits(g \circ f) & \sim \mathop{\mathrm{arr}}\nolimits(f) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(g)\end{align}

(5.3) \begin{align}\mathop{\mathrm{arr}}\nolimits(\mathrm{id}) \mathrel{>\!\!>\!\!>} a & \sim a\end{align}

(5.4) \begin{align}a \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\mathrm{id}) & \sim a\end{align}

(5.5) \begin{align}\mathop{\mathrm{first}}\nolimits(a) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\mathrm{id} \times f) & \sim \mathop{\mathrm{arr}}\nolimits(\mathrm{id} \times f) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits(a)\end{align}

(5.6) \begin{align}\mathop{\mathrm{first}}\nolimits(a) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\pi_1) & \sim \mathop{\mathrm{arr}}\nolimits(\pi_1) \mathrel{>\!\!>\!\!>} a\end{align}

(5.7) \begin{align}\mathop{\mathrm{first}}\nolimits(a) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\alpha) & \sim \mathop{\mathrm{arr}}\nolimits(\alpha) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits(\mathop{\mathrm{first}}\nolimits(a))\end{align}

(5.8) \begin{align}\mathop{\mathrm{first}}\nolimits (\mathop{\mathrm{arr}}\nolimits(f)) & \sim \mathop{\mathrm{arr}}\nolimits(f \times \mathrm{id})\end{align}

(5.9) \begin{align}\mathop{\mathrm{first}}\nolimits (a \mathrel{>\!\!>\!\!>} b) & \sim \mathop{\mathrm{first}}\nolimits(a) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits(b)\end{align}

We denote $\mathrm{Arr}_{\Sigma}(A, B) / {\sim}$ as $\mathcal{A}_{\Sigma}(A, B)$ . We define $\mathop{\mathrm{second}}\nolimits_X(a) = \mathop{\mathrm{arr}}\nolimits(\mathop{sym}_{X, A}) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits_X(a) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\mathop{sym}_{X, B})$ for $a \in \mathrm{Arr}_{\Sigma}(A, B)$ , where the map $\mathop{sym}_{Y, Z} \colon Y \times Z \to Z \times Y$ is defined by $\mathop{sym}_{Y,Z}(y,z) = (z, y)$ .

We use string diagram like notation introduced by Asada and Hasuo (Reference Asada and Hasuo2010). Arrow terms are depicted as follows.

Especially, we write

The $\mathbf{Set}$ -smallness of $\mathrm{Arr}({-}_1, {-}_2) / \sim$ is proven from Proposition 5.5. It says that every arrow term is equivalent to the normal form. The normal form was introduced by Yallop (Reference Yallop2010) for arrows in Haskell to compare two programs. The normal form here is essentially the same as his except that it is defined for arrow terms $a \in \mathrm{Arr}_{\Sigma}(A, B)$ . The size of the collection of all normal forms is small.

Definition 5.4 (normal form.) Let n be a natural number, be a sequence of operations, $(f_i \colon \mathord{\left[\![{\delta_{i-1}}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_{1}}\right]\!]} \times A \to \mathord{\left[\![{\gamma_i}\right]\!]})_{i = 1}^n$ be a sequence of maps and $g \colon \mathord{\left[\![{\delta_n}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_1}\right]\!]} \times A \to B$ . We define an arrow term $\mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i = 1}^{n}}, {(f_i)_{i = 1}^n}; {g}\right)$ inductively as follows:

\begin{align*} \mathop{\mathsf{nf}}\left({()}, {()}; {g}\right) = & \mathop{\mathrm{arr}}\nolimits(g) & (n = 0) \\[0.5em] \mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i = 1}^{n}}, {(f_i)_{i = 1}^{n}}; {g}\right) = & \mathop{\mathrm{arr}}\nolimits(d_A) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits_A( \mathop{\mathrm{arr}}\nolimits(f_1) \mathrel{>\!\!>\!\!>} \mathsf{op}_1 ) \\ & \mathrel{>\!\!>\!\!>} \mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i = 2}^n}, {(f_i)_{i = 2}^n}; {g}\right) & (n > 0) \end{align*}

where $d_X \colon X \to X \times X$ is the diagonal map: $d_X(x) = (x, x)$ . We call $\mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i=1}^n}, {(f_i)_{i=1}^n}; {g}\right)$ a normal form.

Proposition 5.5. Let A and B be sets. For any $a \in \mathrm{Arr}_{\Sigma}(A, B)$ , there exist a natural number $n \in \mathbb{N}$ , a sequence of operations , a sequence of maps $(f_i \colon \mathord{\left[\![{\delta_{i-1}}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_{1}}\right]\!]} \times A \to \mathord{\left[\![{\gamma_i}\right]\!]})_{i = 1 , \dots, n}$ and $g \colon \mathord{\left[\![{\delta_n}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_1}\right]\!]} \times A \to B$ such that

\begin{equation*} a \sim \mathop{\mathsf{nf}}\left({(\mathsf{op})_{i=1}^n}, {(f_i)_{i=1}^n}; {g}\right). \end{equation*}

Proof sketch We prove by induction on the structure of $a \in \mathrm{Arr}_{\Sigma}(A, B)$ . Since the proof is very long, we only prove the following two cases here and the rest of the proof is sent to the appendix.

In case $a = \mathop{\mathrm{arr}}\nolimits(f)$ for some $f \colon A \to B$ . The proposition trivially holds for $n = 0$ .

In case $a = \mathsf{op}$ for some with $\mathord{\left[\![{\gamma}\right]\!]} = A$ and $\mathord{\left[\![{\delta}\right]\!]} = B$ . We have

\begin{align*} a & = \mathsf{op} \\ & \sim \mathop{\mathrm{arr}}\nolimits(\mathrm{id}) \mathrel{>\!\!>\!\!>} \mathsf{op} \\ & \sim \mathop{\mathrm{arr}}\nolimits(\pi_1 \circ d_{A}) \mathrel{>\!\!>\!\!>} \mathsf{op} \\ & \sim \mathop{\mathrm{arr}}\nolimits(d_A) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\pi_1) \mathrel{>\!\!>\!\!>} \mathsf{op} \\ & \sim \mathop{\mathrm{arr}}\nolimits(d_A) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits(\mathsf{op}) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\pi_1) \\ & \sim \mathop{\mathrm{arr}}\nolimits(d_{A}) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits_A(\mathop{\mathrm{arr}}\nolimits(\mathrm{id}_{\mathord{\left[\![{\gamma}\right]\!]}}) \mathrel{>\!\!>\!\!>} \mathsf{op}) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(\pi_1). \end{align*}

See Figure 8.

Fig. 8. In case $a = \mathsf{op}$ .

The collection $\mathcal{A}^{\circ}_{\Sigma}(A, B)$ of all normal forms in $\mathrm{Arr}_{\Sigma}(A, B)$ is a set, not a proper class, because

We identify an equivalence class [a] for an arrow term $a \in \mathrm{Arr}_{\Sigma}(A,B)$ with its normal form.

The map $\mathcal{A}_{\Sigma} \colon \mathrm{Ob}(\mathbf{Set}^{\mathrm{op}}) \times \mathrm{Ob}(\mathbf{Set}) \to \mathrm{Ob}(\mathbf{Ens})$ is extended to an $\mathbf{Ens}$ -profunctor by defining $\mathcal{A}_{\Sigma}(f,g)([a]) = [\mathop{\mathrm{arr}}\nolimits(f) \mathrel{>\!\!>\!\!>} a \mathrel{>\!\!>\!\!>} \mathop{\mathrm{arr}}\nolimits(g)]$ for $f \colon A' \to A$ , $g \colon B \to B'$ and $a \in \mathrm{Arr}_{\Sigma}(A, B)$ . We have constructed a model of the arrow calculus.

Note that the model $(\mathbf{Set}, \mathbf{Ens}, J, \mathcal{A}_{\Sigma})$ is the free model in the sense that if $(\mathbf{Set}, \mathbf{Ens}, J, \mathcal{A})$ is also a model and a family of interpretation of operations is specified, then there is a unique 2-cell $h \colon \mathcal{A}_{\Sigma} \Rightarrow \mathcal{A}$ which is compatible with units and multiplications of $\mathcal{A}_{\Sigma}$ and $\mathcal{A}$ .

5.3 Interpretation of handlers

We interpret handlers in the model $(\mathbf{Set}, \mathbf{Ens}, J, \mathcal{A}_{\Sigma})$ of the arrow calculus. We fix an interpretation of base types $\mathord{\left[\![{{-}}\right]\!]} \colon \mathord{BType} \to \mathrm{Ob}(\mathbf{Set})$ .

5.3.1 The problem of strength

Unlike in the case of the strong monad $\mathcal{T} \colon \mathbf{Set} \to \mathbf{Set}$ in $\mathbf{Cat}$ , in the case of the strong promonad in $\mathbf{Ens}$ - $\mathbf{Prof}$ , the treatment of the strength is non-trivial. To interpret a handler as a $\mathcal{A}_{\Sigma}^{\circ}$ -homomorphism, we have to construct a family of maps

(5.10) \begin{equation} \left( \alpha_{A, B} \colon \mathcal{A}_{\Sigma}^{\circ}(A , B) \times \mathcal{A}_{\Sigma}^{\circ}(B, \mathord{\left[\![{D}\right]\!]}) \to \mathcal{A}_{\Sigma}^{\circ}(A, \mathord{\left[\![{D}\right]\!]}) \right)_{A, B}\end{equation}

from a handler :

The problem is that we cannot define the maps (5.10) since there is no way to define $\alpha(\mathop{\mathrm{first}}\nolimits_S(\mathsf{op}), b)$ for and $b \in \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]})$ :

(5.11) \begin{equation} \begin{split} \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{\delta}\right]\!]} \times S) \times \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}) & \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}) \\ (\mathop{\mathrm{first}}\nolimits_S(\mathsf{op}), b) & \mapsto \alpha(\mathop{\mathrm{first}}\nolimits_S(\mathsf{op}), b). \end{split}\end{equation}

To define the above map, we need maps $\mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}) \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]})$ as an interpretation of $Q_{\mathsf{op}}$ . However, in the naïve interpretation (Definition 5.2), the command $Q_{\mathsf{op}}$ is interpreted as a map $\mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]} \colon \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]}, \mathord{\left[\![{D}\right]\!]}) \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]}, \mathord{\left[\![{D}\right]\!]})$ .

5.3.2 Interpretation with a parameter

We solve this problem by using an additional parameter $S \in \mathrm{Ob}(\mathbf{Set})$ in the interpretation of terms. This additional parameter enables us to define maps $\mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}) \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]})$ as an interpretation of $Q_{\mathsf{op}}$ . For a type A and a set S, we define the interpretation $\mathord{\left[\![{A}\right]\!]}^S$ as an extension of $\mathord{\left[\![{\beta}\right]\!]}$ for $\beta \in \mathord{BType}$ .

\begin{align*} \mathord{\left[\![{\beta}\right]\!]}^S & = \mathord{\left[\![{\beta}\right]\!]} \\ \mathord{\left[\![{A \times B}\right]\!]}^S & = \mathord{\left[\![{A}\right]\!]}^S \times \mathord{\left[\![{B}\right]\!]}^S \\ \mathord{\left[\![{A \to B}\right]\!]}^S & = \mathord{\left[\![{A}\right]\!]}^S \Rightarrow \mathord{\left[\![{B}\right]\!]}^S \\ \mathord{\left[\![{A \rightsquigarrow B}\right]\!]}^S & = \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{A}\right]\!]}^S \times S, \mathord{\left[\![{B}\right]\!]}^S)\end{align*}

The interpretation $\mathord{\left[\![{\Gamma}\right]\!]}^S$ of a context $\Gamma$ is defined as an extension of the interpretation of types:

\begin{equation*} \mathord{\left[\![{\diamond}\right]\!]}^S = 1, \qquad \mathord{\left[\![{\Gamma, x : A}\right]\!]}^S = \mathord{\left[\![{\Gamma}\right]\!]}^S \times \mathord{\left[\![{A}\right]\!]}^S.\end{equation*}

The key is the interpretation $\mathord{\left[\![{A \rightsquigarrow B}\right]\!]}^S$ of a type $A \rightsquigarrow B$ . Adding S to the “input argument” of the arrow allows us to deal with strength.

If a type A is primitive, its interpretation is independent of S, that is we can show the following lemma by the definitions.

Lemma 5.7. If a type A is primitive ( $\Phi(A)$ ), then $\mathord{\left[\![{A}\right]\!]}^S = \mathord{\left[\![{A}\right]\!]}^1$ for any S.

Next, we define interpretation of terms and commands. For judgements $\Gamma \vdash M : A$ and , we want to define:

Let $e \in \mathord{\left[\![{\Gamma}\right]\!]}^S$ . The interpretation of terms is defined as follows. In the following, definitions are described by elements of sets, rather than by morphisms as in Figure 6. This is to avoid making the definition of interpretation of handlers more complex than necessary.

\begin{align*} \mathord{\left[\![{\Gamma, y : A \vdash y : A}\right]\!]}^S(e, a) & = a & a \in \mathord{\left[\![{A}\right]\!]}^S \\ \mathord{\left[\![{\Gamma \vdash \langle {M_1}, {M_2} \rangle : A_1 \times A_2}\right]\!]}^S(e) & = (\mathord{\left[\![{M_1}\right]\!]}^S(e) , \mathord{\left[\![{M_2}\right]\!]}^S(e)) \\ \mathord{\left[\![{\Gamma \vdash \mathop{\mathbf{fst}}{M} : A}\right]\!]}^S(e) & = \pi_1 (\mathord{\left[\![{M}\right]\!]}^S(e)) \\ \mathord{\left[\![{\Gamma \vdash \mathop{\mathbf{snd}}{M} : A}\right]\!]}^S(e) & = \pi_2 (\mathord{\left[\![{M}\right]\!]}^S(e)) \\ \mathord{\left[\![{\Gamma \vdash MN : B}\right]\!]}^S(e) & = \mathord{\left[\![{M}\right]\!]}^S(e)\left(\mathord{\left[\![{N}\right]\!]}^S(e)\right) \\ \mathord{\left[\![{\Gamma \vdash \lambda y : A . M : A \to B}\right]\!]}^S(e) & = \mathord{\left[\![{M}\right]\!]}^S(e, {-}) \\ \mathord{\left[\![{\Gamma \vdash \lambda^{\bullet} y : A . P : A \rightsquigarrow B}\right]\!]}^S(e) & = \mathord{\left[\![{P}\right]\!]}^S(e)\end{align*}

The interpretation of commands is defined as follows.

The interpretation of $\mathord{\left[\![{\mathop{\mathbf{let}} y \Leftarrow P \mathop{\mathbf{in}} Q}\right]\!]}^S(e)$ is illustrated as follows.

To interpret handling , we construct an algebra from . Note that the derivation is

By Lemma 5.7, we have $\mathord{\left[\![{C}\right]\!]}^S = \mathord{\left[\![{C}\right]\!]}^1$ and $\mathord{\left[\![{D}\right]\!]}^S = \mathord{\left[\![{D}\right]\!]}^1$ . We have maps:

The maps $\mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]}^S$ induce an $\mathcal{A}_{\Sigma}$ -algebra $\alpha$ on the presheaf $\mathcal{A}_{\Sigma}({-}, \mathord{\left[\![{D}\right]\!]})$ as follows.

\begin{align*} \alpha : \mathcal{A}_{\Sigma}^{\circ}(A, B) \times \mathcal{A}_{\Sigma}^{\circ}(B, \mathord{\left[\![{D}\right]\!]}^1) & \to \mathcal{A}_{\Sigma}^{\circ}(A, \mathord{\left[\![{D}\right]\!]}^1) \\ (\mathop{\mathrm{arr}}\nolimits(f) , a) & \mapsto \mathop{\mathrm{arr}}\nolimits(f) \mathrel{>\!\!>\!\!>} a \\[0.5em] \alpha : \mathcal{A}_{\Sigma}^{\circ}(A, B) \times \mathcal{A}_{\Sigma}^{\circ}(B, \mathord{\left[\![{D}\right]\!]}^1) & \to \mathcal{A}_{\Sigma}^{\circ}(A, \mathord{\left[\![{D}\right]\!]}^1) \\ (b_1 \mathrel{>\!\!>\!\!>} b_2 , a) & \mapsto \alpha(b_1 , \alpha(b_2, a)) \\[0.5em] \alpha : \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]}, \mathord{\left[\![{\delta}\right]\!]}) \times \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]}, \mathord{\left[\![{D}\right]\!]}^1) & \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]}, \mathord{\left[\![{D}\right]\!]}^1) \\ (\mathsf{op} , a) & \mapsto \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]}^1(a) \\[0.5em] \alpha : \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{\delta}\right]\!]} \times S) \times \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}^1) & \to \mathcal{A}_{\Sigma}^{\circ}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathord{\left[\![{D}\right]\!]}^1) \\ (\mathop{\mathrm{first}}\nolimits_S(\mathsf{op}) , a) & \mapsto \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]}^S(a) \\[0.5em]\end{align*}

Note that, since every arrow term is equivalent to a normal form (Proposition 5.5), $\alpha(b, a)$ is well defined.

We also have $\mathord{\left[\![{P}\right]\!]}^1 \in \mathcal{A}_{\Sigma}(\mathord{\left[\![{C}\right]\!]}^1 , \mathord{\left[\![{D}\right]\!]}^1)$ . Hence, by Corollary 3.5, there exists a homomorphism $h \colon \mu \to \alpha$ such that the following diagram commutes:

We use the homomorphism h to interpret $\mathop{\mathbf{handle}} R \mathop{\mathbf{with}} H$ :

and write $\mathord{\left[\![{H}\right]\!]}$ for the homomorphism h.

The denotational semantics $\mathord{\left[\![{{-}}\right]\!]}^S$ defined here is compatible with the categorical semantics $\mathord{\left[\![{{-}}\right]\!]}$ (Definition 5.2) in the model $(\mathbf{Set}, \mathbf{Ens}, J, \mathcal{A}_{\Sigma})$ in the following sense.

Proposition 5.8. Let $\Gamma$ and $\Delta$ be primitive contexts and A be a primitive type. Let M be a term and P be a command of the arrow calculus with operations (without handlers). The following hold.

1. 1. If $\Gamma \vdash M : A$ then $\mathord{\left[\![{M}\right]\!]}^S = \mathord{\left[\![{M}\right]\!]}$ for any S.

2. 2. If then $(\mathop{\mathrm{arr}}\nolimits(j_s) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}^S(e)) = \mathord{\left[\![{P}\right]\!]}(e)$ for any S, $s \in S$ and $e \in \mathord{\left[\![{\Gamma}\right]\!]}$ where $j_s(z) = (z , s)$ for $z \in \mathord{\left[\![{\Delta}\right]\!]}$ .

Proposition 5.9. Let $\Gamma$ and $\Delta$ be contexts and A be a type. Let M be a term and P be a command of the arrow calculus with operations (without handlers). The following hold.

1. 1. If $\Gamma \vdash M : A$ then $\mathord{\left[\![{M}\right]\!]}^1 = \mathord{\left[\![{M}\right]\!]}$ .

2. 2. If then $\mathord{\left[\![{P}\right]\!]}^1 = \mathord{\left[\![{P}\right]\!]}$ .

Hence, we write $\mathord{\left[\![{A}\right]\!]}^1$ and $\mathord{\left[\![{\Gamma}\right]\!]}^1$ simply as $\mathord{\left[\![{A}\right]\!]}$ and $\mathord{\left[\![{\Gamma}\right]\!]}$ , respectively.

Remark 5.10. Let $\mathbb{C}$ be a cartesian closed category, $\mathbb{C}'$ be a cocomplete cartesian closed category and $J \colon \mathbb{C} \to \mathbb{C}'$ be a strong cartesian fully faithful functor. For an ordinary strong monad $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ , we do not have the problem on the strength. The reason is as follows. Let be a strong promonad ${\mathcal{T}}_{*}$ (Proposition 2.4) in defined by

\begin{equation*} \mathcal{A}(A, B) = \mathbb{C}(A, \mathcal{T} B) = (JA \Rightarrow J\mathcal{T} B) \in \mathbb{C}' \end{equation*}

for a strong monad $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ . This promonad $\mathcal{A}$ is $\mathbb{C}$ -small. Judgements are interpreted as morphisms

\begin{equation*} \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]} \colon \mathord{\left[\![{\gamma}\right]\!]} \times (\mathord{\left[\![{\delta}\right]\!]} \Rightarrow \mathcal{T} \mathord{\left[\![{D}\right]\!]}) \to \mathcal{T} \mathord{\left[\![{D}\right]\!]}, \qquad \mathsf{op} \in \Sigma \end{equation*}

in $\mathbb{C}$ . An $\mathcal{A}$ -algebra $\alpha$ can be constructed from the set of morphisms $\{ \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]} \}_{\mathsf{op} \in \Sigma}$ . The map (5.11) is defined as follows.

(5.12) \begin{equation} \begin{split} \mathbb{C}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathcal{T}(\mathord{\left[\![{\delta}\right]\!]} \times S)) \times \mathbb{C}(\mathord{\left[\![{\delta}\right]\!]} \times S, \mathcal{T} \mathord{\left[\![{D}\right]\!]}) & \to \mathbb{C}(\mathord{\left[\![{\gamma}\right]\!]} \times S, \mathcal{T} \mathord{\left[\![{D}\right]\!]}) \\ (\mathop{\mathrm{first}}\nolimits_S(\mathsf{op}), b) & \mapsto \Lambda^{-1}( \Lambda \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]} \circ (\Lambda b)). \end{split} \end{equation}

The key is that if $\mathcal{A}(A, B) = \mathbb{C}(A, \mathcal{T} B)$ , we have

(5.13) \begin{equation} \mathcal{L}_{A, B, C} \colon \mathcal{A}^{\circ}(C \times A, B) \cong \mathcal{A}^{\circ}(C, \mathcal{A}^{\circ}(A, B)) \qquad \text{for any $A, B, C \in \mathbb{C}$.} \end{equation}

Conversely, assume that (5.13) holds. We have

\begin{align*} \mathcal{L}_{A, B, \mathcal{A}^{\circ}(A, B)}^{-1} \colon \mathcal{A}^{\circ}(\mathcal{A}^{\circ}(A, B), \mathcal{A}^{\circ}(A, B)) & \to \mathcal{A}^{\circ}(\mathcal{A}^{\circ}(A, B) \times A, B) \\ \mathrm{id}_{\mathcal{A}^{\circ}(A, B)} & \mapsto \mathcal{L}_{A, B, \mathcal{A}^{\circ}(A, B)}^{-1}(\mathrm{id}_{\mathcal{A}^{\circ}(A, B)}) =: \mathrm{app}_{A,B}. \end{align*}

The arrow with the maps $\mathrm{app}_{A,B}$ are known as a higher-order arrow (Hughes, Reference Hughes2000), which is equivalent to an ordinary monad (i.e. $\mathcal{A}(A, B) = \mathbb{C}(A, \mathcal{T} B)$ for a monad $\mathcal{T}$ ).

5.4 Soundness and adequacy

We prove the soundness (Theorem 5.13) of the operational semantics in Section 4.2 for the denotational semantics in Section 5.3.

First, observe the denotations of substituted terms and commands.

1. 1. If $\Gamma, x : A \vdash M : B$ and $\Gamma \vdash V : A$ , then $\mathord{\left[\![{M[V / x]}\right]\!]}^S(c) = \mathord{\left[\![{M}\right]\!]}^S(c, \mathord{\left[\![{V}\right]\!]}^S(c))$ .

2. 2. If and $\Gamma \vdash V : A$ , then $\mathord{\left[\![{P[V / x]}\right]\!]}^S(c) = \mathord{\left[\![{P}\right]\!]}^S(c, \mathord{\left[\![{V}\right]\!]}^S(c))$ .

3. 3. If and $\Gamma, \Delta \vdash V : A$ , then

The following lemma is used to show the soundness for $(\mathop{\mathbf{handle}} \mathcal{F}[\mathsf{op}(V)] \mathop{\mathbf{with}} H) \to Q_{\mathsf{op}}[V / z, (\lambda^{\bullet} y : \delta . \mathop{\mathbf{handle}} \mathcal{F}[\lfloor{y}\rfloor] \mathop{\mathbf{with}} H) / k]$ .

Lemma 5.12. If , then

\begin{equation*} \mathord{\left[\![{\mathcal{F}[\mathsf{op}(V)]}\right]\!]}^S(\star) = \mathop{\mathrm{first}}\nolimits_S(\mathop{\mathrm{arr}}\nolimits(\mathord{\left[\![{V}\right]\!]}^S) \mathrel{>\!\!>\!\!>} \mathsf{op}) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{\mathcal{F}[\lfloor{y}\rfloor]}\right]\!]}^S(\star) \end{equation*}

holds.

Combining Lemmas 5.11 and 5.12, we obtain the soundness theorem for the arrow calculus with operations and handlers.

1. 1. If $\diamond \vdash M : A$ and $M \to M'$ , then $\mathord{\left[\![{M}\right]\!]}^S = \mathord{\left[\![{M'}\right]\!]}^S$ for any S.

2. 2. If and $P \to P'$ , then $\mathord{\left[\![{P}\right]\!]}^S = \mathord{\left[\![{P'}\right]\!]}^S$ for any S.

Next, we prove the adequacy theorem using logical relations as done in Bauer and Pretnar (Reference Bauer and Pretnar2013), Sanada (Reference Sanada2023). The logical relations relate programs of type A and elements of $\mathord{\left[\![{A}\right]\!]}$ . Let $\mathord{BType} = \{ \mathrm{Unit} \}$ . We add a constant $\mathtt{\langle\rangle}$ to the terms and values. We also add the following derivation rules to the arrow calculus:

The interpretation $\mathord{\left[\![{\mathrm{Unit}}\right]\!]}$ is the singleton set $\{ \star \}$ and $\mathord{\left[\![{\mathtt{\langle\rangle}}\right]\!]}^S \colon \mathord{\left[\![{\Gamma}\right]\!]}^S \to \mathord{\left[\![{\mathrm{Unit}}\right]\!]}^S = \{ \star \}$ is the unique map.

Definition 5.14 (logical relation). We define relations $(\triangleleft_A) \subseteq \mathord{\left[\![{A}\right]\!]} \times \{ M \mid \diamond \vdash M : A \} $ and for each type A as follows:

\begin{align*} \star \triangleleft_{\mathrm{Unit}} M & \iff M \to^* \mathtt{\langle\rangle} \\ v \triangleleft_{A_1 \times A_2} M & \iff (M \to^* \langle {V_1}, {V_2} \rangle) \land (\pi_1(v) \triangleleft_{A_1} V_1) \land (\pi_2(v) \triangleleft_{A_2} V_2) \\ f \triangleleft_{A \to B} M & \iff (M \to^* \lambda x : A . M') \land \forall N. \forall w. (w \triangleleft_A N \implies fw \triangleleft_B MN) \\ a \triangleleft_{A \rightsquigarrow B} M & \iff (M \to^* \lambda^{\bullet} x : A . P) \land \forall N. \forall w. (w \triangleleft_A N \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_B M \bullet N) \end{align*}

\begin{align*} \mathop{\mathsf{nf}}\left({()}, {()}; {v}\right) \blacktriangleleft_A P & \iff \exists V. \, (v \triangleleft_A V) \land (P \to^* \lfloor{V}\rfloor) \\ \mathop{\mathsf{nf}}\left({(\mathsf{op})_{i=1}^n}, {(u_i)_{i=1}^n}; {v}\right) \blacktriangleleft_A P & \iff \left\{ \begin{array}{l} \exists U . \, (u_1 \triangleleft_{\gamma_1} U) \land (P \to^* \mathcal{F}[\mathsf{op}_1(U)]), \text{and} \\ \forall w. \forall W.\, (w \triangleleft_{\delta} W \implies \\ \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} \mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i=2}^n}, {(u_i)_{i=2}^n}; {v}\right) \blacktriangleleft_{A} \mathcal{F}[\lfloor{W}\rfloor]). \end{array} \right. \end{align*}

Note that by Proposition 5.5 every arrow term is equivalent to a normal form, and the relation $a \blacktriangleleft_A P$ is inductively defined on the number n of operations contained by an arrow term $a \in \mathcal{A}_{\Sigma}(1, \mathord{\left[\![{A}\right]\!]})$ .

1. 1. If $M \to^* M'$ and $v \triangleleft_A M'$ , then $v \triangleleft_A M$ .

2. 2. If $M \to^* M'$ and $v \triangleleft_A M$ , then $v \triangleleft_A M'$ .

3. 3. If $P \to^* P'$ and $a \blacktriangleleft_A P'$ , then $a \blacktriangleleft_A P$ .

4. 4. If $P \to^* P'$ and $a \blacktriangleleft_A P$ , then $a \blacktriangleleft_A P'$ .

We can prove the following theorem using Lemma 5.15.

1. 1. For $\Gamma \vdash M : A$ and $v_i \in \mathord{\left[\![{A_i}\right]\!]}$ and $V_i$ with $v_i \triangleleft_{A_i} V_i$ for each $i \in \{ 1 , \dots , m\}$ ,

   \begin{equation*} \mathord{\left[\![{M}\right]\!]}(v_1, \dots, v_m) \triangleleft_A M[V_1 / x_1 , \dots, V_m / x_m]. \end{equation*}

2. 2. For , $v_i \in \mathord{\left[\![{A_i}\right]\!]}$ and $V_i$ with $v_i \triangleleft_{A_i} V_i$ for each $i \in \{ 1 , \dots , m\}$ and $w_j \in \mathord{\left[\![{B_j}\right]\!]}$ and $W_j$ with $w_j \triangleleft_{B_j} W_j$ for each $j \in \{ 1 , \dots , n\}$ ,

   \begin{align*} & \mathop{\mathrm{arr}}\nolimits(\langle w_1, \dots , w_n\rangle) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}(v_1, \dots, v_m) \\ & \blacktriangleleft_C P[V_1 / x_1 , \dots, V_m / x_m, W_1 / y_1, \dots , W_n / y_n]. \end{align*}

Proof sketch The proof is done by induction on the derivation of $\Gamma \vdash M : A$ and .

Here, we only show the most non-trivial case , and the rest of the proof is sent to the appendix. The derivation is

By the induction hypothesis, we have

(5.14) \begin{equation} \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}(v_1 , \dots, v_m) \blacktriangleleft_C P[V_1 / x_1 , \dots, V_m / x_m, W / y] \end{equation}

for any w and W with $w \triangleleft_B W$ . Given N and w satisfying $w \triangleleft_B N$ , we have $N \to^* W$ for a value W by the definition of $\triangleleft_B$ . Applying Lemma 5.15(2), we have $w \triangleleft_B W$ . Hence, (5.14) holds for this w and W. Now, we have

\begin{align*} (\lambda^{\bullet} y : B. P[V_1 / x_1 , \dots, V_m / x_m]) \bullet N & \to^* (\lambda^{\bullet} y : B. P[V_1 / x_1 , \dots, V_m / x_m]) \bullet W \\ & \to P[V_1 / x_1 , \dots, V_m / x_m, W / y]. \end{align*}

Thus, applying Lemma 5.15(3), we have

\begin{equation*} \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}(v_1 , \dots, v_m) \blacktriangleleft_C (\lambda^{\bullet} y : B. P[V_1 / x_1 , \dots, V_m / x_m]) \bullet N. \end{equation*}

Since $\mathord{\left[\![{P}\right]\!]} = \mathord{\left[\![{\lambda^{\bullet} y : B. P}\right]\!]}$ , we have

\begin{equation*} \mathord{\left[\![{\lambda^{\bullet} y : B. P}\right]\!]}(v_1, \dots, v_m) \triangleleft_{B \rightsquigarrow C} (\lambda^{\bullet} y : B. P[V_1 / x_1 , \dots, V_m / x_m]). \end{equation*}

corollary of the above theorem, we can show adequacy.