Algebraic effects and handlers for arrows

Abstract

We present an arrow calculus with operations and handlers and its operational and denotational semantics. The calculus is an extension of Lindley, Wadler and Yallop’s arrow calculus.

The denotational semantics is given using a strong (pro)monad $\mathcal{A}$ in the bicategory of categories and profunctors. The construction of this strong monad $\mathcal{A}$ is not trivial because of a size problem. To build denotational semantics, we investigate what $\mathcal{A}$-algebras are, and a handler is interpreted as an $\mathcal{A}$-homomorphisms between $\mathcal{A}$-algebras.

The syntax and operational semantics are derived from the observations on $\mathcal{A}$-algebras. We prove the soundness and adequacy theorem of the operational semantics for the denotational semantics.

1 Introduction

Hughes (2000) introduced the notion of arrow as an extension of the notion of monad for Haskell to capture non-monadic computational effects. As a syntactic development, the arrow calculus was introduced by Lindley et al. (2010). Their calculus is an arrow version of Moggi’s metalanguage (Moggi, 1991). As a semantic development, Heunen and Jacobs (2006), Jacobs et al. (2009), Asada (2010) revealed that arrows are strong monads in the bicategory $\mathbf{Prof}$ of categories and profunctors.

It is a natural question whether we can construct an arrow version of algebraic effects and effect handlers since arrows are an extension of monads. Plotkin and Power (2001 a,b) presented an algebraic view for computational effects. Plotkin and Pretnar (2013) provided effect handlers as a way to implement effects. Algebraic effects and effect handlers are the foundations of programming languages with effects that correspond to finitary (or more generally ranked) monads. Can we obtain an arrow version of such foundations?

Lindley (2014) defined an effect system $\lambda_{\mathrm{flow}}$ which has algebraic effects and handlers for arrows, monads and idioms. However, the effect system $\lambda_{\mathrm{flow}}$ is not satisfactory for the following reasons.

• • The theoretical background of algebraic effects for arrows is ambiguous. Any categorical explanation of algebraic theories for arrows is not given.

• • The syntax is complicated. It is unclear why the construction of handlers is given in that way.

• • Denotational semantics is not defined. It seems hard to give denotational semantics because the algebraic foundation of effects and handlers is not discussed enough.

We present an arrow calculus with operations and handlers as an extension of the arrow calculus. We discuss a categorical foundation for algebraic theories for arrows and give denotational semantics for our calculus by constructing an appropriate strong monad in (). As a main result, soundness and adequacy theorems of the operational semantics with respect to denotational semantics are proven.

Our contributions are as follows.

• We describe algebras for arrows from a 2-categorical point of view.

• We present an arrow calculus with operations and handlers based on the notions of algebras for arrows. The progress and preservation theorems for the calculus are shown.

• We give a denotational semantics for the calculus and prove the soundness theorem.

  There are the following non-trivial points in defining the denotational semantics.

  • – The “smallness” of an appropriate strong monad in () $\mathbf{Prof}$ . The collection of arrow terms, which are arrow analogues of terms in ordinary algebraic theories, is a proper class, not a set. Hence, the “smallness” of a monad that we construct is not trivial. We prove the “smallness” of the monad by counting the number of normal forms of arrow terms, which was introduced by Yallop (2010) for Haskell programs of arrow types.

  • – A treatment of strength to construct an algebra from a handler. Unlike ordinary handlers, we need a trick to define an interpretation of handlers for arrows because of the strength of strong monads in $\mathbf{Prof}$ . We define interpretation $\mathord{\left[\![{{-}}\right]\!]}^{S}$ with a set S as a parameter to construct an algebra from a handler.

1.1 Arrows in Haskell

Hughes (2000, 2005) introduced arrows as a generalisation of monads. In Haskell, arrows are defined using a type class.

An instance of $\mathtt{Arrow}$ is required to satisfy the following arrow laws.

(1.1) \begin{align}(a \mathrel{\gt\!\!\gt\!\!\gt} b) \mathrel{\gt\!\!\gt\!\!\gt} c = a \mathrel{\gt\!\!\gt\!\!\gt} (b \mathrel{\gt\!\!\gt\!\!\gt} c)\end{align}

(1.2) \begin{align}\mathtt{arr}\ (g \circ f) & = \mathtt{arr}\ f \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{arr}\ g\end{align}

(1.3) \begin{align}\mathtt{arr}\ \mathrm{id} \mathrel{\gt\!\!\gt\!\!\gt} a & = a\end{align}

(1.4) \begin{align}a \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{arr}\ \mathrm{id} & = a\end{align}

(1.5) \begin{align}\mathtt{first}\ a \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{arr}\ (\mathrm{id} \times f) & = \mathtt{arr}\ (\mathrm{id} \times f) \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{first}\ a\end{align}

(1.6) \begin{align}\mathtt{first}\ a \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{arr}\ \pi_1 & = \mathtt{arr}\ \pi_1 \mathrel{\gt\!\!\gt\!\!\gt} a\end{align}

(1.7) \begin{align}\mathtt{first}\ a \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{arr}\ \alpha & = \mathtt{arr}\ \alpha \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{first}\ (\mathtt{first}\ a)\end{align}

(1.8) \begin{align}\mathtt{first}\ (\mathtt{arr}\ f) & = \mathtt{arr}\ (f \times \mathrm{id})\end{align}

(1.9) \begin{align}\mathtt{first}\ (a \mathrel{\gt\!\!\gt\!\!\gt} b) & = \mathtt{first}\ a \mathrel{\gt\!\!\gt\!\!\gt} \mathtt{first}\ b\end{align}

where $\pi_1 \colon X \times Y \to X$ is a projection, and $\alpha \colon (X \times Y) \times Z \to X \times (Y \times Z)$ is an associator.

We explain some intuition of the type class $\mathtt{Arrow}$ . Let $\mathtt{A}$ be an instance of $\mathtt{Arrow}$ . A type $\mathtt{A\ x\ y}$ is the type of computations whose input type is $\mathtt{x}$ and output type is $\mathtt{y}$ . The function $\mathtt{arr}$ makes pure computation $\mathtt{arr}\ f$ of type $\mathtt{A\ x\ y}$ from a function f of type x -> y. The function $\mathtt{(\mathrel{>\!\!>\!\!>})}$ composes two computations f of type $\mathtt{A\ x\ y}$ and g of type $\mathtt{A\ y\ z}$ and returns a computation $f \mathrel{>\!\!>\!\!>} g$ of type $\mathtt{A\ x\ z}$ . The function $\mathtt{first}$ introduces an additional type z to the input and output types of a computation f of type $\mathtt{A\ x\ y}$ and returns a computation $\mathtt{first}\ f$ of type $\mathtt{A\ (x,\ z)\ (y,\ z)}$ .

1.2 An example: logic circuit simulation by effects and handlers

Suppose we want to write a simulator for logic circuits. Logic circuits are composed of wires and gates. Wires connect gates and transmit boolean values. There are different types of gates, such as $\mathsf{AND}$ , $\mathsf{OR}$ , $\mathsf{NOT}$ and $\mathsf{NAND}$ . The gates $\mathsf{AND}$ , $\mathsf{OR}$ and $\mathsf{NAND}$ take two boolean values as inputs and outputs one boolean value. The gate $\mathsf{NOT}$ takes one boolean value as an input and outputs one boolean value. See Table 1 for the definitions as boolean functions of the gates.

Table 1. Logic gates

1.2.1 Logic circuit simulation by ordinary algebraic effects and handlers

We can write a simulator for logic circuits in a language with ordinary algebraic effects and handlers. Let ${\Sigma_{\mathrm{LC}}}$ be . The set ${\Sigma_{\mathrm{LC}}}$ is a set of algebraic operations and called a signature. For example, is an operation that takes two boolean values as inputs and outputs one boolean value.

First, we write a handler to implement $\mathsf{NAND}$ and $\mathsf{OR}$ by $\mathsf{AND}$ and $\mathsf{NOT}$ .

\begin{align*} H_1 = \{ & \mathsf{NAND}(x,y), k \mapsto \mathop{\mathbf{let}} u \Leftarrow \mathsf{AND}(x,y) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(u) \mathop{\mathbf{in}} k(v) \\ & \mathsf{OR}(x,y), k \mapsto \mathop{\mathbf{let}} u \Leftarrow \mathsf{NOT}(x) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(y) \mathop{\mathbf{in}} \\ & \hspace{2cm} \mathop{\mathbf{let}} w \Leftarrow \mathsf{AND}(u,v) \mathop{\mathbf{in}} \mathop{\mathbf{let}} z \Leftarrow \mathsf{NOT}(w) \mathop{\mathbf{in}} k(z) \}\end{align*}

Second, we write a handler to implement $\mathsf{NOT}$ and $\mathsf{AND}$ .

\begin{align*} H_2 = \{ & \mathsf{AND}(x,y), k \mapsto \mathop{\mathbf{if}} x \mathop{\mathbf{then}} (\mathop{\mathbf{if}} y \mathop{\mathbf{then}} k(\mathtt{true}) \mathop{\mathbf{else}} k(\mathtt{false})) \mathop{\mathbf{else}} k(\mathtt{false}) \\ & \mathsf{NOT}(x), k \mapsto \mathop{\mathbf{if}} x \mathop{\mathbf{then}} k(\mathtt{false}) \mathop{\mathbf{else}} k(\mathtt{true}) \}\end{align*}

By the handlers $H_1$ and $H_2$ , we can simulate logic circuits. For example, we define a program P as

(1.10) \begin{equation} P = \left( \mathop{\mathbf{let}} x \Leftarrow \mathsf{NAND}(\mathtt{true}, \mathtt{false}) \mathop{\mathbf{in}} \mathop{\mathbf{let}} y \Leftarrow \mathsf{OR}(x, \mathtt{false}) \mathop{\mathbf{in}} \mathsf{AND}(y, \mathtt{true}) \right).\end{equation}

The program P corresponds to the following logic circuit.

Then, we can obtain the simulation result of P by handling it with $H_1$ and $H_2$ :

\begin{equation*} \mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} P \mathop{\mathbf{with}} H_1) \mathop{\mathbf{with}} H_2 \to^* \mathtt{true}.\end{equation*}

The advantage of using handlers is that the structure of a logic circuit can be separated from its implementation. We can use a different implementation for logic circuits using the following handlers:

\begin{equation*} H_3 = \left\{ \begin{array}{l} \mathsf{AND}(x,y), k \\ \mapsto \mathop{\mathbf{let}} u \Leftarrow \mathsf{NAND}(x,y) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(u) \mathop{\mathbf{in}} k(v) \\[0.5em] \mathsf{OR}(x,y), k \\ \mapsto \mathop{\mathbf{let}} u \Leftarrow \mathsf{NOT}(x) \mathop{\mathbf{in}} \mathop{\mathbf{let}} v \Leftarrow \mathsf{NOT}(y) \mathop{\mathbf{in}} \mathop{\mathbf{let}} w \Leftarrow \mathsf{NAND}(u,v) \mathop{\mathbf{in}} k(w) \end{array} \right\}\end{equation*}

\begin{equation*} H_4 = \{ \mathsf{NOT}(x), k \mapsto \mathop{\mathbf{let}} u \Leftarrow \mathsf{NAND}(x,x) \mathop{\mathbf{in}} k(u) \},\end{equation*}

\begin{equation*} H_5 = \{\mathsf{NAND}(x,y), k \mapsto \mathop{\mathbf{if}} x \mathop{\mathbf{then}} (\mathop{\mathbf{if}} y \mathop{\mathbf{then}} k(\mathtt{false}) \mathop{\mathbf{else}} k(\mathtt{true})) \mathop{\mathbf{else}} k(\mathtt{true}) \}.\end{equation*}

We have $\mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} P \mathop{\mathbf{with}} H_3) \mathop{\mathbf{with}} H_4) \mathop{\mathbf{with}} H_5 \to^* \mathtt{true}$ .

1.2.2 A problem of the approach with ordinary effects and handlers

Although we can write logic circuits with ordinary algebraic effects, the expressive power of programming languages with such effects is too high. This is because it is possible to describe dynamic- or meta-operations on circuits that cannot be realised in normal circuits. For example, let Q be the following program:

(1.11) \begin{equation} Q = \left( \mathop{\mathbf{let}} x \Leftarrow \mathsf{AND}(\mathtt{true}, \mathtt{false}) \mathop{\mathbf{in}} \mathop{\mathbf{if}} x \mathop{\mathbf{then}} \mathsf{AND}(x, \mathtt{true}) \mathop{\mathbf{else}} \mathsf{NOT}(x) \right).\end{equation}

This program corresponds to the following “logic circuit.”

The above “logic circuit” has dynamic selection of circuits according to the output value of the first $\mathsf{AND}$ gate. Since such dynamic selection is an “out-of-circuit” operation, we want to restrict the possibility of writing such a program.

1.2.3 Logic circuit simulation by the arrow calculus with operations and handlers

Since arrows generalise monads, the expression power of arrows is weaker than that of monads. We can exploit the constraints to restrict dynamic selection of logic circuits. Algebraic effects that correspond to arrows, which we introduce as the arrow calculus with operation and handlers in this paper, have a restriction such that it is impossible to perform conditional branching on their output to select subsequent algebraic effects.

The formal syntax of the arrow calculus with operations and handlers is given in Section 4.1. Here, we give informal descriptions of the syntax and explain the restriction.

The arrow calculus has two kinds of judgements:

where $\Gamma = x_1 : A_1, \dots, x_n : A_n$ and $\Delta = y_1 : B_1, \dots, y_m : B_m$ are typing environments and A is a type. The term M is a pure function of the context, of type A. The command P is a computation which takes inputs of types $\Delta$ and returns an output of type A under the context $\Gamma$ . Compared to the arrow class in Haskell (Section 1.1), the command P corresponds to a Haskell function of type “ $\Gamma \to \mathtt{Ar}\ \Delta\ A$ ” where $\mathtt{Ar}$ is an instance of the arrow class $\mathtt{Arrow}$ .

If we have a pure function M from $\Delta$ to A, we can obtain a pure command:

This rule corresponds to $\mathtt{arr}$ of the class $\mathtt{Arrow}$ in Haskell.

Let $\Sigma$ be a set of operations, called a signature. For an operation $\mathsf{op} \in \Sigma$ , we can perform the operation with an input M:

Abstraction and application of commands are given by the following rules, respectively:

where the type $A \rightsquigarrow B$ corresponds to a type $\mathtt{Ar}\ A\ B$ in Haskell. The rule for $L \bullet M$ corresponds to $\mathtt{(\mathrel{>\!\!>\!\!>})}$ of the class $\mathtt{Arrow}$ in Haskell.

We also have sequential composition $\mathop{\mathbf{let}} x \Leftarrow P \mathop{\mathbf{in}} Q$ of commands P and Q, which corresponds to $\mathtt{(\mathrel{>\!\!>\!\!>})}$ and $\mathtt{first}$ in Haskell:

For terms M, $N_1$ and $N_2$ , we can add $\mathop{\mathbf{if}} M \mathop{\mathbf{then}} N_1 \mathop{\mathbf{else}} N_2$ to the arrow calculus. If we add a conditional branching like $\mathop{\mathbf{if}} M \mathop{\mathbf{then}} P_1 \mathop{\mathbf{else}} P_2$ , where $P_1$ and $P_2$ are commands, to the syntax of the arrow calculus, we cannot interpret the calculus using strong promonads. This is an important difference from the ordinary algebraic effects.

This restriction comes from semantic observation. A term of an algebra of a promonad, which is a semantic counterpart of arrows, is a sequence (without branching) of operations, whereas a term of an algebra of an ordinary monad is a tree of operations. Hence, we cannot add a conditional branching to the arrow calculus because the algebraic structure has no branching, and we can do conditional branching in a language with ordinary algebraic effects because the algebraic structure has branching. This observation is informally described by Lindley (2014), and we give a formal explanation in Section 5.2.

Let us return to the simulation of logic circuits. Now we can restrict the dynamic selection of circuits by using the constraints of the arrow calculus. The program P defined by (1.10) is also a valid program in the arrow calculus, and Q defined by (1.11) is not a program in the arrow calculus.

In the arrow calculus with operations and handlers, handlers $H'_1$ and $H'_2$ corresponding to $H_1$ and $H_2$ are defined as follows.

Note that, in the construction of $H'_2$ , we can use $\mathop{\mathbf{if}}$ ’s because these $\mathop{\mathbf{if}}$ ’s select terms, not commands.

We can simulate logic circuits by handling P with $H'_1$ and $H'_2$ :

\begin{equation*} \mathop{\mathbf{handle}} (\mathop{\mathbf{handle}} P \mathop{\mathbf{with}} H'_1) \mathop{\mathbf{with}} H'_2 \to^* \lfloor{\mathtt{true}}\rfloor.\end{equation*}

We can also construct handlers $H'_3$ , $H'_4$ and $H'_5$ corresponding to $H_3$ , $H_4$ and $H_5$ . For more details, see Section 4.3.1.

1.3 The structure of this paper

The rest of this paper is organised as follows. Section 2 is a section on categorical preliminaries. In Section 3, we describe algebras for a monad in the bicategory of categories and profunctors and observe the universality of a free algebra. The arrow calculus with operations and handlers is introduced in Section 4. Typing rules and operational semantics are presented. In Section 5, we define the denotational semantics for the arrow calculus with operations and handlers. The definition of models is given in Section 5.1. We tackle the “smallness” problem and construct a model in Section 5.2. In Section 5.3, we define the interpretation with attention to the treatment of strength. Soundness and adequacy are shown in Section 5.4.

2 Preliminaries on category theory

In this paper, we assume that the readers are familiar with basic notions of category theory such as adjunctions, monads, presheaves, the Yoneda lemma, Eilenberg–Moore categories and monoidal categories as described in a textbook by Mac Lane (1971). A textbook by Leinster (2014) is also a good reference for category theory. We use advanced topics of category theory such as coends, 2-categories, bicategories and enriched categories. Readers unfamiliar with coends are referred to Appendix A. Readers unfamiliar with higher categories such as 2-categories, bicategories and enriched categories are referred to Appendix B.

Throughout this paper, we use the following notation.

Notation 2.1. We denote the categories of sets and maps and classes and maps of classes as $\mathbf{Set}$ and $\mathbf{Ens}$ , respectively. The 2-category of small categories and functors is denoted by $\mathbf{Cat}$ . For a category $\mathbb{C}$ , we write the class of objects of $\mathbb{C}$ as $\mathrm{Ob}(\mathbb{C})$ . We write $\mathrm{Id}_{\mathbb{C}}$ for the identity functor on $\mathbb{C}$ . When a category $\mathbb{C} = (\mathbb{C}, \otimes, J)$ is symmetric monoidal closed, we write $\Lambda \colon \mathbb{C}(A \otimes B, C) \to \mathbb{C}(A, B \Rightarrow C)$ for the currying operator, where $B \Rightarrow C$ is an internal hom of the symmetric monoidal closed category $\mathbb{C}$ .

2.1 Profunctors

Arrows can be seen as strong monads in the bicategory $\mathbf{Prof}$ of categories and profunctors (Heunen and Jacobs, 2006; Jacobs et al., 2009; Asada, 2010). 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 (1971, Section 9) or Loregian (2021, Section 1).

Definition 2.2 (profunctor, Bénabou, 2000). 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, 1989, 1991). 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.

Definition 2.3. (strong promonad, Asada, 2010; Asada and Hasuo, 2010). Let $\mathbb{C} = (\mathbb{C}, \otimes, J)$ be a monoidal category. A strong promonad on $\mathbb{C}$ is a profunctor with 2-cells $\eta^{\mathcal{A}} \colon \mathrm{I}_{\mathbb{C}} \Rightarrow \mathcal{A}$ , $\mu^{\mathcal{A}} \colon \mathcal{A} \circ \mathcal{A} \Rightarrow \mathcal{A}$ , and $\sigma^{\mathcal{A}} \colon ({\otimes}_{*}) \circ (\mathcal{A} \times \mathrm{I}_{\mathbb{C}}) \Rightarrow \mathcal{A} \circ ({\otimes}_{*})$ :

satisfying the axioms shown in Figure 1.

Fig. 1. Axioms for a strong promonad.

Hughes (2000), Jacobs et al. (2009), Asada (2010) 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 (2010, Theorem 14):

From a monad, we can obtain a promonad:

Proposition 2.4. Let $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ be a monad. The profunctor is 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, 1972):

(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, 1985) 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$ .

Definition 2.5 (the Eilenberg–Moore category of a promonad, Wood, 1985). Let be a promonad in $\mathbf{Prof}$ . The Eilenberg–Moore category $\mathop{\mathcal{E\!\!M}}(\mathcal{A})$ of $\mathcal{A}$ is defined as follows:

• • $\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 (2010) 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 (1982, 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)$ .

Definition 2.7 (Asada, 2010). Let $\mathbb{V}$ be a symmetric monoidal category, $\mathbb{V}'$ be a sufficiently cocomplete symmetric monoidal closed category and $J \colon \mathbb{V} \to \mathbb{V}'$ be a symmetric strong monoidal fully faithful functor. A $\mathbb{V}'$ -profunctor is $\mathbb{V}$ -small if there exists a $\mathbb{V}'$ -functor $F^{\circ} \colon \mathbb{D}^{\mathrm{op}} \otimes \mathbb{C} \to \mathbb{V}$ such that $J \circ F^{\circ} = F$ :

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 Algebras of arrows

For an ordinary monad $\mathcal{T} \colon \mathbb{C} \to \mathbb{C}$ , a $\mathcal{T}$ -algebra is a pair $\langle A , a \rangle$ of an object $A \in \mathbb{C}$ and a morphism $a \colon \mathcal{T} A \to A$ in $\mathbb{C}$ satisfying appropriate axioms, that is an object of the Eilenberg-Moore category $\mathop{\mathcal{E\!\!M}}(\mathcal{T})$ . An ordinary effect handler is interpreted as a homomorphism between two $\mathcal{T}$ -algebras.

What is an $\mathcal{A}$ -algebra for a promonad ? We answer this question in the next section (Section 3.1) from a 2-categorical point of view. We also discuss the universality of a free $\mathcal{A}$ -algebra in Section 3.2. A handler for arrows is interpreted as a homomorphism between $\mathcal{A}$ -algebras in the sense of Section 3.1.

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.

Definition 3.1 (algebras and homomorphisms). Let be a promonad. An algebra for $\mathcal{A}$ is a pair $\langle G, \alpha \rangle$ of 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}$ . A homomorphism h from an algebra $\langle G, \alpha \rangle$ to an algebra $\langle H, \beta \rangle$ , written $h \colon \langle G, \alpha \rangle \to \langle H, \beta \rangle$ , is a 2-cell $h \colon G \Rightarrow H$ in $\mathbf{Prof}$ such that $\beta \circ (\mathcal{A} h) = h \circ \alpha$ .

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}$ .

Remark 3.2. We defined an algebra as a morphism from $\mathbf{1}$ to an Eilenberg–Moore object. We justify the use of $\mathbf{1}$ . A morphism $\mathbb{D} \to \mathop{\mathcal{E\!\!M}}(\mathcal{T})$ in $\mathbf{Cat}$ corresponds to $\mathbf{1} \to \mathop{\mathcal{E\!\!M}}(\mathbf{Cat}(\mathbb{D}, \mathcal{T}))$ . Similarly, a morphism in $\mathbf{Prof}$ corresponds to . In both case, a morphism from a category $\mathbb{D}$ to an Eilenberg–Moore object of a (pro)monad corresponds to a morphism from $\mathbf{1}$ to another Eilenberg–Moore object.

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)

Proof We define $\phi^{\dagger} = \alpha \circ (\mathcal{A}\phi) \circ \rho^{-1} \colon \mathcal{A}({-}, C) \to G$ where $\rho$ is the right unitor:

(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 The arrow calculus with operations and handlers

The arrow calculus was introduced by Lindley et al. (2010, 2011). We add operations and handlers to their calculus.

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., 2010, 2011) 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.

Proposition 4.1 (progress). The following hold.

1. 1. For any well-typed term $\diamond \vdash M : A$ , there exists a term M’ such that $M \to M'$ or M is a value.

2. 2. For any well-typed command , one of following holds.

   1. a. There exists a command P’ such that $P \to P'$ .

   2. b. $P = \lfloor{V}\rfloor$ for some value V.

   3. c. $P = \mathcal{F}{[\mathsf{op}(V)]}$ for some operation $\mathsf{op}$ , value V and context $\mathcal{F}$ .

Lemma 4.2 (substitution) Let $\Gamma$ and $\Delta$ be contexts. The following hold.

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.

Proof The proof is by induction on the derivations.

Proposition 4.3 (Type preservation) The following hold.

1. 1. For any well-typed term $\diamond \vdash M : A$ , if $M \to M'$ then $\diamond \vdash M' : A$ .

2. 2. For any well-typed command , if $P \to P'$ then .

Proof The proof is by induction on the derivation of $M \to M'$ and $P \to P'$ , and Lemma 4.2.

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 Denotational semantics

5.1 Models of arrow calculus

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

Definition 5.1 (a model of arrow calculus). A model of the arrow calculus consists of the following data.

• • 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 (2010). 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 (2010) 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.

Proposition 5.6. The data $(\mathbf{Set}, \mathbf{Ens}, J, \mathcal{A}_{\Sigma})$ is a model of the arrow calculus (Definition 5.1).

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, 2000), 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.

Lemma 5.11. The following hold.

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.

Theorem 5.13 (soundness). The following hold.

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 (2013), Sanada (2023). 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]\!]})$ .

Lemma 5.15. The following hold.

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.

Theorem 5.16. Let $\Gamma = x_1 : A_1 , \dots , x_m : A_m$ and $\Delta = y_1 : B_1, \dots, y_n : B_n$ . The following hold.

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.

Corollary 5.17 (adequacy) If and $\mathord{\left[\![{P}\right]\!]} = \mathop{\mathrm{arr}}\nolimits(\star) \in \mathcal{A}_{\Sigma}(1, \mathord{\left[\![{\mathrm{Unit}}\right]\!]})$ , then $P \to^* \lfloor{\mathtt{\langle\rangle}}\rfloor$ .

Proof By Theorem 5.16, we have $\mathop{\mathrm{arr}}\nolimits(\star) = \mathord{\left[\![{P}\right]\!]} \blacktriangleleft_{\mathrm{Unit}} P$ . By the definition of $\blacktriangleleft_{\mathrm{Unit}}$ , we have $P \to^* \lfloor{V}\rfloor$ for a value V and $\star \triangleleft_{\mathrm{Unit}} V$ . By the definition of $\triangleleft_{\mathrm{Unit}}$ , we have $V = \mathtt{\langle\rangle}$ . Hence, $P \to^* \lfloor{\mathtt{\langle\rangle}}\rfloor$ .

6 Related work

Paterson (2001) introduced a notation for arrows. As mentioned by Lindley et al. (2010), there is a translation between the arrow calculus and Paterson’s notation, see Table 3.

Table 3. Translation between the arrow calculus and Paterson’s notation

There is another approach to semantics for arrows: Freyd categories (Atkey, 2011). As Asada (2010, Theorem 23) proved, small strong monads on $\mathbb{C}$ in with respect to the Yoneda embedding are equivalent to arrows in the sense of Atkey (2011, Definition 2.1). We have adopted the profunctor approach because it is easier to consider with regard to algebras, which are the basis of handlers.

T There are some notions of algebras for arrows or profunctors. Jacobs et al. (2009) defined an algebra for a promonad as a 2-cell $\chi \colon \mathcal{A} \Rightarrow \mathrm{I}_{\mathbb{C}}$ subject to some axioms (Jacobs et al., 2009, Definition 6.5), which is different from ours. From a 2-cell $\chi \colon \mathcal{A} \Rightarrow \mathrm{I}_{\mathbb{C}}$ , we obtain $\mathcal{A} \circ \mathbb{C}({-}, C) \Rightarrow \mathbb{C}({-}, C)$ for any $C \in \mathrm{Ob}(\mathbb{C})$ . Hence, an algebra in the sense of Jacobs et al. (2009) is a family of special algebras in this paper.

In nLab (2021), an algebra for a profunctor is defined as a pair (X, x) of an object $X \in \mathbb{C}$ and an element $x \in H(X,X)$ , which does not induce our definition of algebras.

Altenkirch et al. (2010) introduced relative monads as a generalisation of monads. Let $\mathbb{C}$ be a category and $\widehat{{\mathbb{C}}} = [\mathbb{C}^{\mathrm{op}}, \mathbf{Set}]$ . A relative monad ${\mathcal{T}} \colon \mathbb{C} \to \widehat{{\mathbb{C}}}$ on the Yoneda embedding corresponds to a promonad on $\mathbb{C}$ (Altenkirch et al., 2010, Theorem 9). An Eilenberg–Moore algebra for ${\mathcal{T}}$ is a pair $(G, \chi)$ of an object $G \in \widehat{{\mathbb{C}}}$ and a natural transformation subject to some axioms (Altenkirch et al., 2010, Definition 3). Eilenberg–Moore algebras for a relative monad ${\mathcal{T}}$ are equivalent to algebras in the sense of Definition 3.1 for the promonad $\mathcal{A}$ defined by $\mathcal{A}(X,Y) = {\mathcal{T}} YX$ . Especially, giving natural in Z is equivalent to giving $\alpha \colon \mathcal{A}(Y,Z) \times GY \to GZ$ natural in Z and extranatural in Y because we have

Here, we used end $\int_{X} ({-})$ , which is the dual notion of coend. Uustalu (2010) introduced strong relative monads, which corresponds to strong promonads.

Pieters et al. (2020) introduced handlers for monoidal effects. In their framework, an inductive handler for arrows (without static parameters) is constructed by giving a 2-cell $(\mathrm{I}_{\mathbb{C}} + \vec{\Sigma} \circ \mathcal{A}) \Rightarrow \mathcal{A}$ in the bicategory of (strong) profunctors, where . A 2-cell $(\mathrm{I}_{\mathbb{C}} + \vec{\Sigma} \circ \mathcal{A}) \Rightarrow \mathcal{A}$ consists of

• • a family of maps $\eta_{A,B} \colon \mathbb{C}(A,B) \to \mathcal{A}(A,B)$ natural in A and B, and

• • families of maps $\iota_{\mathrm{op},A,B,C} \colon \mathbb{C}(A,\mathord{\left[\![{\gamma}\right]\!]} \times (\mathord{\left[\![{\delta}\right]\!]}\Rightarrow C)) \times \mathcal{A}(C, B) \to \mathcal{A}(A,B)$ natural in A and B and extranatural in C.

From this semantic structure, Pieters et al. (2020) defined syntax of inductive handlers for arrows (without static parameters) as follows.

From an inductive handler, we can obtain a handler in the sense of this paper because we have the following map in $\mathbf{Set}$ :

Proposition 6.1. There is a map

for any set D.

Hence, given a 2-cell $h \colon (\mathrm{I}_{\mathbb{C}} + \vec{\Sigma} \circ \mathcal{A}) \Rightarrow \mathcal{A}$ , we have $\pi_1(\Xi(h)) \in \mathcal{A}(D,D)$ and $\{ \pi_{\mathsf{op}}(\pi_2(\Xi(h))) \colon \mathcal{A}(\mathord{\left[\![{\delta}\right]\!]}, D) \to \mathcal{A}(\mathord{\left[\![{\gamma}\right]\!]}, D)\}_{\mathsf{op}}$ , which determine a handler in the sense of this paper. Note that inductive handlers cannot modify the answer type whereas handlers in the sense of this paper can.

7 Conclusion and future work

We have introduced an arrow calculus with operations and handlers and defined its operational semantics and denotational semantics. The calculus design is based on categorical observations. The preservation and progress theorems are proved. We have also proved soundness and adequacy.

For future work, we plan to investigate the following topics.

$\lambda_{\mathrm{flow}}$ is a calculus with handlers for monads, arrows and idioms (Lindley, 2014). The relationship between the arrow calculus with operations and handlers and $\lambda_{\mathrm{flow}}$ is to be investigated. Is there translation from the arrow calculus with operations and handlers to Lindley’s $\lambda_{\mathrm{flow}}$ ?

Combination of handlers for monads and arrows in categorical way is interesting to investigate. Monoidal effects by Pieters et al. (2020) are one answer to this question. As another answer, can we use double categorical frameworks, focusing on the relationship between monads and promonads?

An algebraic theory corresponds to a finitary monad (Adamek and Rosicky, 1994). Can we develop a promonad version of such theory?