1 Introduction
Hughes (Reference Hughes2000) 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. (Reference Lindley, Wadler and Yallop2010). Their calculus is an arrow version of Moggi’s metalanguage (Moggi, Reference Moggi1991). As a semantic development, Heunen and Jacobs (Reference Heunen and Jacobs2006), Jacobs et al. (Reference Jacobs, Heunen and Hasuo2009), Asada (Reference Asada2010) 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 (Reference Plotkin and Power2001 a,b) presented an algebraic view for computational effects. Plotkin and Pretnar (Reference Plotkin and Pretnar2013) 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 (Reference Lindley2014) 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 (Reference Yallop2010) 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 (Reference Hughes2000, Reference Hughes2005) 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.
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.
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}$ .
Second, we write a handler to implement $\mathsf{NOT}$ and $\mathsf{AND}$ .
By the handlers $H_1$ and $H_2$ , we can simulate logic circuits. For example, we define a program P as
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$ :
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:
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:
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 (Reference Lindley2014), 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$ :
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 (Reference Mac Lane1971). A textbook by Leinster (Reference Leinster2014) 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, 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:
for $E \in \mathrm{Ob}(\mathbb{E})$ and $C \in \mathrm{Ob}(\mathbb{C})$ . The identity profunctor is defined by
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:
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.
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
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.
Definition 2.3. (strong promonad, Asada, Reference Asada2010; Asada and Hasuo, Reference Asada and Hasuo2010). 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.
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:
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, Reference Street1972):
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
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, Reference Wood1985). 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 (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}$ :
The identity $\mathbb{V}$ -profunctor is defined by
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, Reference Asada2010). 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.
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
between $\mathcal{A}$ -algebras that makes the following diagram commute up to isomorphism:
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:
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
and
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
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
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. (Reference Lindley, Wadler and Yallop2010, Reference Lindley, Wadler and Yallop2011). 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., 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.
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 .
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:
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.
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.
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. 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. For any well-typed command , one of following holds.
-
a. There exists a command P’ such that $P \to P'$ .
-
b. $P = \lfloor{V}\rfloor$ for some value V.
-
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. If $\Gamma, x : A \vdash M : B$ and $\Gamma \vdash N : A$ are derivable, then $\Gamma \vdash M[N / x] : B$ is derivable.
-
2. If and $\Gamma \vdash N : A$ are derivable, then is derivable.
-
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. For any well-typed term $\diamond \vdash M : A$ , if $M \to M'$ then $\diamond \vdash M' : A$ .
-
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.
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.
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.
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.
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.
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.
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).
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:
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
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
See Figure 8.
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
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]\!]})$ :
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}$ .
The interpretation $\mathord{\left[\![{\Gamma}\right]\!]}^S$ of a context $\Gamma$ is defined as an extension of the interpretation of types:
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.
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.
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. If $\Gamma \vdash M : A$ then $\mathord{\left[\![{M}\right]\!]}^S = \mathord{\left[\![{M}\right]\!]}$ for any S.
-
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. If $\Gamma \vdash M : A$ then $\mathord{\left[\![{M}\right]\!]}^1 = \mathord{\left[\![{M}\right]\!]}$ .
-
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
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
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.
The key is that if $\mathcal{A}(A, B) = \mathbb{C}(A, \mathcal{T} B)$ , we have
Conversely, assume that (5.13) holds. We have
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.
Lemma 5.11. The following hold.
-
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. 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. 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
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. If $\diamond \vdash M : A$ and $M \to M'$ , then $\mathord{\left[\![{M}\right]\!]}^S = \mathord{\left[\![{M'}\right]\!]}^S$ for any S.
-
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:
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. If $M \to^* M'$ and $v \triangleleft_A M'$ , then $v \triangleleft_A M$ .
-
2. If $M \to^* M'$ and $v \triangleleft_A M$ , then $v \triangleleft_A M'$ .
-
3. If $P \to^* P'$ and $a \blacktriangleleft_A P'$ , then $a \blacktriangleleft_A P$ .
-
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. 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. 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
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
Thus, applying Lemma 5.15(3), we have
Since $\mathord{\left[\![{P}\right]\!]} = \mathord{\left[\![{\lambda^{\bullet} y : B. P}\right]\!]}$ , we have
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 (Reference Paterson2001) introduced a notation for arrows. As mentioned by Lindley et al. (Reference Lindley, Wadler and Yallop2010), there is a translation between the arrow calculus and Paterson’s notation, see Table 3.
There is another approach to semantics for arrows: Freyd categories (Atkey, Reference Atkey2011). As Asada (Reference Asada2010, 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 (Reference Atkey2011, 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. (Reference Jacobs, Heunen and Hasuo2009) 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., Reference Jacobs, Heunen and Hasuo2009, 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. (Reference Jacobs, Heunen and Hasuo2009) 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. (Reference Altenkirch, Chapman and Uustalu2010) 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., Reference Altenkirch, Chapman and Uustalu2010, 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., Reference Altenkirch, Chapman and Uustalu2010, 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 (Reference Uustalu2010) introduced strong relative monads, which corresponds to strong promonads.
Pieters et al. (Reference Pieters, Rivas and Schrijvers2020) 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. (Reference Pieters, Rivas and Schrijvers2020) 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, Reference Lindley2014). 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. (Reference Pieters, Rivas and Schrijvers2020) 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, Reference Adamek and Rosicky1994). Can we develop a promonad version of such theory?
Acknowledgements
We thank Kazuyuki Asada for helpful discussions, suggestions on the structure of the paper and comments, Masahito Hasegawa, Ichiro Hasuo, Satoshi Kura, Keisuke Hoshino and Yuto Kawase for helpful discussions and comments and anonymous reviewers for their many valuable suggestions, comments and pointing us to related work. We also thank Soichiro Fujii for providing his gentle introduction to profunctors (Fujii Reference Fujii2021). This work was supported by JST Grant Number JPMJFS2123.
Conflicts of interest
None.
A Coends
In this section, we review the definition and construction of coends. We also give an informal description of coends.
Definition A.1. (extranatural transformation). Let $F, G \colon \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbb{D}$ be functors. An extranatural transformation $\phi$ from F to G, we write $\phi \colon F \Rightarrow G$ , is a family of morphisms $ (\phi_C \colon F(C, C) \to G(C, C))_{C \in \mathrm{Ob}(\mathbb{C})} $ such that the following diagram commutes for any morphisms $f \colon C \to C'$ in $\mathbb{C}$ :
In the following, we deal only with extranatural transformations whose codomain (G) is a constant functor.
A coend is a pair of an object and an extranatural transformation defined for a functor. It has a universal property like a colimit.
Definition 1.2 (coend). Let $F \colon \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbb{D}$ be a functor. A coend of F is a pair of an object $\int^{C \in \mathbb{C}} F(C, C) \in \mathbb{D}$ and an extranatural transformation
satisfying the following universal property. If $\phi \colon F \Rightarrow X$ is an extranatural transformation to an object $X \in \mathbb{D}$ , then there exists a unique morphism $\kappa \colon \int^{C \in \mathbb{C}} F(C, C) \to X$ such that $\phi = \kappa \circ \omega$ :
The existence of a coend of $F \colon \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbb{D}$ depends on the properties of $\mathbb{C}$ , $\mathbb{D}$ and F. The following proposition is known (Loregian, Reference Loregian2021, (1.29)) for the cases we often use in this paper.
Proposition A.3. If $\mathbb{C}$ is small, for the functor $F \colon \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbf{Set}$ , the coend $\omega \colon F \Rightarrow \int^{C \in \mathbb{C}} F(C, C)$ of F always exists.
Proof We only construct the set $\int^{C \in \mathbb{C}} F(C, C)$ and $\omega$ , and the proof of universality is left to the reader. First, we define an equivalence relation $\sim$ on a set $\coprod_{C \in \mathrm{Ob}(\mathbb{C})} F(C,C)$ as follows. For $a \in F(C,C)$ and $b \in F(C', C')$ , $a \sim b$ if there exists a morphism $f \colon C \to C'$ in $\mathbb{C}$ and $c \in F(C', C)$ such that $F(f, C)(c) = a$ and $F(C', f)(c) = b$ .
We write [a] for the equivalence class of $a \in F(C,C)$ in $\sim$ . Now, we define
We define $\omega_C \colon F(C,C) \to \int^{C \in \mathbb{C}} F(C, C)$ as the canonical injection:
The proof of Proposition A.3 relies on the construction (A1), which small cocompleteness of $\mathbf{Set}$ . Similarly, we can show that a coend $\int^C F(C,C)$ for a functor $F \colon \mathbf{Set}^{\mathrm{op}} \times \mathbf{Set} \to \mathbf{Ens}$ exists because $\mathbf{Ens}$ is sufficiently cocomplete.
Informally, we can think of $\int^{C \in \mathbb{C}}$ as an existential quantifier $\exists$ over $C \in \mathrm{Ob}(\mathbb{C})$ . An element w of $\int^{C \in \mathbb{C}} F(C, C)$ is regarded as a witness of a proposition that there exists $C \in \mathrm{Ob}(\mathbb{C})$ such that F(C, C) holds.
B 2-Categories, bicategories and enriched categories
B.1 2-Categories
Roughly speaking, a 2-category is a category whose hom-sets have a categorical structure.
Definition B.1 (2-categories). A 2-category $\mathbf{C}$ consists of the following data.
-
• A class $\mathrm{Ob}(\mathbf{C})$ . We call an element a of $\mathrm{Ob}(\mathbf{C})$ an object or a 0-cell.
-
• A family $\{ \mathbf{C}(a, b) \}_{a, b \in \mathrm{Ob}(\mathbf{C})}$ of categories, called hom-categories. We call an object f of $\mathbf{C}(a, b)$ a morphism or a 1-cell from a to b of $\mathbf{C}$ . A morphism $\alpha \colon f \to g$ in $\mathbf{C}(a, b)$ is called a 2-cell from f to g of $\mathbf{C}$ .
-
• An identity functor $\mathrm{id}_a \colon \mathbf{1} \to \mathbf{C}(a,a)$ for each $a \in \mathrm{Ob}(\mathbf{C})$ .
-
• A composition functor for each $a, b, c \in \mathrm{Ob}(\mathbf{C})$
subject to the following axioms expressed by the (strict) commutativity of
We write $f \colon a \to b$ for a 1-cell f from a to b, and $\alpha \colon f \Rightarrow g$ for a 2-cell $\alpha$ from f to g:
We also write $g \circ f$ for the composition of 1-cells $f \colon a \to b$ and $g \colon b \to c$ .
For 1-cells, the axiom (B1) is the associativity of composition and (B2) is the unitality of composition. Let $f \colon a \to b$ , $g \colon b \to c$ and $h \colon c \to d$ be 1-cells in a 2-category $\mathbf{C}$ . The associativity of composition (B1) for the 1-cells f, g and h is
in the hom-category $\mathbf{C}(a,d)$ , and the unitality (B2) for the 1-cell f is
in the hom-category $\mathbf{C}(a,b)$ .
An example of 2-categories is the 2-category $\mathbf{Cat}$ , whose 0-cells, 1-cells and 2-cells are small categories, functors and natural transformation, respectively.
2-category theory is a formal language to describe the ordinary category theory. For example, a definition of monads in 2-categories is as follows.
Definition B.2 (monads in 2-categories). Let $\mathbf{C}$ be a 2-category. A monad in $\mathbf{C}$ is an endo 1-cell $t \colon c \to c$ equipped with
-
• a 2-cell $\eta \colon \mathrm{id}_c \Rightarrow t$ called a unit and
-
• a 2-cell $\mu \colon t \circ t \Rightarrow t$ called a multiplication
such that the following axioms hold:
Monads in the 2-category $\mathbf{Cat}$ in the sense of Definition B.2 coincide with ordinary monads.
B.2 Bicategories
In the definition of 2-categories, the axioms (B1) and (B2) are strict in the sense that the equalities hold in the hom-categories. From a category-theoretic principle, these axioms may be too strict because we want to identify two functors in (B1) and (B2) which are not only strictly equal, but naturally isomorphic.
Definition B.3 (bicategories). A bicategory $\mathbf{C}$ consists of the same data in the definition of 2-categories (Definition B.1) which make (B1) and (B2) commute up to natural isomorphism.
For 1-cells $f \colon a \to b$ , $g \colon b \to c$ and $h \colon c \to d$ in a bicategory $\mathbf{C}$ , the associativity of composition (B1) and the unitality (B2) are expressed as follows:
The equalities in (B3) and (B4) are replaced by the isomorphisms.
We can obtain a definition of monads in bicategories from the definition of monads in 2-categories (Definition B.2).
B.3 Enriched categories
We write $\mathbf{Cat}_0 = (\mathbf{Cat}_0, \times, \mathbf{1})$ for the monoidal category of small categories and functors. In the definition of 2-categories (Definition B.1), the monoidal structure of $\mathbf{Cat}_0$ is essential to describe the identity functors $\mathrm{id}_a$ and composition functors and the axioms. The descriptions of the identity and composition in ordinary categories also use the monoidal structure of $\mathbf{Set} = (\mathbf{Set}, \times, 1)$ . We generalise (2-)categories from this perspective and obtain the following definition of enriched categories.
Definition B.4 (enriched category). Let $\mathbb{V} = (\mathbb{V}, \otimes, J)$ be a symmetric monoidal category. A $\mathbb{V}$ -enriched category (or simply a $\mathbb{V}$ -category) $\mathbb{C}$ consists of the following data.
-
• A class $\mathrm{Ob}(\mathbb{C})$ of objects.
-
• A family of objects $\{ \mathbb{C}(a,b) \}_{a, b \in \mathrm{Ob}(\mathbb{C})}$ of $\mathbb{V}$ . We call $\mathbb{C}(a,b) \in \mathbb{V}$ a hom-object.
-
• A morphism $\mathrm{id}_a \colon J \to \mathbb{C}(a,a)$ for each $a \in \mathrm{Ob}(\mathbb{C})$ , called an identity.
-
• A morphism for each $a, b, c \in \mathrm{Ob}(\mathbb{C})$ , called a composition
subject to the following axioms expressed by the commutativity of
An ordinary category is a $\mathbf{Set}$ -enriched category, and a 2-category in the sense of Definition B.1 is a $\mathbf{Cat}_0$ -enriched category.
The enriched version of a functor between categories is called a $\mathbb{V}$ -functor, which preserves $\mathbb{V}$ -category structures. See Kelly (Reference Kelly1982) for the definition.
C Proofs for Section 4 (The arrow calculus with operations and handlers)
Proposition 4.1 (progress). The following hold.
-
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. For any well-typed command , one of following holds.
-
a. There exists a command P’ such that $P \to P'$ .
-
b. <texmath>inline504</texmath> for some value V.
-
c. $P = \mathcal{F}{[\mathsf{op}(V)]}$ for some operation $\mathsf{op}$ , value V and context $\mathcal{F}$ .
-
Proof. (1). By induction on the derivation of $\diamond \vdash M : A$ .
In case . This case cannot happen because the context is empty.
In case . In this case, we have $M = \lambda x . N$ for some term N, and M is a value.
In case . We have
By the induction hypothesis, $M_1$ is a value or $M_1 \to M_1'$ for some $M_1'$ , and $M_2$ is a value or $M_2 \to M_2'$ for some $M_2'$ . If $M_1 \to M_1'$ holds for some $M_1'$ , then we have $M_1 M_2 \to M_1' M_2$ . If $M_1$ is a value, then $M_1 = \lambda x . N$ for some N because $\diamond \vdash M_1 : A \to B$ . We have two subcases: If $M_2$ is a value V, then we have $M_1 M_2 = (\lambda x . N) V \to N[V / x]$ . If $M_2 \to M_2'$ holds for some $M_2'$ , then we have $M_1 M_2 = (\lambda x . N) M_2 \to (\lambda x . N) M_2'$ .
In case . In this case, we have $M = \lambda^{\bullet} x . N$ for some term N, and M is a value.
In case .
By the induction hypothesis, $M_1$ is a value or $M_1 \to M_1'$ for some $M_1'$ , and $M_2$ is a value or $M_2 \to M_2'$ for some $M_2'$ . If $M_1 \to M_1'$ holds for some $M_1'$ , then we have $\langle {M_1}, {M_2} \rangle \to \langle {M_1'}, {M_2} \rangle$ . If $M_1$ is a value $V_1$ , we have two subcases: if $M_2$ is a value $V_2$ , then $M = \langle {M_1}, {M_2} \rangle = \langle {V_1}, {V_2} \rangle$ is a value. If $M_2 \to M_2'$ holds for some $M_2'$ , then we have $\langle {M_1}, {M_2} \rangle = \langle {V_1}, {M_2} \rangle \to \langle {V_1}, {M_2'} \rangle$ .
In case , . Straightforward.
(2). By induction on the derivation of .
In case . We have
for some term M. By (1), M is a value or $M \to M'$ holds for some M’. If M is a value V, then $P = \lfloor{V}\rfloor$ and this satisfies (b). If $M \to M'$ holds for some M’, then we have $P = \lfloor{M}\rfloor \to \lfloor{M'}\rfloor$ .
In case . We have
By the similar argument to Case T -App, we have either $L \bullet N \to L' \bullet N$ for some L’, $L = (\lambda^{\bullet} x. L_1)$ and $L \bullet N \to L \bullet N'$ for some N’, or $L = (\lambda^{\bullet} x. L_1)$ , N is a value, and $L \bullet N = (\lambda^{\bullet} x. L_1) \bullet V \to L_1[V/x]$ for some V.
In case . We have
By the induction hypothesis, we have the following three cases.
-
1. $P \to P'$ for some command P’. We have $(\mathop{\mathbf{let}} x \Leftarrow P \mathop{\mathbf{in}} Q) \to (\mathop{\mathbf{let}} x \Leftarrow P' \mathop{\mathbf{in}} Q)$ .
-
2. $P = \lfloor{V}\rfloor$ for some value term V. We have $(\mathop{\mathbf{let}} x \Leftarrow P \mathop{\mathbf{in}} Q) = (\mathop{\mathbf{let}} x \Leftarrow \lfloor{V}\rfloor \mathop{\mathbf{in}} Q) \to Q[V / x]$ .
-
3. $P = \mathcal{F}[\mathsf{op}(V)]$ for some value term V, operation symbol $\mathsf{op} \in \Sigma$ and context $\mathcal{F}$ . We have $P = \mathcal{F}'[\mathsf{op}(V)]$ for $\mathcal{F}' = (\mathop{\mathbf{let}} x \Leftarrow \mathcal{F} \mathop{\mathbf{in}} Q)$ .
In case . We have
By the induction hypothesis, M is a value or $M \to M'$ for some M’. If M is a value V, then $P = \mathsf{op}(V) = \mathcal{F}[\mathsf{op}(V)]$ for $\mathcal{F} = [{-}]$ . If $M \to M'$ holds, then $P = \mathsf{op}(M) \to \mathsf{op}(M')$ .
In case . We have
where . By the induction hypothesis, we have the following three cases.
-
1. $R \to R'$ for some command R’. We have $(\mathop{\mathbf{handle}} R \mathop{\mathbf{with}} H) \to (\mathop{\mathbf{handle}} R' \mathop{\mathbf{with}} H)$ .
-
2. $R = \lfloor{V}\rfloor$ for some value term V. We have
\[ (\mathop{\mathbf{handle}} R \mathop{\mathbf{with}} H) = (\mathop{\mathbf{handle}} \lfloor{V}\rfloor \mathop{\mathbf{with}} H) \to P[V / x]. \] -
3. $R = \mathcal{F}[\mathsf{op}(V)]$ for some value term V, operation symbol $\mathsf{op} \in \Sigma$ and context $\mathcal{F}$ . We have
D Proofs for Section 5 (Denotational semantics)
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
Proof prove by induction on the structure of $a \in \mathrm{Arr}_{\Sigma}(A, B)$ .
In case $a = \mathop{\mathrm{arr}}\nolimits(f)$ for some $f \colon A \to B$ . This case is proved in the main text.
In case $a = \mathsf{op}$ for some with $\mathord{\left[\![{\gamma}\right]\!]} = A$ and $\mathord{\left[\![{\delta}\right]\!]} = B$ . This case is proved in the main text.
In case $a = \mathop{\mathrm{first}}\nolimits_X(a')$ for some $a' \in \mathrm{Arr}_{\Sigma}(A', B')$ with $A' \times X = A$ and $B' \times X = B$ . By the induction hypothesis, we have
for some $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_m}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_1}\right]\!]} \times A' \to B'$ .
We show $a = \mathop{\mathrm{first}}\nolimits_{X}(a') \sim \mathop{\mathsf{nf}}\left({(\mathsf{op}_i)_{i = 1, \dots, n}}, {(f'_i)_{i = 1, \dots, n}}; {g \times \mathrm{id}_X}\right)$ for some $f'_i$ ( $i = 1, \dots, n$ ) by induction on n.
In the base case, $n = 0$ , we have
We assume that the claim holds in case n and show the claim in case $n + 1$ . We have
where $f'_1 = f_1 \circ \pi_1 \colon A' \times X \to \mathord{\left[\![{\gamma_1}\right]\!]}$ . See Figure D1.
In case $a = b \mathrel{>\!\!>\!\!>} c$ for some $b \in \mathrm{Arr}_{\Sigma}(A, X)$ and $c \in \mathrm{Arr}_{\Sigma}(X, B)$ . By the induction hypothesis, we have
for some $m \in \mathbb{N}$ , , $(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, m}$ and $g' \colon \mathord{\left[\![{\delta_n}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_1}\right]\!]} \times A \to X$ , and
for some $n \in \mathbb{N}$ , , $(f'_i \colon \mathord{\left[\![{\delta_{m + i-1}}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_{m + 1}}\right]\!]} \times A \to \mathord{\left[\![{\gamma_{m + i}}\right]\!]})_{i = 1 , \dots, n}$ and $g'' \colon \mathord{\left[\![{\delta_{m + n + 1}}\right]\!]} \times \cdots \times \mathord{\left[\![{\delta_{m + 1}}\right]\!]} \times X \to B$ . We show $a = b \mathrel{>\!\!>\!\!>} c \sim \mathop{\mathsf{nf}}\left({(\mathsf{op})_{i = 1, \dots, m + n}}, {(f_i)_{i = 1, \dots, m + n}}; {g}\right)$ for some $(f_i)_{i = m + 1, \dots, m + n}$ and g by induction on n.
In the base case, $n = 0$ , we have
We assume that the claim holds in case n, and show the claim in case $n + 1$ . We have
where $f_{m + 1} = f'_1 \circ g'$ . See Figure D2. By the induction hypothesis, we obtain
for some $(f_{m + 1 + i})_{i = 1, \dots, n}$ and g.
Lemma 5.11. The following hold.
-
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. 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. If and $\Gamma, \Delta \vdash V : A$ , then
Proof. The proof is by induction on the derivations.
(1). In case . The derivation is
By the induction hypothesis (1), we have
for any $c \in \mathord{\left[\![{\Gamma}\right]\!]}^S$ . Hence, we have
In case . The derivation is
By the induction hypothesis (1), we have
for any $c \in \mathord{\left[\![{\Gamma}\right]\!]}^S$ . Hence, we have
In case . The derivation is
By the induction hypothesis (3), we have
Hence, we have
In case . The derivation is
By the induction hypothesis (1), we have
for any $c \in \mathord{\left[\![{\Gamma}\right]\!]}^S$ . Hence, we have
In case . The derivation is
By the induction hypothesis (3), we have
Hence, we have
Lemma 5.12. If , then
holds.
Proof The proof is by induction on the structure of $\mathcal{F}$ .
If $\mathcal{F} = [{-}]$ , then we have
Otherwise, $\mathcal{F} = (\mathop{\mathbf{let}} x \Leftarrow \mathcal{F}' \mathop{\mathbf{in}} P)$ , we have
by the induction hypothesis.
Theorem 5.13 (soundness). The following hold.
-
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. If and $P \to P'$ , then $\mathord{\left[\![{P}\right]\!]}^S = \mathord{\left[\![{P'}\right]\!]}^S$ for any S.
Proof By induction on the derivations $M \to M'$ and $P \to P'$ .
(1). In case . We have $\diamond \vdash \mathop{\mathbf{fst}} \langle {V_1}, {V_2} \rangle : A_1$ and $\mathop{\mathbf{fst}} \langle {V_1}, {V_2} \rangle \to V_1$ . The derivation of $\diamond \vdash \mathop{\mathbf{fst}} \langle {V_1}, {V_2} \rangle : A_1$ is
We have
for any S and $\star \in \mathord{\left[\![{\diamond}\right]\!]}^S = 1 = \{ \star \}$ .
In case . Similar to the case .
In case . We have $\diamond \vdash (\lambda x : A. M) V : B$ and $(\lambda x : A . M) V \to M[V / x]$ . The derivation of $\diamond \vdash (\lambda x : A. M) V : B$ is
We have
for any S and $\star \in \mathord{\left[\![{\diamond}\right]\!]}^S = 1 = \{ \star \}$ .
In case . We have $\diamond \vdash \mathcal{E}[M] : A$ and $\mathcal{E}[M] \to \mathcal{E}[M']$ . From the derivation of $\mathcal{E}[M] \to \mathcal{E}[M']$ , we have $M \to M'$ . By the induction hypothesis, we have $\mathord{\left[\![{M}\right]\!]}^S = \mathord{\left[\![{M'}\right]\!]}^S$ . We obtain $\mathord{\left[\![{\mathcal{E}[M]}\right]\!]}^S = \mathord{\left[\![{\mathcal{E}[M']}\right]\!]}^S$ by induction on the structure of $\mathcal{E}$ .
(2). In case . We have and $(\lambda^{\bullet} x : A . P) \bullet V \to P[V / x]$ . The derivation of is
We have
for any S and $\star \in \mathord{\left[\![{\Gamma}\right]\!]}^S = 1 = \{ \star \}$ .
In case . We have and $\mathop{\mathbf{let}} x \Leftarrow \lfloor{V}\rfloor \mathop{\mathbf{in}} Q \to Q[V / x]$ . The derivation of is
We have
for any S and $\star \in \mathord{\left[\![{\diamond}\right]\!]}^S = 1 = \{ \star \}$ .
In case . We have and $\mathop{\mathbf{handle}} \lfloor{V}\rfloor \mathop{\mathbf{with}} H \to P[V / x]$ where . The derivation of is
where C and D are primitive. We have
for any S and $\star \in \mathord{\left[\![{\diamond}\right]\!]}^S = 1 = \{ \star \}$ .
In case . We have and $\mathop{\mathbf{handle}} \mathcal{F}[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]$ where . The derivation of is
where C and D are primitive. We have
In case . We have and $\mathcal{F}[P] \to \mathcal{F}[P']$ . From the derivation of $\mathcal{F}[P] \to \mathcal{F}[P']$ , we have $P \to P'$ . By the induction hypothesis, we have $\mathord{\left[\![{P}\right]\!]}^S = \mathord{\left[\![{P'}\right]\!]}^S$ .
We show $\mathord{\left[\![{\mathcal{F}[P]}\right]\!]}^S = \mathord{\left[\![{\mathcal{F}[P']}\right]\!]}^S$ by induction on the structure of $\mathcal{F}$ . If $\mathcal{F} = [{-}]$ , we have nothing to do. Suppose $\mathcal{F} = \mathop{\mathbf{let}} x \Leftarrow \mathcal{F}' \mathop{\mathbf{in}} Q$ . By the induction hypothesis, we have $\mathord{\left[\![{\mathcal{F}'[P]}\right]\!]}^S = \mathord{\left[\![{\mathcal{F}'[P']}\right]\!]}^S$ . From the definition of the interpretation of $\mathop{\mathbf{let}} x \Leftarrow R \mathop{\mathbf{in}} Q$ , we obtain $\mathord{\left[\![{\mathcal{F}[P]}\right]\!]}^S = \mathord{\left[\![{\mathop{\mathbf{let}} x \Leftarrow \mathcal{F}'[P] \mathop{\mathbf{in}} Q}\right]\!]}^S = \mathord{\left[\![{\mathop{\mathbf{let}} x \Leftarrow \mathcal{F}'[P'] \mathop{\mathbf{in}} Q}\right]\!]}^S = \mathord{\left[\![{\mathcal{F}[P']}\right]\!]}^S$ .
Lemma 5.15. The following hold.
-
1. If $M \to^* M'$ and $v \triangleleft_A M'$ , then $v \triangleleft_A M$ .
-
2. If $M \to^* M'$ and $v \triangleleft_A M$ , then $v \triangleleft_A M'$ .
-
3. If $P \to^* P'$ and $a \blacktriangleleft_A P'$ , then $a \blacktriangleleft_A P$ .
-
4. If $P \to^* P'$ and $a \blacktriangleleft_A P$ , then $a \blacktriangleleft_A P'$ .
Proof We can prove (3) and (4) straightforwardly by the definition. To prove (1) and (2), we do induction on the type A.
(1). In case Unit. Suppose $M \to^* M'$ and $v \triangleleft_{\mathrm{Unit}} M'$ . We have $v = \star$ and $M' \to^* \mathtt{\langle\rangle}$ by the definition of $\triangleleft_{\mathrm{Unit}}$ . Hence, we have $M \to^* M' \to^* \mathtt{\langle\rangle}$ , which means $v \triangleleft_{\mathrm{Unit}} M$ .
In case $A_1 \times A_2$ . Suppose $M \to^* M'$ and $v \triangleleft_{A_1 \times A_2} M'$ . We have $M \to^* M' \to^* \langle {V_1}, {V_2} \rangle$ , $\pi_1(v) \triangleleft_{A_1} V_1$ and $\pi_2(v) \triangleleft_{A_2} V_2$ . This means $v \triangleleft_{A_1 \times A_2} M$ .
In case $A \to B$ . Suppose $M \to^* M'$ and $f \triangleleft_{A \to B} M'$ . We have $M \to^* M' \to^* \lambda x : A . M''$ and $(w \triangleleft_{A} N \implies fw \triangleleft_{B} M'N)$ for any N and w. Given N and w with $w \triangleleft_{A} N$ , we have $fw \triangleleft_{B} M'N$ . Since $M \to^* M'$ , we have $MN \to^* M'N$ . By the induction hypothesis (1), we have $fw \triangleleft_{B} MN$ . This means $f \triangleleft_{A \to B} M$ .
In case $A \rightsquigarrow B$ . Suppose $M \to^* M'$ and $a \triangleleft_{A \rightsquigarrow B} M'$ . We have $M \to^* M' \to^* \lambda^{\bullet} x : A . P$ and $(w \triangleleft_{A} N \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M' \bullet N)$ for any N and w. Given N and w with $w \triangleleft_{A} N$ , we have $\mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M' \bullet N$ . Since $M \to^* M'$ , we have $M \bullet N \to^* M' \bullet N$ . By (3), we have $\mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M \bullet N$ . This means $a \triangleleft_{A \rightsquigarrow B} M$ .
(2). Note that we can show that $M' \to^* V$ if $M \to^* V$ and $M \to^* M'$ .
In case Unit. Suppose $M \to^* M'$ and $v \triangleleft_{\mathrm{Unit}} M$ . We have $v = \star$ and $M \to^* \mathtt{\langle\rangle}$ by the definition of $\triangleleft_{\mathrm{Unit}}$ . Hence, we have $M' \to^* \mathtt{\langle\rangle}$ , which means $v \triangleleft_{\mathrm{Unit}} M'$ .
In case $A_1 \times A_2$ . Suppose $M \to^* M'$ and $v \triangleleft_{A_1 \times A_2} M$ . We have $M \to^* \langle {V_1}, {V_2} \rangle$ , $\pi_1(v) \triangleleft_{A_1} V_1$ and $\pi_2(v) \triangleleft_{A_2} V_2$ . This means $v \triangleleft_{A_1 \times A_2} M$ since we have $M' \to^* \langle {V_1}, {V_2} \rangle$ .
In case $A \to B$ . Suppose $M \to^* M'$ and $f \triangleleft_{A \to B} M$ . We have $M \to^* \lambda x : A . M''$ and $(w \triangleleft_{A} N \implies fw \triangleleft_{B} MN)$ for any N and w. Given N and w with $w \triangleleft_{A} N$ , we have $fw \triangleleft_{B} MN$ . Since $M \to^* M'$ , we have $MN \to^* M'N$ . By the induction hypothesis (2), we have $fw \triangleleft_{B} M'N$ . This means $f \triangleleft_{A \to B} M'$ .
In case $A \rightsquigarrow B$ . Suppose $M \to^* M'$ and $a \triangleleft_{A \rightsquigarrow B} M$ . We have $M \to^* \lambda^{\bullet} x : A . P$ and $(w \triangleleft_{A} N \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M \bullet N)$ for any N and w. Given N and w with $w \triangleleft_{A} N$ , we have $\mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M \bullet N$ . Since $M \to^* M'$ , we have $M \bullet N \to^* M' \bullet N$ . By (4), we have $\mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} a \blacktriangleleft_{B} M' \bullet N$ . This means $a \triangleleft_{A \rightsquigarrow B} M'$ .
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. 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. 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 The proof is done by induction on the derivation of $\Gamma \vdash M : A$ and . Suppose that $\Gamma = x_1 : A_1, \dots, x_m : A_m$ and $\Delta = y_1 : B_1, \dots, y_n : B_n$ , $V_i$ is a value and $v_i \in \mathord{\left[\![{A_i}\right]\!]}$ with $v_i \triangleleft_{A_i} V_i$ for each $i \in \{ 1 , \dots , m\}$ , and $W_j$ is a value and $w_j \in \mathord{\left[\![{B_j}\right]\!]}$ with $w_j \triangleleft_{B_j} W_j$ for each $j \in \{ 1 , \dots , n\}$ .
-
(1) The case is proved in the main text, and the other cases are proved straightforwardly by the definition of $\triangleleft_A$ .
-
(2) In case . The derivation is
\begin{equation*} \mathord{\left[\![{M}\right]\!]}(v_1, \dots, v_m, w_1, \dots, w_n) \triangleleft_A M[V_1 / x_1 , \dots, V_m / x_m, W_1 / y_1, \dots , W_n / y_n]. \end{equation*}By the definition of $\triangleleft_A$ , there exists a value $\vdash V : A$ such that\begin{align*} & \mathop{\mathrm{arr}}\nolimits(\langle w_1, \dots, w_n \rangle) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{\lfloor{M}\rfloor}\right]\!]}(v_1, \dots, v_m) \\ & \blacktriangleleft_A \lfloor{M}\rfloor[V_1 / x_1 , \dots, V_m / x_m, W_1 / y_1, \dots , W_n / y_n]. \end{align*}
In case . The derivation is
By the induction hypothesis, we have
By the definition of $\triangleleft_{A \rightsquigarrow B}$ , we have
We also have
and
Therefore, we have
In case . The derivation is
By the induction hypothesis, we have
By the definition of $\triangleleft_{\delta}$ , there exists a value U such that
From (D1), (D2), and Lemma 5.15(1), we have
We have
for the trivial context $\mathcal{F} = [{-}]$ , and
If $w \triangleleft_{\delta} W$ then $\mathop{\mathrm{arr}}\nolimits(w) \blacktriangleleft_{\delta} \lfloor{W}\rfloor = \mathcal{F}[\lfloor{W}\rfloor]$ . Therefore, by the definition of $\blacktriangleleft_{\delta}$ , we have
In case . The derivation is
Let $P' = P[V_1 / x_1, \dots, V_m / x_m, W_1 / y_1, \dots, W_n / y_n]$ and $Q' = Q[V_1 / x_1, \dots, V_m / x_m, W_1 / y_1, \dots, W_n / y_n]$ . By the induction hypothesis, we have
and
for any $u \in \mathord{\left[\![{B}\right]\!]}$ and a value U with $u \triangleleft_{B} U$ . By the definition of $\blacktriangleleft_{A}$ , there are two cases.
Case $P' \to^* \lfloor{U}\rfloor$ for a value U and there exists $u \in \mathord{\left[\![{B}\right]\!]}$ such that $\mathop{\mathrm{arr}}\nolimits(w_1, \dots, w_n) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}(v_1, \dots, v_m) = \mathop{\mathrm{arr}}\nolimits(u)$ and $u \triangleleft_B U$ . We have
and
where $\vec{w} = \langle w_1, \dots, w_n \rangle$ . Hence, by Lemma 5.15(3), we obtain
Case $P' \to^* \mathcal{F}[\mathsf{op}(U)]$ for a value U and and there exists $u \in \mathord{\left[\![{\gamma}\right]\!]}$ with $u \triangleleft_{\gamma} U$ and $b \in \mathcal{A}_{\Sigma}(\mathord{\left[\![{\delta}\right]\!]}, \mathord{\left[\![{A}\right]\!]})$ such that $\mathop{\mathrm{arr}}\nolimits(\langle w_1, \dots, w_n \rangle) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{P}\right]\!]}(v_1, \dots, v_m) = \mathop{\mathrm{arr}}\nolimits(u) \mathrel{>\!\!>\!\!>} \mathsf{op} \mathrel{>\!\!>\!\!>} b$ and $w \triangleleft_{\delta} W \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} b \blacktriangleleft_{A} \mathcal{F}[\lfloor{W}\rfloor]$ for any $w \in \mathord{\left[\![{\delta}\right]\!]}$ and a value W. We have
where $\mathcal{F}' = \mathop{\mathbf{let}} y \Leftarrow \mathcal{F} \mathop{\mathbf{in}} Q'$ , and
where $\vec{w} = \langle w_1, \dots, w_n \rangle$ , $\vec{v} = \langle v_1, \dots, v_m \rangle$ and $b' = \mathop{\mathrm{arr}}\nolimits(\lambda x . \langle x, \vec{w} \rangle) \mathrel{>\!\!>\!\!>} \mathop{\mathrm{first}}\nolimits(b) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{Q}\right]\!]}(\vec{v})$ . Given $w \in \mathord{\left[\![{\delta}\right]\!]}$ and $\diamond \vdash W : \delta$ with $w \triangleleft_{\delta} W$ , we can show $\mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} b' \blacktriangleleft_{B} \mathcal{F}'[\lfloor{W}\rfloor]$ . Therefore, we have
In case . The derivation is
where . Let $R' = R[V_1 / x_1, \dots, V_m / x_m, W_1 / y_1, \dots, W_n / y_n]$ . By the induction hypothesis, we have
By the definition of $\blacktriangleleft_{C}$ , there are two cases.
Case $R' \to^* \lfloor{U}\rfloor$ for a value U and there exists $u \in \mathord{\left[\![{C}\right]\!]}$ such that $\mathop{\mathrm{arr}}\nolimits(\langle w_1, \dots, w_n \rangle) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{R}\right]\!]}(v_1, \dots, v_m) = \mathop{\mathrm{arr}}\nolimits(u)$ and $u \triangleleft_{C} U$ . By the induction hypothesis and $u \triangleleft_{C} U$ , we have
We have
and
Therefore, by Lemma 5.15(3), we obtain
Case $R' \to^* \mathcal{F}[\mathsf{op}(U)]$ for a value U and and there exist $u \in \mathord{\left[\![{\gamma}\right]\!]}$ with $u \triangleleft_{\gamma} U$ and $b \in \mathcal{A}_{\Sigma}(\mathord{\left[\![{\delta}\right]\!]}, \mathord{\left[\![{C}\right]\!]})$ such that $\mathop{\mathrm{arr}}\nolimits(\langle w_1, \dots, w_n \rangle) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{R}\right]\!]}(v_1, \dots, v_m) = \mathop{\mathrm{arr}}\nolimits(u) \mathrel{>\!\!>\!\!>} \mathsf{op} \mathrel{>\!\!>\!\!>} b$ and $w \triangleleft_{\delta} W \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} b \blacktriangleleft_{C} \mathcal{F}[\lfloor{W}\rfloor]$ for any $w \in \mathord{\left[\![{\delta}\right]\!]}$ and $\diamond \vdash W : \delta$ . Let $Q_{\mathsf{op}}' = Q_{\mathsf{op}}[U / z, (\lambda^{\bullet} y . \mathop{\mathbf{handle}} \mathcal{F}[\lfloor{y}\rfloor] \mathop{\mathbf{with}} H) / k]$ . We have
By the induction hypothesis and $u \triangleleft_{\gamma} U$ , we have $\mathop{\mathrm{arr}}\nolimits(u) \mathrel{>\!\!>\!\!>} \mathord{\left[\![{Q_{\mathsf{op}}}\right]\!]}( \kappa ) \blacktriangleleft_{D} Q_{\mathsf{op}}'$ for any $\kappa \in \mathord{\left[\![{\delta \rightsquigarrow D}\right]\!]}$ with $\kappa \triangleleft_{\delta \rightsquigarrow D} (\lambda^{\bullet} y . \mathop{\mathbf{handle}} \mathcal{F}[\lfloor{y}\rfloor] \mathop{\mathbf{with}} H)$ . We can show $\mathord{\left[\![{H}\right]\!]}(b) \triangleleft_{\delta \rightsquigarrow D} \lambda^{\bullet} y . \mathop{\mathbf{handle}} \mathcal{F}[\lfloor{y}\rfloor] \mathop{\mathbf{with}} H$ from $\forall w.\ \forall W.\ w \triangleleft_{\delta} W \implies \mathop{\mathrm{arr}}\nolimits(w) \mathrel{>\!\!>\!\!>} b \blacktriangleleft_{C} \mathcal{F}[\lfloor{W}\rfloor]$ . Thus, we have
By Lemma 5.15(3), we obtain
E Proofs for Section 6 (Related work)
Proposition 6.1. There is a map
for any set D.
Proof. By the following calculation:
where $\phi \colon \mathcal{A}(\mathord{\left[\![{\gamma}\right]\!]} \times (\mathord{\left[\![{\delta}\right]\!]} \Rightarrow \mathord{\left[\![{\delta}\right]\!]}), D) \to \mathcal{A}(\mathord{\left[\![{\gamma}\right]\!]}, D)$ is defined as
Discussions
No Discussions have been published for this article.