Category-Graded Algebraic Theories and Eﬀect Handlers

(1)

Category-Graded Algebraic Theories and Effect Handlers

Takahiro Sanada^1,2

Research Institute for Mathematical Sciences Kyoto University

Kyoto, Japan

Abstract

We provide an effect systemCatEff based on a category-graded extension of algebraic theories that correspond to category- graded monads. CatEff has category-graded operations and handlers. Effects inCatEff are graded by morphisms of the grading category. Grading morphisms represent fine structures of effects such as dependencies or sorts of states. Handlers inCatEff are regarded as an implementation of category-graded effects. We define the notion of category-graded algebraic theory to give semantics ofCatEff and prove soundness and adequacy. We also give an example using category-graded effects to express protocols for sending receiving typed data.

Keywords: Algebraic theory, algebraic effect, effect handler, category-graded monad

1 Introduction

1.1 Background

Moggi [14] usedmonads to capture computational effects. Monads have a close relationship withalgebraic theories [7]. Algebraic effects [17] are effects based on algebraic theories. Handlers of algebraic effects [18] provide clear ways to implement effects. Algebraic effects and handlers are useful notions to make programs with effects.

There are several extensions of monads [1,8,15,16]. These variations of monads enable us to reason about computational effects in more detail.

Parameterised monads [1] are monads with parameters which represent initial and terminal states of computational effects such as change of type of state. In an effect system based on parameterised monads, each computational term is graded by an object of a parameter categoryS. For example, we can capture the feature of mutable state of mutable type. To see this, let S be a discrete category whose objects are int and 1. The parameter indicates the type of state. We can construct computational terms, M with parameterintandN with parameter1. We can know that the computationsM and N have states of type int and 1 respectively. Let us consider lookup and update operations for this mutable state of mutable type. There are two lookup operations and four update operations lookup_int(),lookup₁(), update_int→1(V), update_1→int(V), update_int→int(V) and update_1→1(V). lookup_int() is an operation that

1 I would like to thank the people of computer science group at RIMS, especially Masahito Hasegawa and Soichiro Fujii for discussions and comments, and the anonymous reviewers for comments. This work was supported by JST, the establishment of university fellowships towards the creation of science technology innovation, Grant Number JPMJFS2123 and JST ERATO Grant Number JPMJER1603.

2 Email: tsanada@kurims.kyoto-u.ac.jp

(2)

reads the state of type int and returns the value in it. We can use lookup_int() only when the type of the state is int. lookup₁() is similar. update_α→β(V) is an operation that writes the valueV in the state changing the type of state fromαtoβ. The parameter categoryS does not need to be a discrete category.

IfShas nontrivial morphisms, the intuition is that morphisms mean subtyping relations between the types of the state.

Graded monads [8,12] are monads graded by a partially ordered monoid. Elements of the partially ordered monoid express quantity of effects such as memory locations that effects affect. Its formal theory was given in [5], and its algebraic theories were given in [20,4,9]. For example, let L ={l₁, l₂, . . . , l_n} be a set of memory locations. Then we can get a partially ordered monoid 2^L where the product · of 2^L is the union of sets∪ and the order ≤ of 2^L is the inclusion ⊆. If a computation term M is graded by A∈2^L, we can know thatM may access the memory locations contained in A. The role of the order is weakening of a set of locations which may be accessed. If a computation termM is graded by A∈2^Land A ≤B, we can deduce that M is also graded by B. The intuition is that computation that may access the locations inA may access the locations in B which is larger than A. Let us consider memory lookup and update operations. Let lookup_i() be an operation that reads location l_i and returns its value and update_j(V) be an operation that writes V on the location l_j and returns the unit value. lookup_i() and update_j(V) are graded by {l_i} and {l_j} respectively. If M is graded by A ∈ 2^L, letx ← lookup_i()inM andlet ←update_j(V)inM are graded by {l_i} ·A and{l_j} ·A, respectively.

Category-graded monads [15] are introduced to unify parameterised and graded monads. Graded monads are 2-category-graded monads with a single object. Parameterised monads are category-graded monads withgeneralised units. Category-graded monads and the constructions of these Eilenberg-Moore and Kleisli categories are a special case of lax functors and these two constructions are studied by Street [21].

1.2 Overview

In this paper, we provide

• category-graded extensions of algebraic theories,

• a category-graded effect systemCatEff with effect handlers based on category-graded algebraic theories, and

• operational and denotational semantics of the effect system.

In category-graded algebraic theories, terms are graded by morphisms of a grading category S. In the effect system that corresponds to category-graded algebraic theories, we will define a judgement Γ`_f M :A for computational termM and a morphismf inS. This judgement means that the computation M will return a value of type A under the environment Γ and invoke effects graded by f. The term M will be denoted by a map [[Γ]]→T_f[[A]], where T is a category-graded monad. Grading morphisms can express a finer structure of computational effects than elements of monoids in ordinary graded monads or parameters in parameterised monads can, especially structures of dependency and sorts of state.

For instance, let us consider the following morphisms f = (1 ^τ

1

−−→int int −−−−→^send^int int ^recv

int

−−−−→int int) and g= (1 ^recv

1

−−−−→int int−−−−→^send^int int) in a categoryS. A computational term M graded by f is a computation that behaves as follows.

(i) The type of the initial state is unit type 1.

(ii) Some effects are invoked in M and a value of type intis stored in the state. Thus, the type of state is changed from 1 toint. These effects are graded by τ_int¹ , which means internal computation with a change of types of the state.

(iii) An effect sending the value of the state to another process is invoked. It is graded bysend_int. The type of the state is not changed by the sending effect, so the domain and codomain ofsend_intare the same.

(iv) An effect receiving graded by recv^int_int is invoked. It receives a value of type int and stores it in the state. In this case, the types of state before receiving and after receiving are the same, but in general,

(3)

they may be changed.

A computational termN graded byg is a computation that behaves as follows.

(i) The type of the initial type is unit type1.

(ii) An effect graded by recv¹_int is invoked. It receives a value of typeintand stores it in the state. The type of state before receiving and the type of receiving value are different, so the type of state is changed from 1 toint.

(iii) An effect graded by sendint is invoked. It sends a value of the state.

Thanks to the grading morphisms, we can know the transition of the type of the state, and deduce that M and N can interact with each other and yield values. We think of morphisms in S as protocols of communication.

We can construct handlers of category-graded effects. As ordinary handlers are the morphisms induced by the universality of free models of algebraic theories, category-graded handlers are the morphisms induced by the universality of free models of category-graded algebraic theories. We can regard category-graded handlers as an implementation of category-graded effects. (Monoid-)graded monads without order and parameterised monads whose parameterising category is discrete are special category-graded monads, so we can get handlers for effects corresponding to these monads automatically.

Contents. In Section2, we introduce notations and review some categorical notions. In Section3, we define category-graded algebraic theory and describe the free construction for the theory. In Section4, we explain our effect system based on category-graded algebraic theory. We call the effect systemCatEff. The effect system has handlers of category-graded effects. In Section5 and Section6, we describe operational and denotational semantics of our effect system, respectively. In Section 7, we show the soundness and adequacy of the semantics.

2 Category-Graded Monads

We assume that readers are familiar with basic notions of category theory such as monads [11]. Throughout this paper, we use the following notations.

• LetCAT be the 2-category of all categories, functors and natural transformations.

• LetSet be the category of all sets and maps.

• For a category C, Id_C is the identity functor on C.

• For a category C, Endo(C) is the full 2-subcategory ofCAT whose 0-cell is onlyC.

• For a category C with finite and countable products and coproducts, an object C of C, and a finite or countable set X,C^X is the X-fold product of C, that is Q

x∈XC and X×C is the X-fold sum ofC, that is P

x∈XC.

2.1 Lax Functors and Category-Graded Monads

Category-graded monads are introduced by Orchard et al. [15]. In this section, we fix a categoryC and a small categoryS.

Definition 2.1 [Lax functor] LetCbe a 2-category. Alax functor F:S −−→^lax Cis a tupleF = (F, η^F, µ^F) where

• For each object aofS,F ais a 0-cell of C.

• For each morphism f:a→b ofS,F f:F a→F bis a 1-cell of C.

• For each object aofS,η^F_a : idF a⇒Fida is a 2-cell of C.

• For each morphism f:a→b and g:b→c ofS,µ^F_g,f:F g◦F f ⇒F(g◦f) is a 2-cell ofC

(4)

satisfying the following commutative diagrams:

F f F f ◦Fid_a Fid_b◦F f F f

F f η^F_a

η^F_bF f µ^F_f,ida

µ^F_id

b,f

F h◦F g◦F f F h◦F(g◦f)

F(h◦g)F f F(h◦g◦f)

F hµ^F_g,f

µ^F_h,gF f µ^F_h,g◦f

µ^F_h◦g,f

We callη^F and µ^F unit andmultiplication ofF respectively.

We use string diagrams [19] for diagrammatic reasoning. In string diagram, a region of a diagram represents a 0-cell of a 2-category, a string between two regions represents a 1-cell from the 0-cell of the left regions to the 0-cell of the right region, and a node on strings represents a 2-cells from the 1-cell of bottom strings to the 1-cell of top strings. We can depict unit and multiplication, and the axioms of lax functor by string diagrams as follows:

η_a^F = Fid_a

η_a^F

, µ^F_f,g =

F(g◦f)

F f F g µ^F_f,g

,

F f

= F f

F f

=

F f

,

F(h◦g◦f)

F f F g F h

=

F(h◦g◦f)

F f F g F h .

Definition 2.2 [Category-graded monads] A category-graded monad (or an S-graded monad) on C is a lax functorS^{op lax}−−→Endo(C). That is, an S-graded monad consists of mapping of objects and morphisms T:S^op →Endo(C) and families of natural transformationsηa: IdC ⇒T_id_a fora∈ S andµ_f,g:T_fTg ⇒T_f;g forf:a→b and g:b→c inS that make the following diagrams commute.

T_f T_id_aT_f

TfTid_b Tf ηaT_f

Tfηb µida,f

µf,idb

T_fT_gT_h T_fT_g;h

Tf;gTh Tf;g;h T_fµ_g,h

µf,gTh µf,g;h

µf;g,h

If S is the trivial category, that is the category with a single object and the identity morphism on it, S-graded monad is a usual monad [3]. If S is a category with single object and endomorphisms on it, the endomorphisms form a monoid and S-graded monad is a (monoid-)graded monad without order.

To consider parameterised monads as category-graded monads introduced in [15], we have to introduce generalised units, see [15].

2.2 Eilenberg-Moore Construction on Lax Functors

According to [21], there are two functors obtained from a lax functor. The two constructions correspond to Eilenberg-Moore and Kleisli construction on a monad, respectively. In this subsection, we review the Eilenberg-Moore construction on lax functors.

LetSbe a small category andF:S →CATbe a lax functor. The Eilenberg-Moore construction gives a functor ˆF:S →CAT.

(5)

Definition 2.3 For a lax functor F = (F, η^F, µ^F) :S → CAT, the functor ˆF: S → CAT is defined as follows:

• For an object a∈ObS, the category ˆF a is defined as follows.

· Objects are pairs (A, ξ) where A is a map which assigns to each morphism f:a → b of S an object A_f ∈ObF band ξ is a family of morphisms {ξ_f,g:F_fA_g →A_f◦g}_f,g such that the following diagrams commute:

A_f F_id_bA_f

A_f

η^F_bAf

ξidb,f

F_hF_gA_f F_hAg◦f

Fh◦gA_f Ah◦g◦f Fhξg,f

µ^F_h,gAf ξh,g◦f

ξh◦g,f

for each f:a→b,g:b→c,h:c→dinS.

· Morphisms areα: (A, h)→(A⁰, ξ⁰) whereα is a family of morphisms n

α_f:A_f →A⁰_f o

f such that the following diagram commutes:

FgAf FgA⁰_f

Ag◦f A⁰_g◦f

Fgαf

ξ_g,f ξ⁰_g,f

αg◦f

for each f:a→b,g:b→c.

• For a morphismf:a→b, a functor ˆF f: ˆF a→F bˆ is defined as follows:

· F fˆ assigns an object (B, ζ) := ( ˆF f)(A, ξ) of ˆF b to an object (A, ξ) of ˆF a where B_g = Ag◦f and ζ_h,g=ξh,g◦f forg:b→c,h:c→d.

· For a morphismα: (A, ξ)→(A⁰, ξ⁰) of ˆF a, a morphism

( ˆF f)α: ( ˆF f)(A, ξ)→( ˆF f)(A⁰, ξ⁰) is defined as (( ˆF f)α)_g =αg◦f forg:b→cinS.

SinceS-graded monadT:S^op →Endo(C) is a special case of lax functorS^op→CAT, the category of Eilenberg-Moore algebras ofS-graded monad T is obtained by the above construction.

Next, we describe an adjunction between F a and ˆF a fora∈ObS. A functor ˆJa:F a→F aˆ is defined as follows.

• For an object X ∈ObF a, ˆJaX := (A, ξ) ∈ Ob ˆF a where A_f = F_fX and ξ_g,f = µ^F_g,f,X:FgA_f → Ag◦f

forf:a→b,g:b→c inS.

• For a morphismx:X→Y inF a, ˆJax: ˆJaX →JˆaY is a family of ˆJax_f :=Ffx.

A functor ˆEa: ˆF a→F a is defined as follows.

• For an object (A, ξ)∈Ob ˆF a, ˆEa(A, ξ) :=Aida ∈F a.

• For a morphismα: (A, ξ)→(A⁰, ξ⁰) in ˆF a, ˆE_aα=α_id_a.

We will show that ˆJ is a left adjoint to ˆE. To do so, we construct a unit and a counit of the adjunction.

The unit ˆη_a: Id_{F a} ⇒ Eˆ_aJˆ_a is a natural transformation whose components are ˆη_a,X := η^F_X:X → F_id_aX.

The counit ˆε_a: ˆJ_aEˆ_a⇒Id_{F a}_ˆ is a natural transformation whose components are ˆ

ε_a,(A,ξ) :=ξ_(−),id_a:

F₍₋₎A_id_a,(µ^F_g,f,A_id

a)

g,f

→(A, ξ).

Proposition 2.4 The tuple( ˆJa,Eâ,ηâ,εâ) forms an adjunction.

(6)

Proof. Follows by definition. For detail, see [21]. 2 For a morphism f:a → b, let us calculate the functor Ê_bF fˆ Jâ:F a → F b. For an object X ∈ F a, we have Ê_bF fˆ Jˆ_a(X) = Ê_bF fˆ

F₍₋₎X,(µ^F_g,k,X)

g,k

= ˆE_b

F_(−)◦fX,(µ^F_g,k◦f,X)

g,k

=F_id_b_◦fX =F_fX. For a morphism x:X → Y, we have Ê_bF fˆ Jˆ_a(x) = Ê_bF fˆ (F−x) = Ê_b(F−◦fx) =F_id_b◦fx= F_fx. Therefore, we haveF_f = Ê_bF fˆ Jˆ_a.

2.3 A Lax Functor Induced by Adjunctions and a Functor

In Section2.2, a lax functorF:S →CATgives adjunctions and a functor. Conversely, we will show that adjunctions and a functor determine a lax functor. The construction of lax functor is a generalization of the construction [5,13] of lax M-action from an adjunction and a strict M-action whereM is a monoid.

Theorem 2.5 Given a functor G:S →CAT, a map F: ObS →ObCAT and adjunctions (Ja:F a→ Ga, E_a:Ga→F a, η_a, ε_a) for each a∈ObS, F is extended to a lax functor F:S →CAT.

Proof. For each morphism f:a→b ofS, we define F f :=Eb◦Gf ◦Ja:F a→F b. The unit η^F ofF is induced by the units of the adjunctions. For eacha∈ObS, we defineη_a^F :=ηa: IdF a⇒Fida.

F a Ga

F b Gb

Ja

F f Gf

Eb

=

JaGf E_b

J_aGf E_b ,

F a Ga

Ja

IdF a Gida=IdGa

Ea

ηa =

JaEa

id_{F a} ηa

The multiplicationµ^F ofF is induced by the counits of adjunctions. We defineµ^F_g,f =J_aε_bE_c:F g◦F f ⇒ F(g◦f) for each f:a→band g:b→cof S.

Ga Gb Gb Gc

F a F b F b F c

Gf

G(g◦f)

E_b

IdGb Gg

Ec

Ja

F f IdF b

J_b

F g

εb = εb

J_aG(g◦f)E_c

J_aGf E_b J_bGg E_c

We claim that (F, η^F, µ^F) is a lax functor. To show this claim, we have to show that the axioms of lax functors hold. The following equations of string diagrams imply the axioms hold.

J_aGf E_b J_bGg E_cJ_cGhE_d JaG(h◦g◦fE)_d

εb

ε_c

=

J_aGf E_b J_bGg E_cJ_cGhE_d JG(ha ◦g◦fE)_d

ε_b εc

(7)

J_a Gf E_b

J_aGf E_b η_a

ε_a =

J_aGf E_b

=

J_a Gf E_b

J_aGf E_b η_b ε_b

2 Corollary 2.6 Given a functor G: S^op → CAT, a category C and adjunctions (Ja:C →Ga, Ea:Ga→ C, η_a, εa) for each a∈ObS, there exists an S-graded monad T: S^op → Endo(C) such that T_f =E_bGf Ja

for each f:b→ain S.

3 Category-Graded Algebraic Theories

We explain category-graded extensions of algebraic theories. In this section, we fix a small categoryS and a categoryC with countable products.

3.1 Category-Graded Terms

In a category-graded algebraic theory, each term is graded by a morphism in a grading categoryS. This is analogous to parameterised and (monoid-)graded algebraic theories [1,9].

Definition 3.1 [Signature] An (S-graded) signature Σ is a set of symbols. For eachσ ∈Σ, countable or finite setsP and A, and a morphism f inS are assigned. σ ∈Σ is called an operation. P, A and f are called a parameter, arity and grade of σ, respectively. We write σ: P A;f for an operation σ whose parameter, arity and grade areP,A,f, respectively.

Definition 3.2 [Σ-term] Let X be a set. The set of Σ-terms TermΣ(f, X) for each f:b → a in S is defined recursively as follows.

a∈ObS x∈X e(a, x)∈TermΣ(ida, X)

p∈P σ:P A;f:c→b {t_i}_i∈A⊂Term_Σ(g:b→a, X) do(σ, p,{t_i}_i∈A)∈TermΣ(f;g, X)

We sometimes write do(σ, p, λi.ti) instead of do(σ, p,{t_i}_i∈A). Intuitively, do(σ, p, λi.ti) is the term that performs the operation σ with parameter p, binds the result to i, and invokes the continuation ti. Note that, whenAis the arity ofσ, the termdo(σ, p, λi.t_i) is a term that takes A-many terms{t_i}_i∈Aas arguments.

Definition 3.3 [Σ-model] Let Σ be a signature. A Σ-model I = (I,|−|^I) at a ∈ S is a pair of a map I: Q

b∈SS(b, a) → C and an interpretation |σ|^I_k: P × I(k)^A → I(f;k) for each operation σ:P A;f:c→b∈Σ and morphism k:b→ainS.

A homomorphism α: I → J between two Σ-models I and J at a is a family of morphisms {α_k:I(k)→J(k)}_k:_b→a such that for every operation σ: P A;f:b→c and morphism k: c → a, the following diagram commutes:

P ×I(k)^A P×J(k)^A

I(f;k) J(f;k)

P×α^A_k

|σ|^I_k |σ|^J_k

αf;k

The mapI :Q

bS(b, a)→ C assigns a “carrier set”I(k) to each k:b→a. Given a Σ-model I, we can interpret Σ-terms by extending the interpretation ofI.

(8)

Definition 3.4 [Interpretation of Σ-terms] Let Σ be a signature and I be a Σ-model at a ∈ ObS.

For each Σ-term t ∈ Term_Σ(f:b→a, X), the element |t|^I, called its interpretation, of the set Q

a⁰∈S,k∈S(a,a⁰)C(I(k)^X, I(f;k)) is defined recursively as

|e(a, x)|^I :={π_x:I(k)^X →I(k)}_k_:_a→a0,

|do(σ, p, λi.t_i)|Î :={(p× h|t_i|Î_ki_i∈A);|σ|Î_g;k:I(k)^X →I(f;g;k)}

k:a→a⁰

where (σ:P A;f :c→b)∈Σ andti ∈TermΣ(g:b→a, X).

Intuitively, grading morphisms are sequences of sorts of effects that will be invoked by executing terms.

Example 3.5 Category graded algebraic theories are useful to deal with “order-sensitive” operations. To illustrate this, we provide an example that contains operations for mutable state and sending and receiving data. In this example, grading morphisms represent orders of sending and receiving effect and types of data, analogously to session types. LetS be a category whose objects are base types and morphisms are generated byα ^recv

α

−−−→β β,α−^send−−−→^α α,α ^τ

α

−→β β,τγ^β◦τ_β^α=τ_γ^α, andτ_α^α= id_α. Let recvint_α:1 1;α−−→^recv int, sendint :1 1;int−−−→^send int, lookupint : 1 int;int−−−→^id^int int, updateint_α:int 1;α−→^τ int, and Σ be{recvint_α,updateint_α}_α∪ {sendint,lookupint}. We have the following Σ-terms:

t:=do(updateint,2, λ .do(sendint, ?, λ .do(recvintint, ?, λ .

do(lookupint, ?, λn.e(int, n)))))∈TermΣ(τ;sendint;recv^int_int,int), s:=do(recvint₁, ?, λ .do(lookupint, ?, λn.do(updateint, n+ 1, λ .

do(sendintint, ?, λ .e(int, ?)))))∈TermΣ(recv¹_int;sendint,1).

The termt is graded by the morphism 1−→^τ int−−−−→^send^int int ^recv

int

−−−−→int intin S. This means that the term t executes internal effect τ, sends data of type int, and then receives data of type int. The term s is graded by the morphism1 ^recv

1

−−−−→int int−−−−→^send^int int. This means that the termsreceives data of type int and then sends data of typeint. We can know from grading morphisms oft andsthat they can interact with each other.

3.2 Equations

Next, we introduce equations to represent the equational theory on terms. The equation is defined as a pair of terms as in the non-graded case. However, the pairs of terms must have the same grading morphism.

Definition 3.6 [Equations and category-graded algebraic theory] A graded family ofequations for Σ is a family of setsE = (E_f)_f where E_f is a set of pairs of terms in Term_Σ(f, X). We write t= s for a pair (t, s)∈ E_f. An S-graded algebraic theory is a pair T = (Σ, E) of S-graded signature Σ and equations E for Σ.

Definition 3.7 [Model for category-graded algebraic theory] Let T = (Σ, E) be an S-graded algebraic theory and a be an object of S. A model for T at a is a Σ-model I at a that satisfies |t|^I = |s|^I for each morphismf:c→b in S and equation t=s∈Ef. We denote the category of models for T ataby Mod^T_a(C).

3.3 Free Models and Adjunctions

We explain free models of a category-graded algebraic theory and its universal property.

Definition 3.8 Let T = (Σ, E) be an S-graded algebraic theory. We define a functor F_a^T : Set → Mod^T_a(Set) by (F_a^TX)(k) = TermΣ(k, X)/∼fork:b→ainS and|σ|^F_k^a^T^X(p,{[t_i]}_i∈A) = [do(σ, p, λi.ti)]

for each X ∈ Set, k:b → a in S and σ: P A;f where ∼ is the equivalence relation induced by

(9)

the equations E and [t] is the equivalence class of t. We also define a map η_X: X → (F_a^TX)(id_a) by η_X(x) = [e(a, x)]∈Term_Σ(id_a, X)/∼.

We can show that the modelF_a^TX withηX has the universal property of a free model.

Proposition 3.9 Let T = (Σ, E) be an S-graded algebraic theory. Given a model A in Set for T at a and a map φ:X →Aid_a, there exists a unique homomorphism φ:F_a^TX →A such thatφ_id_a◦η_X =φ.

X (F_a^TX)(ida)

Aid_a

ηX

φ φ_id_a

F_a^TX

A

φ

Proof. For each f:b → a, we define a map ˆφf: TermΣ(f, X) → Af from the set of Σ-terms to Af recursively by: ˆφ_id_a(e(a, x)) =φ(x) and ˆφ_f(do(σ, p, λi.ti)) = |σ|^A(p, λi.φ(tˆ i)). Since A is a model for T, all equations inEholds inA. Therefore, the mapφ([t]) := [ ˆφ(t)] is well-defined. We can showφ_id_a◦η_X =φ

by definition. 2

The forgetful functor for modelsU_a^T : Mod^T_a(Set)→Setis the evaluation at ida, that isU_a^T(A) =A_id_a. By the universality of the free construction, we have isomorphisms Mod^T_a(Set)(F_a^TX, A)∼=C(X, U_a^TA) for eacha∈ObS. Thus, we have adjunctionsF_a^T aU_a^T.

C Mod^T_a(Set)

F_a^T

U_a^T

a .

We can define Mod^T_k(Set) : Mod^T_a(Set) → Mod^T_b (Set) for a morphism k: b → a in S to make Mod^T₋(Set) a functorS^op →CAT. For a modelAin Mod^T_a(Set), a map Mod^T_k(Set)A: Q

cS(c, b)→Set is defined as (Mod^T_k(Set)A)(f) = A(f;k). Interpretation of operations |−|^Mod^T^k^(Set)A is defined as

|σ|^Mod

T k(Set)A

f =|σ|^A_f;k. It is easy to check that Mod^T_k(Set) is a functor from Mod^T_a(Set) to Mod^T_b (Set).

More generally, we can define a category of models Mod^T_a(C) for a category C in the same way as C=Set, and we can apply the same argument as above if the left adjoint of forgetful functor exists.

Applying Corollary2.6, we obtain anS-graded monadS^op →Endo(C). We denote the category-graded monad byT^T. The unit and multiplication ofT^T are depicted as follows.

η_a^T^T =

F_a^TU_a^T

IdC

, µ^T_g,f^T =

F_a^T

Mod^T_f_;g(C) U_c^T

F_a^T Mod^T_f(C)

U_b^TF_b^T Mod^T_g(C)

U_c^T .

4 A Category-Graded Effect System

In this section, we introduce an effect system with category-graded operations based on category-graded algebraic theories. We call the effect system CatEff. We also construct handlers of category-graded algebraic operations. We fix small categories S and S⁰, and S,S⁰-signatures Σ, Σ⁰.

(10)

4.1 Language

Syntax. Our effect system CatEff is based on fine-grained call-by-value calculus [10]. The syntax is divided into two parts, values and computations.

|projV ashx, yi.M |matchV{x.M₁;y.M₂}

whereais an object inS, andf is a morphism inS. Values are usual except for lambda abstraction. The lambda abstractionλ^fx :A.M means that this function has effects represented by the morphism f. We sometimes writeVΣ andMΣ to specify its signature.

Types. Types are defined by the following BNF:

P, Q::=1|P ×Q|P+Q, A, B::=1|A×B |A+B |A→B;a−→^f b.

where f: a → b is a morphism in S. The key idea is that a function type A → B;a −→^f b indicates that a function of this type consumes an argument of type A and returns a result of type B with effects represented byf. We callP aprimitive type. We assume that parameters and arities of operations in the signatures Σ and Σ⁰ are primitive types.

Typing rules. There are value judgements of the form Γ ` V : A and computation judgements of the form Γ `^Σ_f M :A where Γ is a list of distinct variables with types and f is a morphism in S. The judgement Γ`^Σ_f M :Ameans that the computationM returns a result of typeAunder type environment Γ and causes effects represented by f. We omit Σ in the judgement Γ `^Σ_f M : A if it is clear from the context. The typing rules for terms inCatEff are presented in Figure 1.

Values

Γ`?:1 Tv-Unit x:A∈Γ

Γ`x:A Tv-Var

Γ, x:A`_f M :B

Γ`λ^fx.M :A→B;f Tv-Abs Γ`V :A Γ`W :B

Γ` hV, Wi:A×B Tv-Pair Γ`V :A

Γ`inlV :A+B Tv-InjL Γ`V :B

Γ`inrV :A+B Tv-InjR Computations

Γ`V :A

Γ`_id_a valaV :A Tc-Val

Γ`V :P op :P Q;a−→^f b∈Σ

Γ`_f op(V) :Q Tc-Op Γ`_f_:a→bM :A Γ, x:A`_g:b→cN :B

Γ`_f;gletx←MinN :B Tc-Let Γ`V :A→B;f Γ`W :A

Γ`_f V W :B Tc-App Γ`V :A₁×A₂ Γ, x:A₁, y:A₂`_f M :B

Γ`_f projV ashx, yi.M :B Tc-Proj Γ`V :A₁+A₂ Γ, x:A₁ `_f M₁:B Γ, y :A₂ `_f M₂ :B

Γ`_f matchV{x.M₁;y.M₂}:B Tc-Match

Fig. 1. Typing rules.

(11)

4.2 Handlers

Handlers for ordinary algebraic theories [18] are homomorphisms from a free model for a theory to another one. We can also construct handlers for category-graded algebraic theories in a similar way to the ordinary handlers. Let G:S → S⁰ be a functor and T = (Σ, E), T⁰ = (Σ⁰, E⁰) be S-, and S⁰-graded algebraic theories, respectively. For an object a of S and sets X and Y, a handler from F_a^TX to (F_Ga^T⁰Y)(G−) is obtained by the universality of the free modelF_a^TX. To obtain the handler, (F_Ga^T⁰Y)(G−) must be a model forT ata. So we need the following data:

• a mapφ:X→(F_Ga^T⁰Y)(Gida), and

• interpretations |σ|^(F_k ^Ga^{T 0}^Y^)G:P×(F_Ga^T⁰Y)(Gk)^Q →(F_Ga^T⁰Y)(G(f;k)) of operations in Σ for every σ:P Q;c−→^f b∈Σ andk:b→a.

satisfying all equations in E, that is the interpretations of terms in Term_Σ(f, X) induced by |σ|^(F^Ga^{T 0}^Y^)G satisfies|t|^(F^Ga^{T 0}^Y^)G =|s|^(F^Ga^{T 0}^Y^)G for everyt=s∈E.

Together with the above data, (F_Ga^T⁰Y)(G−) becomes a model for T at a, and there is a homomorphism φ: F_a^TX → (F_Ga^T⁰Y)G such that φ_id_a ◦η_X = φ by the universal property of free model. We can calculate the homomorphism φ ={φ_l}_l_:_b→a as φ_id_a([e(a, v)]) = φ(v) and φ_l_:_b→a([do(σ, p, λi.t_i)]) =

|σ|^(F_k ^Ga^{T 0}^Y^)G(p, λi.φ_k([t_i])) wheret_i∈(F_Ga^T⁰Y)(Gk).

We add syntax and typing rules for handlers as follows. Note that the following constructions of handlers don’t care about equations of algebraic theories. Programmers must ensure on their responsibilities that handlers they are constructing respect proper equations of effects.

Additional syntax. To construct handlers for CatEff, we need data that corresponds to φ:X → (F_Ga^T⁰Y)(Gida) and|σ|^(F

T 0 GaY)G

k :P ×(F_Ga^T⁰Y)(Gk)^Q →(F_Ga^T⁰Y)(G(f;k)) as argued above. Thus, we extend the syntax ofCatEff as follows:

Computations M_Σ⁰ ::= · · · |handleMΣwithHΣ⇒Σ⁰

Handlers HΣ⇒Σ⁰ ::= {val_bx7→M_Σ⁰}

∪{op(p), r7→_k (M_Σ⁰)^k_op}^k:^c→b

op :P Q;d−→^g c∈Σ

Additional typing rules. We add a new judgement Γ`^G_b H:R⇒R⁰ whereR and R⁰ are primitive types. This means that the handlerH handles operations in computation of type R and then produces a computation of type R⁰. Let ∆ be an environment x₁ :P₁, . . . , x_n:P_n.

∆`^Σ_f_:_a→bM :R Γ`^G_b H :R⇒R⁰ ∆⊆Γ

Γ`^Σ_G(f⁰ ₎handleMwithH:R⁰ Tc-Handle Γ, x:R`^Σ_id⁰

Gb M :R⁰ n

Γ, p:P, r:Q→R⁰;Gk `^Σ_G(g;k)⁰ M_op^k :R⁰

ok:c→b

op :P Q;d−→^g c∈Σ

Γ`^G_b {val_bx7→M} ∪ {op(p), r7→_kM_op^k}^k_op∈Σ :R⇒R⁰ Th-Handler

Note that the environment ∆ contains only variables typed by primitive types. If it contained a type A → B;f, the morphism f is in S while the morphism must be in another grading category S⁰ after a computation graded byf is handled. This is impossible in general.

We omit the morphism k in op(p), r 7→_k M_op^k and write simply op(p), r 7→Mop when Mop =M_op^k for allk. This convention is used in Example 5.9.

(12)

S-App (λ^fx.M)V → M[V /x]

S-Let letx←val_aV inM → M[V /x]

S-Proj projhV₁, V₂iashx, yi.M → M[V₁/x, V₂/y]

S-MatchLeft match(inlV){x.M₁;y.M₂} →M₁[V /x]

S-MatchRight match(inrV){x.M₁;y.M2} →M2[V /y]

S-HandleRet handle(valaV)withH → M[V /x]

S-HandleOp handleE[op(V)]withH → N

S-Lift F[M]→ F[M⁰] ifM →M⁰ whereH={val_ax7→M} ∪ {op(p), r7→_kM_op^k }^k

op inS-HandleRetand S-HandleOp, and N =M_op^k^:^c→b[V /p, λ^Gky.handleE[val_by]withH/r] inS-HandleOp.

Fig. 2. Small-step operational semantics

5 Operational Semantics

To define the operational semantics ofCatEff, we need some auxiliary notions.

Definition 5.1 [Evaluation context] Evaluation contexts E and F are defined by the following BNF:

E_Σ ::= [ ]|letx← E_ΣinM_Σ

F_Σ⁰ ::= [ ]|letx← F_Σ⁰inM_Σ⁰ |handleF_ΣwithHΣ⇒Σ⁰

We write Γ ` F : A B;G(b⁰) −→^f a if Γ, x : A `_f F[val_b⁰x] : B is derived where G is a functor that corresponds to handlers inF and x does not appear inF as a free variable.

Figure 2 gives the small-step operational semantics for CatEff. It is based on [6]. The rules of operational semantics are usual except for S-HandleOp. InS-HandleOp, the grading morphism plays an important role. LetE beletx_n ←(. . .(letx₁←[ ]inM₁). . .)inM_n and f_i be the grading morphism ofM_i for eachi= 1, . . . , n. Consider a termhandleE[op(V)]withH. The handlerH handles op(V) with the termMop^f¹^;...;fⁿ in H. For example, see Example5.8.

The goal of the rest of this section is to show the progress lemma and the preservation lemma for CatEff. We start by proving the following lemmas by induction on derivations.

Lemma 5.2 (Substitution) If Γ, x₁ : A₁, . . . , x_n :A_n `_f M : B and Γ `V_i :A_i for each i= 1, . . . , n, thenΓ`_f M[V₁/x₁, . . . , V_n/x_n] :B.

Lemma 5.3 If Γ` F :A B;b−→^f a, Γ`_g⁰_:_c⁰_→b⁰ M :A, and G(b⁰) =b, then Γ`_G(g⁰_);f F[M] :B Lemma 5.4 If Γ`_hF[M] :B, then we have Γ`_g⁰ M :A and Γ` F :A B;f satisfying h=G(g⁰);f.

Lemma 5.5 (Progress) If `_f_:_b→aM :A then one of the following holds.

(i) f = ida andM =valaV for some value term V, (ii) M =E[op(V)] for some E, op and V, or

(iii) there exists a computation term N such that M →N.

Lemma 5.6 (Preservation) If `_f_:_b→aM :A and M →N then`_f N :B is derivable.

Together with the progress lemma(Lemma5.5) and preservation lemma(Lemma5.6), we have a safety theorem. The safety theorem says that if a computation term is well-typed then the term comes from value (valaV) or is about to perform an operation.

(13)

Theorem 5.7 (Safety) If `_f_:_b→a M : A is a terminating term then there exists a value term V such thatM =val_aV, or M calls an operation, that is M =E[op(V)]for some E, op∈Σand V.

Example 5.8 [Handler] We present an example of small-step evaluation with handlers. Let S be a category such that ObS = {c, d, e} and morphisms are identities and g:c → d and h: d → e, and S⁰ be a category such that ObS⁰ ={•} and the identity is the only morphism. There is a unique functor G:S → S⁰, which sends all objects inS to• inS⁰. LetS-signature Σ be{op₁:P A;g,op₂:Q B;h}

andS⁰-signature Σ⁰ be∅. Given terms

N =letx←op₁(V)in lety ←op₂(W)in val_ehx, yi, M_op^h

1 =rV⁰, M_op^id^e

2 =rW⁰, H ={val_ez7→val•z; op₁(p), r7→_h M_op^h

1; op₂(p), r7→_id_e M_op^id^e

2}

such that ` V : P, ` W : Q, ` V⁰ : A, ` W⁰ : B, `^Σ_g;h N : A×B and `^G_e H : A×B ⇒ A×B. By the handlerH, op₁ and op₂ are implemented as constant operations that always return values V⁰ and W⁰ for any arguments, respectively. By Tc-Handle, we have a judgement `^Σ_id⁰

• handleNwithH :A×B.

Therefore, the term handleNwithH is evaluated to the form val•U by the safety theorem. Indeed, handleNwithH is evaluated as follows:

handleNwithH

→(λ^Ghv.handle(letx←val_dvin lety←op₂(W)in valehx, yi)withH)V⁰

→^∗handle(lety←op₂(W)in val_ehV⁰, yi)withH

→M_op^h

2[W/p, λ^Gid^ew.handle lety←val_ewin val_ehV⁰, yiwithH/r]

= (λ^Gid^ew.handle lety←valewin valeha, yiwithH)W⁰ →^∗ val•hV⁰, W⁰i.

We have `^Σ_id⁰

• val•hV⁰, W⁰i:A×B.

Example 5.9 [Mutable store of mutable type with a plan] We can make a program with a mutable store of mutable type with a mutation plan. LetA and B be primitive types, V and W are value terms such that`V :A and`W :B. LetS be a category such that ObS={1, A, B}and morphisms are generated by f_β^α: α → β for α, β ∈ ObS and S⁰ be a category such that ObS⁰ ={1+ (A+B)} and morphism is only identity. There is a unique functor G: S → S⁰, which sends all objects in S to 1+ (A+B) in S⁰. Intuitively, objects are possible types of mutable store and morphisms are plans of mutations of types of the store. Let Σ be anS-signature {update^α_β}

α,β∈ObS∪ {lookup_α}_α∈Ob_S where the type of update^α_β ∈Σ is β 1;f_β^α:α→β and the type of lookup_α is 1 α; idα for each α, β ∈ ObS. Let Σ⁰ be an S⁰- signature {update,lookup} where the type of update is 1+ (A+B) 1; id and the type of lookup is 1 1+ (A+B); id.

We can implement the behavior of mutable types by the following handlers: H1 = {val₁x 7→

val_1+(A+B)inlx} ∪ Hop, HA = {val_Ax 7→ val_1+(A+B)inr(inlx)} ∪ Hop and HB = {val_Bx 7→

val_1+(A+B)inr(inrx)} ∪Hop where

Hop ={update¹₁( ), r7→let ←update(inl?)inr?

...

update^B_B(b), r7→let ←update(inr(inrb))inr?

lookup₁( ), r7→letx←lookup(?)in

matchx{inly.r?;inry.matchy{inla.r?;inrb.r?}}

lookup_A( ), r7→letx←lookup(?)in

matchx{inly.rV;inry.matchy{inla.ra;inrb.rV}}

lookup_B( ), r7→letx←lookup(?)in

matchx{inly.rW;inry.matchy{inla.rW;inrb.rb}}

(14)

We have judgements`^G_α H_α:α⇒1+ (A+B) for allα∈Ob (S). Let us consider the term N =let ←update¹_A(V)in let ←update^A_BWin letx←lookup_B(?)in val_Bx We have a judgement`^Σ

f_A¹;f_B^A N :B. The grading morphismf_A¹;f_B^A:1→A→B implies that the program N stores a value of typeAand then stores a value of typeB. Handling operations in Σ byH_B, a mutable store of mutable type with a plan is transformed to a mutable store of fixed type 1+ (A+B). We have

`^Σ_id⁰

1+(A+B) handleNwithH_B:1+ (A+B).

6 Denotational Semantics

In this section, we give denotational semantics for CatEff. The denotational semantics is based on [2].

Let Σ, Σ⁰ beS- and S⁰-signatures, respectively. For the sake of simplicity, we work in Set. To interpret computation terms that return a value in X, we use the sets Term_Σ(f:b→a, X) = U_bMod^Σ_f(Set)F_aX defined in section 3. We don’t care about equations and so consider free models without any equations.

Each computational term is interpreted by a term of a category-graded algebraic theory. We can think of elements of TermΣ(f:b→a, X) as trees whose leaves are labelled by elements of X, and internal nodes are labelled by operations and their arguments. For example, e(a, v) ∈ TermΣ(ida:a→a, X) is a tree with only one node labelled by v. Note that, for any tree t ∈ TermΣ(f, X), we obtain f by composing morphisms of label op of nodes in a path from the root to a leaf.

Definition 6.1 We define the interpretation of types [[A]]∈Set as follows:

[[1]] ={?}, [[A→B;b−→^f a]] = TermΣ(f,[[B]])^[[A]], [[A+B]] = [[A]]t[[B]], [[A×B]] = [[A]]×[[B]].

For a context Γ =x₁ :A₁, . . . , x_n:A_n, we define [[Γ]] = [[A₁]]× · · · ×[[A_n]].

We interpret value Γ ` V : A, computation Γ `_f M : A and handler Γ `^G_a H : R ⇒ R⁰ as maps [[Γ`V :A]] : [[Γ]] → [[A]], [[Γ`_f M :A]] : [[Γ]] → TermΣ(f,[[A]]) and [[Γ`^G_a H :R⇒R⁰]] : [[Γ]] → Term_Σ⁰(Gf ,[[R⁰]])^Term^Σ^(f,[[R]]), respectively. We write the lift of a morphism φ: X → TermΣ(g, Y) as φ^†^f :=µf,g(TermΣ(f, φ)) and often simply writeφ^† when f is clear from the context.

Definition 6.2 Let Γ be a typing context. Givens∈[[Γ]], we define the interpretation of terms as follows:

[[Γ`?:1]]s=?, [[Γ` hV₁, V₂i:A×B]]s=h[[V₁]]s,[[V₂]]si, [[Γ`inlV :A+B]]s= in₁[[V]]s, [[Γ`inrV :A+B]]s= in₂[[V]]s, [[Γ, x:A`x:A]]s=πx(s), [[Γ`λ^fx.M :A→B;f]]s= [[M]](s,−), [[Γ`_id_a valaV :A]]s=e(a,[[V]]s), [[Γ`_f V W :B]]s= ([[V]]s)([[W]]s),

[[Γ`_f op(V) :A]]s=do(op,[[V]]s,{e(a, x)}_x∈[[A]]), [[Γ`_f;gletx←MinN :B]]s= ([[N]](s,−))^†([[M]]s), [[Γ`_f projV ashx, yi.M :B]]s= [[M]](s, π₁([[V]]s), π₂([[V]]s)), [[Γ`_f matchV{x.y;M₁.M₂}:B]]s= [[[M₁]](s,−),[[M₂]](s,−)]([[V]]s),

[[Γ`^Σ_Gf⁰ handleMwithH :R⁰]]s= ([[H]]s)([[M]]s), [[Γ`^G_a H:R⇒R⁰]]s=

(e(a, v) 7→ [[M]](s, v)

do(op, p,{t_i}_i) 7→ [[M_op^k ]](s, p,{[[H]](s, t_i)}_i) whereH={val_ax7→M} ∪ {op(p), r7→M_op^k}^k_op∈Σ.

(15)

7 Soundness and Adequacy

We show soundness and adequacy. These theorems assert that operational semantics and denotational semantics are compatible with each other.

Theorem 7.1 (Soundness) If `_f M :A and M →M⁰ then[[`_f M :A]] = [[`_f M⁰:A]].

To show adequacy(Theorem7.5), we define relations A for values and ^f_A for computations as done in [2].

Definition 7.2 Forv∈[[A]] and a closed value term `V :A, we definevAV as follows:

• v1V ifv=1and V =?.

• vA×BV ifv=hv₁, v2i,V =hV₁, V2i,v1AV1 andv2BV2.

• vA+BV if either v= in₁v₁,V =inlV₁ and v₁AV₁, orv= in₂v₂,V =inrV₂ and v₂BV₂.

• vA→B;f V ifv(w)^f_BV W for each w∈[[A]] and closed value`W :Asatisfying wAW. Simultaneously, forc∈TermΣ(f,[[A]]) and a closed computation term `_f M :A,c^f_AM holds if

(i) f = ida,c= e(a, v),M →^∗valaV andvAV, or

(ii) c=do(σ, v,{t_x}_x∈[[C]]),M →^∗E[op(V)], vP V, and if wC W thentw^k_AE[val_bW].

Lemma 7.3 If c^f_AM⁰ and M →M⁰ then c^f_AM. Proof. By assumptionc^f_AM⁰, we have two cases:

(i) f = ida,c= e(a, v),M⁰ →^∗ valaV and vAV. In this case, we haveM →^∗ valaV.

(ii) c=do(σ, v,{t_x}_x∈[[C]]),M⁰→^∗E[op(V)], vP V, and ifwCW then tw^k_AE[val_bW]. In this case, we have M →^∗E[op(V)].

In both cases, we can concludec^f_AM as required. 2

Lemma 7.4 Let Γ be a typing context x₁ :A₁, . . . , x_n:A_n, and `W_i :A_i be a closed value term and w_i be an element of[[A_i]] withw_iAiW_i for each 1≤i≤n. Then followings hold.

(i) If Γ`V :A then[[V]](w₁, . . . , w_n)AV[W₁/x₁, . . . , W_n/x_n].

(ii) If Γ`_f M :A then [[M]](w₁, . . . , w_n)^f_AM[W₁/x₁, . . . , W_n/x_n].

Theorem 7.5 (Adequacy) If `_id_a M :1 and [[`_id_a M :1]] =e(a, ?) then M →^∗ val_a?.

Proof. By Lemma 7.4, we have [[M]]îd₁â M. Thus, we have e(a, ?) îd₁â M by assumption. By the definition ofîd₁â, we obtainM →^∗ val_aV and?1V. Therefore, by definition of1, we conclude V =?

andM →^∗ vala?. 2

8 Future Work

User-defined grading category and graded operations. The grading categories of CatEff are con- sidered to be built-in in this paper. To provide user-defined grading operations, the syntax to write grading categories and graded operations is needed. This is future work.

Category-graded Lawvere theories. Graded Lawvere theories which correspond to graded algebraic theories were developed in [9]. Category-graded extensions of Lawvere theories are future work.

2-category-graded monads. Graded monads are graded by partially ordered monoids in general.

We must consider2-category-graded monads, whose grading category is 2-category, to generalise partially ordered monoid-graded monads. This situation is beyond [21]. Thus, the Eilenberg-Moore and Kleisli constructions on these monads are not trivial.