Equational Theories and Monads from Polynomial Cayley Representations
Abstract
We generalise Cayley’s theorem for monoids by providing an explicit formula for a (multisorted) equational theory represented by the type \(PX \rightarrow X\), where \(P\) is an arbitrary polynomial endofunctor with natural coefficients. From the computational perspective, examples of effects given by such theories include backtracking nondeterminism (obtained with the original Cayley representation \(X \rightarrow X\)), finite mutable state (obtained with \(n \rightarrow X\), for a constant n), and their different combinations (via \(n \times X \rightarrow X\) or \(X^n \rightarrow X\)). Moreover, we show that monads induced by such theories are implementable using the type formers available in programming languages based on a polymorphic \(\lambda \)calculus, both as compositions of algebraic datatypes and as continuationlike monads. We give a settheoretic model of the latter in terms of Barrdinatural transformations. We also introduce CayMon, a tool that takes a polynomial as an input and generates the corresponding equational theory together with the two implementations of the induced monad in Haskell.
1 Introduction
The relationship between universal algebra and monads has been studied at least since Linton [13] and Eilenberg and Moore [4], while the relationship between monads and the general theory of computational effects (exceptions, mutable state, nondeterminism, and such) has been observed by Moggi [14]. By transitivity, one can study computational effects using concepts from universal algebra, which is the main theme of Plotkin and Power’s prolific research programme (see [10, 20, 21, 22, 23, 24] among many others).
This suggests a simple recipe for computational effects: it is enough to come up with an equational theory, and out of the hat comes the induced monad of free algebras that implements the corresponding effect. Such an approach is indeed possible in the category \(\mathbf {Set}\), where every finitary equational theory admits a free monad, constructed by quotienting terms over the signature by the congruence induced by the equations. However, if we want to implement this monad in a programming language, the situation is not so simple, since in most programming languages (in particular, those without higher inductive types) we cannot generally express this kind of quotients. For instance, to describe a variant of nondeterminism that does not admit duplicate results, we may extend the theory of monoids with an equation stating that \(\gamma \) is idempotent, that is, \(\gamma (x,x) = x\). But, unlike in the case of general monoids, the monad induced by the theory of idempotent monoids seems to be no longer directly expressible in, say, Haskell. This means that there is no implementation that satisfies all the equations of the theory “on the nose”—one informal argument is that the representations of \(\gamma (x,x)\) and x should be the same whatever the type of x, and this would require a decidable equality test on every type, which is not possible.
Thus, both from the practical viewpoint of programming and as a question on the general nature of equational theories, it makes sense to ask which theories are “simple” enough to induce monads expressible using only the basic type formers, such as (co)products, function spaces, algebraic datatypes, universal and existential quantification. This question seems difficult in general, and to our knowledge there is little work that addresses it. In this paper, we focus on a small piece of this problem: we study a certain subset of such implementable equational theories, and conjure some novel extensions.
In Sect. 4, we give the formula that defines an equational theory given a polynomial functor \(P\). In general, the theories we construct can be multisorted, which is useful for avoiding a combinatory explosion of the induced theories, hence a brief discussion of such theories in Sect. 3. We show that \(PX \rightarrow X\) is indeed a tight representation of the generated theory. Then, in Sect. 5, we study a number of examples in order to discover what effects are denoted by the generated theories. It turns out that each theory can be seen as a (rather complex, for nontrivial polynomial functors) composition of backtracking nondeterminism and finite mutable state. Moreover, in Sect. 6, we show that the corresponding monads can be implemented not only as continuationlike monads (1), but also in “direct style”, using algebraic datatypes.
Since they are parametrised by a polynomial, both the equational theory and its representation consist of many indexed components, so it is not necessarily trivial to get much intuition simply by looking at the formulas. To facilitate this, we have implemented a tool, called CayMon, that generates the theory from a given polynomial, and produces two implementations in Haskell: as a composition of algebraic datatypes and as a continuationlike (“Cayley”) monad (1). The tool can be run in a web browser, and is available at http://pluwr.bitbucket.io/caymon.
2 Tight Cayley Representations
In this section, we take a more abstract view on the concept of “Cayley representation”. In the literature (for example, [2, 5, 17, 25]), authors usually define Cayley representations of different forms of algebraic structures in terms of embeddings. This means that given an object X, there is a homomorphism \(\sigma : X \rightarrow Y\) to a different object Y, and moreover \(\sigma \) has a retraction (not necessarily a homomorphism) \(\rho : Y \rightarrow X\) (meaning \(\rho \cdot \sigma = \mathsf {id}\)). One important fact, which is usually left implicit, is that the construction of Y from X is in some sense functorial. Since we are interested in coming up with representations for many different equational theories, we first identify sufficient properties of such a representation needed to carry out the construction of the monad (2) sketched in the introduction. In particular, we introduce the notion of tight Cayley representation, which characterises the functoriality and naturality conditions for the components of the representation.
As for notation, we use \(A \rightarrow B\) to denote both the type of a morphism in a category, and the set of all functions from A to B (the exponential object in \(\mathbf {Set}\)). Also, for brevity, we write the application of a bifunctor to two arguments, e.g., G(X, Y), without parentheses, as GXY. We begin with the following definition:
Definition 1
An important property of Barrdinaturality is that the componentwise composition gives a wellbehaved notion of vertical composition of two such transformations. The connection between Barrdinatural transformations and Cayley representations is suggested by the fact, shown by Paré and Román [16], that the collection of such transformations of type \(H \rightarrow H\) for the \(\mathbf {Set}\)bifunctor \(H(X,Y) = X \rightarrow Y\) is isomorphic to the set of natural numbers. The latter, equipped with addition and zero (or the former with composition and the identity transformation, respectively), is simply the free monoid with a single generator, that is, an instance of (1) with \(PX = X\) and \(A = 1\).
For the remainder of this section, assume that \(\mathscr {T}\) is a category, while \(F : \mathbf {Set}\rightarrow \mathscr {T}\) is a functor with a right adjoint \(U : \mathscr {T} \rightarrow \mathbf {Set}\). Intuitively, \(\mathscr {T}\) is a category of algebras of some theory, and U is the forgetful functor. Then, the monad generated by the theory is given by the composition UF. For a function \(f : A \rightarrow UX\), we write \(\widehat{f} = U f' : UFA \rightarrow UX\), where \(f' : FA \rightarrow X\) is the contraposition of f via the adjunction (intuitively, the unique homomorphism induced by the freeness of the algebra FA).
Definition 2
 (a)
A bifunctor \(R: \mathbf {Set}^\mathsf {op}\times \mathbf {Set}\rightarrow \mathbf {Set}\),
 (b)
For each set X, an object \({\mathbb RX}\) in \(\mathscr {T}\), such that \(U{\mathbb RX}= {RX X}\),
 (c)For all sets A, X, Y and functions \(f_1 : A \rightarrow {RX X}\), \(f_2 : A \rightarrow {RY Y}\), \(g : X \rightarrow Y\), it is the case that
 (d)
For each object M in \(\mathscr {T}\), a morphism \(\sigma _M : M \rightarrow {\mathbb R(UM)}\) in \(\mathscr {T}\), such that \(U\sigma _M : UM \rightarrow {R(UM) (UM)}\) is Barrdinatural in M,
 (e)
A Barrdinatural transformation \(\rho _M : {R(UM) (UM)} \rightarrow UM\), such that \(\rho _M \cdot U\sigma _M = \mathsf {id}\),
 (f)For each set X, a set of indices \(I_X\) and a family of functions \(\mathsf {run}_{X,i} : {RX X} \rightarrow X\), where \(i \in I_X\), such that \({R({RX X}) \mathsf {run}_{X}}\) is a jointly monic family, and the following diagram commutes for all X and \(i \in I_X\):
Note that the condition (c) states that the objects \(\mathbb R\) are, in a sense, natural. Intuitively, understanding an object \({\mathbb RX}\) as an algebra, the condition states that the algebraic structure of \({\mathbb RX}\) does not really depend on the set X. The condition (f) may seem rather complicated: the intuition behind the technical formulation is that RXY behaves like a form of a function space (after all, we are interested in abstract Cayley representations), and \(\mathsf {run}_{X,i}\) is an application to an argument specified by i, as in the example below. In such a case, the joint monicity becomes the extensional equality of functions.
Example 3
Let us check how Cayley representation for monoids fits the definition above: (a) The bifunctor is \(RXY = X \rightarrow Y\). (b) The \(\mathscr {T}\)object for a monoid M is the monoid \(M \rightarrow M\) with \(\gamma (f,g) = f \circ g\) and \(\varepsilon = \mathsf {id}\). (c) Given some elements \(a,b, \ldots , c \in A\), we need to see that \(g \circ f_1(a) \circ f_1(b) \circ \cdots \circ f_1(c) = f_2(a) \circ f_2(b) \circ \cdots \circ f_2(c) \circ g\). Fortunately, the assumption, which in this case becomes \(g\circ f_1(a) = f_2(a) \circ g\) for all \(a \in A\), allows us to “commute” g from one side of the chain of function compositions to the other. (d) \(\sigma _M(a) = b \mapsto \gamma (a,b)\). It is easy to verify that it is a homomorphism. The Barrdinaturality condition: assuming \(f(m) = n\) for some \(m \in M\) and \(n \in N\), and a homomorphism \(f : M \rightarrow N\), it is the case that, omitting the U functor, \(RfN(\sigma _N(n)) = RfN(\sigma _N(f (m))) = b \mapsto \gamma (f(m),f(b)) = b \mapsto f(\gamma (m,b)) = RMf(\sigma _M(m))\), where the equalities can be explained respectively as: assumption in the definition of Barrdinaturality, unfolding definitions, homomorphism, unfolding definitions. (e) \(\rho _M(f) = f(\varepsilon )\). It is easy to show that it is Barrdinatural; note that we need to use the fact that \(\mathscr {T}\)morphisms (that is, monoid homomorphisms) preserve \(\varepsilon \). (f) We define \(I_X = X\), while \(\mathsf {run}_{X,i}(f) = f(i)\).
The first main result of this paper states that given a tight representation of \(\mathscr {T}\) with respect to \(F \dashv U\), the monad given by the composition UF can be alternatively defined using a continuationlike monad constructed with sets of Barrdinatural transformations:
Theorem 4
For a tight Cayley representation R with respect to \(F \dashv U\), elements of the set UFA are in 11 correspondence with Barrdinatural transformations of the type \((A \rightarrow {RX X}) \rightarrow {RX X}\). In particular, this means that the latter form a set. Moreover, this correspondence gives a monad isomorphism between UF and the evident continuationlike structure on (2), given by the unit \((\eta _A(a))_X(f) = f(a)\) and the Kleisli extension \((f^*(k))_X(g) = k_X(a \mapsto (f (a))_X(g))\).
We denote the set of all Barrdinatural transformations from the bifunctor \((X,Y) \mapsto A \rightarrow R XY\) to R as \(\forall X. (A \rightarrow {RX X}) \rightarrow {RX X}\). This gives us a monad similar in shape to the continuation monad, or, more generally, Kock’s codensity monad [12] embodied using the formula for right Kan extensions as ends. One important difference with the codensity monad (except, of course, the fact that we have bifunctors on the righthand sides of arrows) is that we use Barrdinatural transformations instead of the usual dinatural transformations [3]. Indeed, if we use ends instead of \(\forall \), the end \(\textstyle \int _X (A \rightarrow {RX X}) \rightarrow {RX X}\) is given as the collection of all dinatural transformations of the given shape. It is known, however, that even in the simple case when \(A = 1\) and \(RXY = X \rightarrow Y\), this collection is too big to be a set (see the discussion in [16]), hence such end does not exist.
3 Multisorted Equational Theories with a Main Sort
The equational theories that we generate in Sect. 4 are multisorted, which is useful for trimming down the combinatorial complexity of the result. This turns out to be, in our view, essential in understanding what computational effects they actually represent. In this section, we give a quick overview of what kind of equational theories we work with, and discuss the construction of their free algebras.
We need to discuss the free algebras here, since we want the freeness to be with respect to a forgetful functor to \(\mathbf {Set}\), rather than to the usual category of sorted sets; compare [26]. This is because we want the equational theories to generate monads on \(\mathbf {Set}\), as described in the previous section. In particular, we are interested in theories in which one of the sorts is chosen as the main one, and work with the functor that forgets not only the structure, but also the carriers of all the other sorts, only preserving the main one. Luckily, this functor can be factored as a composition of two forgetful functors, each with an obvious left adjoint.
4 Theories from Polynomial Cayley Representations
In this section, we introduce algebraic theories that are tightly Cayleyrepresented by \(PX \rightarrow X\) for a polynomial functor \(P\). Notationwise, whenever we write \(i \le k\) for a fixed \(k \in \mathbb N\), we mean that i is a natural number in the range \(1 , \ldots , k\), and use \([ x_i ]_{ i \le k }\) to denote a sequence \(x_1, \ldots , x_k\). The latter notation is used also in arguments of functions and operations, so \(f([ x_i ]_{ i \le k })\) means \(f(x_1, \ldots , x_k)\), while \(f(x,[ y_i ]_{ i \le k })\) means \(f(x, y_1, \ldots , y_k)\). We sometimes use double indexing; for example, by \(\textstyle \prod _{i=1}^{k}\prod _{j=1}^{t_i} X_{i,j} \rightarrow Y\) for some \([ t_i ]_{ i \le k }\), we mean the type \(X_{1,1} \times \cdots \times X_{1,t_1} \times \cdots \times X_{k,1} \times \cdots \times X_{k,t_k} \rightarrow Y\). This is matched by a doublenested notation in arguments, that is, \(f([ [ x_i^j ]_{ j \le t_i } ]_{ i \le k })\) means \(f(x_1^1 , \ldots , x_1^{t_1} , \ldots , x_k^1 , \ldots , x_k^{t_k})\). Also, whenever we want to repeat an argument ktimes, we write \([ x ]_{ k }\); for example, \(f([ x ]_{ 3 })\) means f(x, x, x). Because we use a lot of sub and superscripts as indices, we do not use the usual notation for exponentiation. This means that \(x^i\) always denotes some x at index i, while a kfold product of some type X, ordinarily denoted \(X^k\), is written as \(\textstyle \prod ^k X\). We use the \(\llbracket \text {} \rrbracket \) brackets to denote the interpretation of sorts and operations in an algebra (that is, a model of the theory). If the algebra is clear from the context, we skip the brackets in the interpretation of operations.
Definition 5
 Sorts:
 Operations:
 Equations:
Thus, in the theory \(\mathfrak T\), there is a main sort \(\varOmega \), which we think of as corresponding to the entire functor, and one sort \(K_i\) for each “monomial” \(\textstyle \prod ^{e_i}X\). Then, we can think of \(\varOmega \) as a tuple containing elements of each sort, where each sort \(K_i\) has exactly \(c_i\) occurrences. The fact that \(\varOmega \) is a tuple, which is witnessed by the \(\mathsf {cons}\) and \(\pi \) operations equipped with the standard equations for tupling and projections, is not too surprising—one should keep in mind that \(\mathfrak T\) is a theory represented by the type \(PX \rightarrow X\), which can be equivalently given as the product of function spaces \(c_i \times \textstyle \prod ^{e_i}X \rightarrow X\) for all \(i \le d\).
Each operation \(\gamma ^j_i\) can be used to compose an element of \(K_j\) and \(e_j\) elements of \(K_i\) to obtain an element of \(K_i\). The \(\varepsilon \) constants can be seen as selectors: in (beta\(\varepsilon \)), \(\varepsilon _j^k\) in the first argument of \(\gamma ^j_i\) selects the kth argument of the sort \(K_i\), while the (eta\(\varepsilon \)) equation states that composing a value of \(K_i\) with the successive selectors of \(K_i\) gives back the original value. The equation (assoc\(\gamma \)) states that the composition of values is associative in an appropriate sense. In Sect. 5, we provide a reading of the theory \(\mathfrak T\) as a specification of a computational effect for different choices of d, \(c_i\), and \(e_i\).
Remark 6
If it is the case that \(e_i = e_j\) for some \(i,j \le d\), then the sorts \(K_i\) and \(K_j\) are isomorphic. This means that in every algebra of such a theory, there is an isomorphism of sorts \(\varphi : \llbracket K_i \rrbracket \rightarrow \llbracket K_j \rrbracket \), given by \(\varphi (x) = \gamma _j^i(x,[ \varepsilon _j^k ]_{ k \le e_i })\). This suggests an alternative setting, in which instead of having a single \(c_i \times \prod ^{e_i}X\) comoponent, we can have \(c_i\) components of the shape \(\prod ^{e_i}X\). In such a setting, the equational theory \(\mathfrak T\) in Definition 5 would be slightly simpler—specifically, there would be no need for doubleindexing in the types of \(\mathsf {cons}\) and \(\pi \). On the downside, this would obfuscate the connection with computational effects described in Sect. 5 and some conjured extensions in Sect. 7.
The theory \(\mathfrak T\) has a tight Cayley representation using functions from \(P\), as detailed in the following theorem. This gives us the second main result of this paper: by Theorem 4, the theory \(\mathfrak T\) is the equational theory of the monad (1). The notation \(\mathsf {in}_i\) means the ith inclusion of the coproduct in the functor \(P\).
Theorem 7

The bifunctor \(RXY = PX \rightarrow Y\),
 For a set X, the following algebra:
 Carriers of sorts:$$\begin{aligned}&\llbracket \varOmega \rrbracket = RXX \\&\llbracket K_i \rrbracket = \textstyle \prod ^{e_i}X \rightarrow X \end{aligned}$$
 Interpretation of operations:$$\begin{aligned}&\llbracket \mathsf {cons} \rrbracket ([ [ f_k^j ]_{ j \le c_k } ]_{ k \le d })(\mathsf {in}_i(c,[ x_t ]_{ t\le e_i })) = f_i^c([ x_t ]_{ t\le e_i }) \\&\llbracket \pi _i^j \rrbracket (f)([ x_t ]_{ t \le e_i }) = f(\mathsf {in}_i(j,[ x_t ]_{ t \le e_i })) \\&\llbracket \varepsilon _i^j \rrbracket ([ x_t ]_{ t \le e_i }) = x_j \\&\llbracket \gamma _i^j \rrbracket (f,[ g_k ]_{ k \le e_j })([ x_t ]_{ t\le e_i }) = f([ g_k([ x_t ]_{ t\le e_i }) ]_{ k \le e_j }) \end{aligned}$$

 The homomorphism \(\sigma _M\) for the main sort and sorts \(K_i\):$$\begin{aligned}&\sigma ^\varOmega _M(m)(\mathsf {in}_i(c,[ x_t ]_{ t \le e_i })) = \mathsf {cons}([ [ \gamma _k^{i}(\pi _{i}^{c}(m),[ \pi _k^j(x_t) ]_{ t \le e_i }) ]_{ j \le e_k } ]_{ k \le d }) \\&\sigma ^i_M(s)([ x_t ]_{ t \le e_i }) = \mathsf {cons}([ [ \gamma _k^{i}(s,[ \pi _k^j(x_t) ]_{ t \le e_i }) ]_{ j \le e_k } ]_{ k \le d }) \end{aligned}$$
 The transformation \(\rho _M\):$$\begin{aligned}&\rho _M(f) = \mathsf {cons}([ [ \pi _k^j(f (\mathsf {in}_k (j, [ \mathsf {cons}([ w^f_r ]_{ r< k }, [ \varepsilon _k^t ]_{ c_k }, [ w^f_r ]_{ k < r \le d }) ]_{ t \le e_k }))) ]_{ j \le c_k } ]_{ k \le d }) \\&\quad \text {where } w^f_r = [ \pi _r^c( f(\mathsf {in}_r(c, [ \varepsilon _r^j ]_{ j \le e_r }))) ]_{ c \le c_r } \end{aligned}$$

The set of indices \(I_X = PX\) and the functions \(\mathsf {run}_{X,i}(f) = f(i)\).
In the representing algebra, it is the case that each \(\llbracket K_i \rrbracket \) represents one monomial, as mentioned in the description of \(\mathfrak T\), while \(\llbracket \varOmega \rrbracket \) is the appropriate tuple of representations of monomials, which is encoded as a single function from a coproduct (in our opinion, this encoding turns out to be much more readable on paper), while \(\mathsf {cons}\) and \(\pi \) are indeed given by tupling and projections. For each \(i \le d\), the function \(\varepsilon _i^j\) simply returns its jth argument, while \(\gamma \) is interpreted as the usual composition of multiargument functions.
Homomorphisms between multisorted algebras are defined as operationpreserving functions for each sort, so \(\sigma \) is defined for the sort \(\varOmega \) and for each sort \(K_i\). In general, the point of Cayley representations is to encode an element m of an algebra M using its possible behaviours with other elements of the algebra. It is no different here: for each sort \(K_i\) at the cth occurrence in the tuple, the function \(\sigma ^\varOmega \) packs (using \(\mathsf {cons}\)) all possible compositions (by means of \(\gamma \)) of values of \(K_i\) with the “components” of m (extracted using \(\pi \)). The same happens for each \(s \in \llbracket K_i \rrbracket \) in \(\sigma ^i_M(s)\), but there is no need to unpack s, as it is already a value of a single sort.
The transformation \(\rho _M\) is a bit more complicated. The argument f is, in general, a function from a coproduct to M, but we cannot simply apply f to one value \(\mathsf {in}_i(\ldots )\) for some sort \(K_i\), as we would obviously lose the information about the components in different sorts. This is why we need to apply f to all possible sorts with \(\varepsilon \) in the right place to ensure that we recover the original value. We extract the information about particular sorts from such values, and combine them using \(\mathsf {cons}\). Interestingly, the elements of \(w^f_r\) could actually be replaced by any expression of the appropriate sort that is preserved by homomorphisms, assuming that f is also preserved. This is needed to ensure that \(\rho \) is Barrdinatural (the fact that f is preserved by homomorphisms is exactly the assumption in the definition of Barrdinaturality). For example, if \(e_r > 0\) for some \(r \le d\), one can define \(w^f_r\) simply as \([ \varepsilon _r^j ]_{ c_r }\) for some \(j \le e_r\). The complicated expression in the definition of \(w^f_r\) is a way to produce values also for sorts \(K_r\) with \(e_r = 0\), which do not have any \(\varepsilon \) constants.
5 Effects Modeled by Polynomial Representations
Now we describe what kind of computational effects are captured by the theories introduced in the previous section. It turns out that they all are different compositions of finite mutable state and backtracking nondeterminism. These compositions include the two most basic ones: when the state is local for each nondeterministic branch, and when it is global to the entire computation.
In the following, if there is only one object of a given kind, we skip the indices. For example, if for some i, it is the case that \(e_i = 1\), we write \(\varepsilon _i\) instead of \(\varepsilon _i^1\). If \(d=1\), we skip the subscripts altogether.
5.1 Backtracking Nondeterminism via Monoids
5.2 Finite Mutable State
5.3 Backtracking with Local State
We obtain one way to combine nondeterminism with state using the functor \(PX = n \times X\), for \(n \in \mathbb N\), that is, \(d=1\), \(c_1 = n\) and \(e_1 = 1\). It has two sorts, \(\varOmega \) and \(K\), which play roles similar to those detailed in the previous section. However, this time \(K\) additionally has the structure of a monoid. This gives us the theory of backtracking with local state, which means that whenever we make a choice using the \(\gamma \) operation, the computations in each argument carry separate, noninterfering states. In particular, in a computation \(\gamma (x,y)\), both subcomputations x and y start with the same state, which is the initial state of the entire computation. This noninterference is guaranteed simply by the system of sorts: the arguments of \(\gamma \) are of the sort \(K\), which means that the stateful computations inside the arguments begin with \(\pi \), which sets a new state.
5.4 Backtracking with Global State
6 DirectStyle Implementation
7 Discussion
The idea for employing Cayley representations to explore implementations of monads induced by equational theories is inspired by Hinze [8], who suggested a connection between codensity monads, Church representation of lists, and the Cayley theorem for monoids. We note that Hinze’s discussion is informal, but he suggests using ends, which, as we discuss in Sect. 2, is not sound.
Most of related work follows one of two main paths: it either concentrates on algebraic explanation of monads already used in programming and semantics (for example, [11, 19, 23]), or on the general connection between different kinds of algebraic theories and computational effects, but without much interest in whether it leads to structures implementable in a programming language. Some exceptions are the construction of the sum of a theory and a free theory [9] or the sum of ideal monads [6]. What we propose in Sect. 4 is a form of a “functional combinatorics”: given a type, what kind of algebra describes the possible values?
As our approach veers off the main paths of the recent work on effects, there are many possible directions of future work. One interesting direction would be to generalise \(\mathbf {Set}\), the base category used throughout this paper, to more abstract categories. After all, we want to talk about structures definable only in terms of (co)products, exponentials, and quantifiers—which are all constructions whose universal properties are singled out and explored using (co)cartesian (or even monoidal) closed categories. However, the current development relies heavily on the particular properties of \(\mathbf {Set}\), such as extensional equality of functions, which appears in disguise in the condition (f) in Definition 2.
One can also try to extend the type used as a Cayley representation. For example, we could consider the polynomial \(P\) in (3) to range over the space of all sets, that is, allow the coefficients \(c_i\) to vary over sets rather than natural numbers. In the Cayley representation, it would be enough to consider functions from \(c_i\) in place of \(c_i\)fold products. We would immediately gain expressiveness, as the obtained state monad would no longer need to be defined only for a finite set of possible states. On the flip side, this would make the resulting theory infinitary – which, of course, is not uncommon in the field of algebraic treatment of computational effects. However, we decide to stick to the simplest possible setting in this paper, which greatly simplifies the presentation, but still gives us some novel observations, like the fact that the theory of finite state is simply the theory of 2sorted tuples in Sect. 5.2, or the novel theory of backtracking nondeterminism with global state in Sect. 5.4. Other future extensions that we believe are worth exploring include iterating the construction to obtain a from of a distributive tensor (compare Rivas et al.’s [25] “double” representation of nearsemirings) or quantifying over more variables, leading to less interaction between sorts.
Footnotes
 1.
Although one usually writes \(\gamma \) as an infix operation, we use a “functional” syntax, since, in the following, the arity of corresponding operations may vary.
Notes
Acknowledgements
We thank the reviewers for their insightful comments and suggestions.
Piotr Polesiuk was supported by the National Science Centre, Poland, under grant no. 2014/15/B/ST6/00619.
Filip Sieczkowski was supported by the National Science Centre, Poland, under grant no. 2016/23/D/ST6/01387.
References
 1.Bird, R.: Functional pearl: a program to solve Sudoku. J. Funct. Program. 16(6), 671–679 (2006). http://dx.doi.org/10.1017/S0956796806006058CrossRefGoogle Scholar
 2.Bloom, S.L., Ésik, Z., Manes, E.G.: A Cayley theorem for Boolean algebras. Am. Math. Monthly 97(9), 831–833 (1990). http://dx.doi.org/10.2307/2324751MathSciNetCrossRefGoogle Scholar
 3.Dubuc, E., Street, R.: Dinatural transformations. In: MacLane, S., et al. (eds.) Reports of the Midwest Category Seminar IV, pp. 126–137. Springer, Heidelberg (1970). https://doi.org/10.1007/BFb0060443CrossRefGoogle Scholar
 4.Eilenberg, S., Moore, J.C.: Adjoint functors and triples. Illinois J. Math. 9(3), 381–398 (1965). https://projecteuclid.org:443/euclid.ijm/1256068141MathSciNetCrossRefGoogle Scholar
 5.Ésik, Z.: A Cayley theorem for ternary algebras. Int. J. Algebra Comput. 8, 311–316 (1998)MathSciNetCrossRefGoogle Scholar
 6.Ghani, N., Uustalu, T.: Coproducts of ideal monads. ITA 38(4), 321–342 (2004). https://doi.org/10.1051/ita:2004016MathSciNetzbMATHGoogle Scholar
 7.Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, 19–21 September 2011, pp. 2–14. ACM (2011). http://doi.acm.org/10.1145/2034773.2034777
 8.Hinze, R.: Kan extensions for program optimisation Or: Art and Dan explain an old trick. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 324–362. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642311130_16CrossRefzbMATHGoogle Scholar
 9.Hyland, M., Plotkin, G.D., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013MathSciNetCrossRefGoogle Scholar
 10.Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. Electron. Notes Theor. Comput. Sci. 172, 437–458 (2007). https://doi.org/10.1016/j.entcs.2007.02.019MathSciNetCrossRefzbMATHGoogle Scholar
 11.Jaskelioff, M., Moggi, E.: Monad transformers as monoid transformers. Theor. Comput. Sci. 411(51–52), 4441–4466 (2010). https://doi.org/10.1016/j.tcs.2010.09.011MathSciNetCrossRefzbMATHGoogle Scholar
 12.Kock, A.: Continuous Yoneda representation of a small category (1966). Aarhus University preprint. http://home.math.au.dk/kock/CYRSC.pdf
 13.Linton, F.: Some aspects of equational categories. In: Eilenberg, S., Harrison, D.K., MacLane, S., Röhrl, H. (eds.) Proceedings of the Conference on Categorical Algebra, pp. 84–94. Springer, Heidelberg (1966). https://doi.org/10.1007/9783642999024_3CrossRefGoogle Scholar
 14.Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991). https://doi.org/10.1016/08905401(91)900524MathSciNetCrossRefzbMATHGoogle Scholar
 15.Mulry, P.S.: Strong monads, algebras and fixed points. London Mathematical Society Lecture Note Series, pp. 202–216. Cambridge University Press, New York (1992)zbMATHGoogle Scholar
 16.Paré, R., Román, L.: Dinatural numbers. J. Pure Appl. Algebra 128(1), 33–92 (1998). http://www.sciencedirect.com/science/article/pii/S0022404997000364MathSciNetCrossRefGoogle Scholar
 17.Piróg, M.: EilenbergMoore monoids and backtracking monad transformers. In: Atkey, R., Krishnaswami, N.R. (eds.) Proceedings of 6th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2016, Eindhoven, Netherlands, 8th April 2016. EPTCS, vol. 207, pp. 23–56 (2016). https://doi.org/10.4204/EPTCS.207.2
 18.Piróg, M., Schrijvers, T., Wu, N., Jaskelioff, M.: Syntax and semantics for operations with scopes. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS 2018, pp. 809–818. ACM, New York (2018). http://doi.acm.org/10.1145/3209108.3209166
 19.Piróg, M., Staton, S.: Backtracking with cut via a distributive law and leftzero monoids. J. Funct. Program. 27, e17 (2017). https://doi.org/10.1017/S0956796817000077MathSciNetCrossRefzbMATHGoogle Scholar
 20.Plotkin, G.: Adequacy for algebraic effects with state. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds.) CALCO 2005. LNCS, vol. 3629, pp. 51–51. Springer, Heidelberg (2005). https://doi.org/10.1007/11548133_3CrossRefGoogle Scholar
 21.Plotkin, G., Power, J.: Adequacy for algebraic effects. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001). https://doi.org/10.1007/3540453156_1CrossRefGoogle Scholar
 22.Plotkin, G.D., Power, J.: Semantics for algebraic operations. Electron. Notes Theor. Comput. Sci. 45, 332–345 (2001). https://doi.org/10.1016/S15710661(04)809708CrossRefzbMATHGoogle Scholar
 23.Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3540459316_24CrossRefzbMATHGoogle Scholar
 24.Plotkin, G.D., Power, J.: Computational effects and operations: an overview. Electron. Notes Theor. Comput. Sci. 73, 149–163 (2004). http://dx.doi.org/10.1016/j.entcs.2004.08.008CrossRefGoogle Scholar
 25.Rivas, E., Jaskelioff, M., Schrijvers, T.: From monoids to nearsemirings: the essence of MonadPlus and alternative. In: Falaschi, M., Albert, E. (eds.) Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, 14–16 July 2015. pp. 196–207. ACM (2015). http://doi.acm.org/10.1145/2790449.2790514
 26.Tarlecki, A.: Some nuances of manysorted universal algebra: a review. Bull. EATCS 104, 89–111 (2011)MathSciNetzbMATHGoogle Scholar
 27.Vene, V., Ghani, N., Johann, P., Uustalu, T.: Parametricity and strong dinaturality (2006). https://www.ioc.ee/~tarmo/tdayvoore/veneslides.pdf
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.