# Container Combinatorics: Monads and Lax Monoidal Functors

Tarmo Uustalu

► To cite this version:

Tarmo Uustalu. Container Combinatorics: Monads and Lax Monoidal Functors. 2nd International Conference on Topics in Theoretical Computer Science (TTCS), Sep 2017, Tehran, Iran. pp.91-105, 10.1007/978-3-319-68953-1_8 . hal-01760638

HAL Id: hal-01760638

https://inria.hal.science/hal-01760638

Submitted on 6 Apr 2018

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Container Combinatorics:
Monads and Lax Monoidal Functors

Tarmo Uustalu

Dept. of Software Science, Tallinn University of Technology
Akadeemia tee 21B, 12618 Tallinn, Estonia,
*tarmo@cs.ioc.ee*

**Abstract.** Abbott et al.'s containers are a "syntax" for a wide class of set functors in terms of shapes and positions. Containers whose "denotation" carries a comonad structure can be characterized as directed containers, or containers where a shape and a position in it determine another shape, intuitively a subshape of this shape rooted by this position. In this paper, we develop similar explicit characterizations for container functors with a monad structure and container functors with a lax monoidal functor structure as well as some variations. We argue that this type of characterizations make a tool, e.g., for enumerating the monad structures or lax monoidal functors that some set functor admits. Such explorations are of interest, e.g., in the semantics of effectful functional programming languages.

# 1 Introduction

Abbott et al.'s containers [1], a notational variant of polynomials, are a "syntax" for a wide class of set functors. They specify set functors in terms of shapes and positions. The idea is that an element of $FX$ should be given by a choice of a shape and an element of $X$ for each of the positions in this shape; e.g., an element of $\text{List} X$ is given by a natural number (the length of the list) and a matching number of elements of $X$ (the contents of the list). Many constructions of set functors can be carried out on the level of containers, for example the product, coproduct of functors, composition and Day convolution of functors etc. One strength of containers is their usefulness for enumerating functors with specific structure or properties or with particular properties. It should be pointed out from the outset that containers are equivalent to simple polynomials in the sense of Gambino, Hyland and Kock [9,10,13,8], except that in works on polynomials one is often mainly interested in Cartesian polynomial morphisms whereas in works on containers general container morphisms are focussed on. The normal functors of Girard [11] are more constrained: a shape can only have finitely many positions.

Ahman et al. [3,4] sought to find a characterization of those containers whose interpretation carries a comonad structure in terms of some additional structure on the container, using that comonads are comonoids in the monoidal category of set functors. This additional structure, of what they called directed containers,
turned out to be very intuitive: every position in a shape determines another
shape, intuitively the subshape corresponding to this position; every shape has
a distinguished root position; and positions in a subshape can be translated
into positions in the shape. Directed containers are in fact the same as small
categories, yet directed container morphisms are not functors, but cofunctors in
the sense of Aguiar [2].

In this paper, we develop similar characterizations of container functors with a monad structure and those with a lax monoidal structure. We use that both monads and lax monoidal endofunctors are monoids in the category of set endofunctors wrt. its composition resp. Day convolution monoidal structures and that both monoidal structures are available also on the category of containers and preserved by interpretation into set functors. The relevant specializations of containers, which we here call mnd-containers and lmf-containers, are very similar, whereby every mnd-container turns out to also define an lmf-container.

Our motivation for this study is from programming language semantics and
functional programming. Strong monads are a generally accepted means for or-
ganizing effects in functional programming since Moggi’s seminal works. That
strong lax monoidal endofunctors have a similar application was noticed first
by McBride and Paterson [12] who called them applicative functors. That lax
monoidal functors are the same as monoids in the Day convolution monoidal
structure on the category of functors (under some assumptions guaranteeing
that this monoidal structure is present) was noticed in this context by Capriotti
and Kaposi [7]. It is sometimes of interest to find all monad or lax monoidal
functor structures that a particular functor admits. Containers are a good tool
for such explorations. We demonstrate this on a number of standard examples.

The paper is organized as follows. In Section 2, we review containers and directed containers as an explicit characterization of those containers whose interpretations carries a comonad structure. In Section 3, we analyze containers whose interpretation is a monad. In Section 4, we contrast this with an analysis of containers whose interpretation is a lax monoidal functor. In Section 5, we consider some specializations of monads and monoidal functors, to conclude in Section 6.

To describe our constructions on containers, we use type-theoretically in-
spired syntax, as we need dependent function and pair types throughout. For
conciseness of presentation, we work in an informal extensional type theory,
but everything we do can be formalized in intensional type theory. “Minor”
(“implicit”) arguments of functions are indicated as subscripts in II-types, λ-
abstractions and applications to enhance readability (cf. the standard notation
for components of natural transformations). We use pattern-matching lambda-
abstractions; _ is a “don’t care” pattern.

The paper is a write-up of material that was presented by the author at the
SSGEP 2015 summer school in Oxford<fnref n="1" />, but was not published until now.

<footnote n="1">¹ See the slides at http://cs.ioc.ee/~tarmo/ssgep15/.</footnote>
# 2 Containers, Directed Containers

## 2.1 Containers

We begin by a condensed review of containers [1].

A container is given by a set $S$ (of shapes) and a $S$-indexed family $P$ of sets (of positions in each shape).

A container morphism between two containers $(S, P)$ and $(S', P')$ is given by operations $t: S \to S'$ (the shape map) and $q: \Pi_{s:S}. P'(ts) \to Ps$ (the position map). Note that while the shape map goes in the forward direction, the position map for a given shape goes in the backward direction.

The identity container morphism on $(S, P)$ is $(\mathrm{id}_S, \lambda_s \cdot \mathrm{id}_{Ps})$. The composition of container morphisms $(t, q) : (S, P) \to (S', P')$ and $(t', q') : (S', P') \to (S'', P'')$ is $(t' \circ t, \lambda_s \cdot q_s \circ q_s)$.

A container $(S, P)$ interprets into a set functor $[[S, P]]^c = F$ where $FX = \Sigma s : S. Ps \to X, Ff = \lambda(s, v). (s, f \circ v)$.

A container morphism $(t, q)$ between containers $(S, P)$ and $(S', P')$ interprets into a natural transformation $[[t, q]]^c = \tau$ between $[[S, P]]^c$ and $[[S', P')]^c$ where $\tau(s, v) = (ts, v \circ q_s)$.

Interpretation $[[–]]^c$ is a fully-faithful functor from **Cont** to $[\mathbf{Set}, \mathbf{Set}]$.

For example, the list functor can be represented by the container $(S, P)$ where $S = \mathbb{N}$, because the shape of a list is a number—its length, and $Ps = [0..s)$, as a position in a list of length $s$ is a number between 0 and $s$, with the latter excluded. We have $[[S, P]]^c X = \Sigma s : \mathbb{N} [0..s) \to X \cong \mathrm{List} X$, reflecting that to give a list amounts to choosing a length together with the corresponding number of elements. The list reversal function is represented by the container endomorphism $(t, q)$ on $(S, P)$ where $ts = s$, because reversing a list yields an equally long list, and $q_s p = s - p$, as the element at position $p$ in the reversed list is the element at position $s - p$ in the given list. But the list selfAppend function is represented by $(t, q)$ where $ts = s + s$ and $q_s p = p \bmod s$.

There is an identity container defined by $\mathrm{id}^c = (1, \lambda* \cdot 1)$. Containers can be composed, composition is defined by $(S, P) \cdot^c (S', P') = (\Sigma s : S. Ps \to S', \lambda(s, v)). \Sigma p : Ps \cdot P'(vp)$). Identity and composition of containers provide a monoidal category structure on **Cont**.

Interpretation $[[–]]^c$ is a monoidal functor from $(\mathbf{Cont}, \mathrm{id}^c, \cdot^c)$ to the strict monoidal category $([\mathbf{Set}, \mathbf{Set}], \mathrm{id}, \cdot)$. Indeed, $\mathrm{id} X = X \cong \Sigma^* : 1 \cdot 1 \to X = [[\mathrm{id}]^c] X$ and $([S, P]^c \cdot [[S', P']^c] X) = [[S, P]^c ([[S', P']^c] X) \cong \Sigma s : S. Ps \to \Sigma s' : S'. P' s' \to X \cong \Sigma(s, v) : (\Sigma s : S. Ps \to S'). (\Sigma p : Ps \cdot P'(vp)) \to X = [[(S, P) \cdot^c (S', P')]^c X$.

Another monoidal category structure on **Cont** is symmetric. Define Handbook's tensor by $(S, P) \otimes^c (S', P') = (S \times S', \lambda(s, s'). Ps \times P's)$. Now $(\mathbf{Cont}, \mathrm{id}^c, \otimes^c)$ form a symmetric monoidal category.

Interpretation $[[–]]^c$ is a symmetric monoidal functor from $(\mathbf{Cont}, \mathrm{id}^c, \otimes^c)$ to the symmetric monoidal category $([\mathbf{Set}, \mathbf{Set}], \mathrm{id}, \otimes)$ where $\otimes$ is the Day convolutional category.
lution defined by $(F \otimes G)Z = \int^{X,Y}(X \times Y \to Z) \times (FX \times GY)$. Indeed,

$$ \begin{align*} & [[S, P]]^c \circled{\circ} [[S', P']^c Z \\ &= \int^{X,Y}(X \times Y \to Z) \times ((\Sigma s : S. P s \to X) \times (\Sigma s' : S'. P' s' \to Y)) \\ &\cong \Sigma(s, s') : S \times S'. \int^{X,Y}(X \times Y \to Z) \times ((P s \to X) \times (P' s' \to Y)) \\ &\cong \Sigma(s, s') : S \times S'. P s \times P' s' \to Z \\ &= [[(S, P) \circled{\circ} (S, P)]^c Z \end{align*} $$

## 2.2 Directed Containers

Next we review directed containers as a characterization those containers whose interpretation carries a comonad structure; we rely on [3,4].

A *directed container* is defined as a container $(S, P)$ with operations

- $\downarrow : \Pi s : S. P s \to S$ (the subshape corresponding to a position in a shape),

- $\circ : \Pi_{s:S} P s$ (the root position), and

- $\oplus : \Pi_{s:S} \Pi p : P s. P (s \downarrow p) \to P s$ (translation of a position in a position's subshape)

satisfying

- $s \downarrow \mathbf{o}_s = s$

- $s \downarrow (p \oplus_s p') = (s \downarrow p) \downarrow p'$

- $p \oplus_s \mathbf{o}_{s \downarrow p} = p$

- $\mathbf{o}_s \oplus_s p = p$

- $(p \oplus_s p') \oplus_s p'' = p \oplus_s (p' \oplus_{s \downarrow p} p'')$

The data $(\mathbf{o}, \oplus)$ resemble a monoid structure on $P$. However, $P$ is not a set, but a family of sets, and $\oplus$ operates across the family. Similarly, $\downarrow$ resembles a right action of $(P, \mathbf{o}, \oplus)$ on $S$. When none of $P s, \mathbf{o}_s, p \oplus_s p'$ depends on $s$, these data form a proper monoid structure and a right action.

A *directed container morphism* between two directed containers $(S, P, \downarrow, \mathbf{o}, \oplus)$ and $(S', P', \downarrow', \mathbf{o}', \oplus')$ is a morphism $(t, q)$ between the underlying containers satisfying

- $t(s \downarrow q_s p) = t s \downarrow' p$

- $\mathbf{o}_s = q_s \mathbf{o}'_{t s}$

- $q_s p \oplus_s q_{s \downarrow q_s p} p' = q_s (p \oplus'_{t s} p')$

Directed containers form a category **DCont** whose identities and composition are inherited from **Cont**.

A directed container $(S, P, \downarrow, \mathbf{o}, \oplus)$ interprets into a comonad $[[S, P, \downarrow, \mathbf{o}, \oplus]]^{\mathrm{dc}} = (D, \varepsilon, \delta)$ where

- $D = [[S, P]]^c$

- $\varepsilon(s, v) = v \circ \mathbf{o}_s$

- $\delta(s, v) = (s, \lambda p. (s \downarrow p, \lambda p'. v (p \oplus_s p')))$
A directed container morphism $(t, q)$ between $(S, P, \downarrow, \mathbf{o}, \oplus)$ and $(S', P', \downarrow', \mathbf{o}', \oplus')$ interprets into a comonad morphism $[[t, q]]^{\mathrm{dc}} = [[t, q]]^c$ between $[[S, P, \downarrow, \mathbf{o}, \oplus]]^{\mathrm{dc}}$ and $[[S', P', \downarrow', \mathbf{o}', \oplus']^{\mathrm{dc}}$.

$[[−]]^{\mathrm{dc}}$ is a fully-faithful functor between **DCont** and **Comonad**(Set). Moreover, the functor $[[−]]^{\mathrm{dc}}$ is the pullback of the fully-faithful functor $[[−]]^c : \mathbf{Cont} \to [\mathbf{Set}, \mathbf{Set}]$ along $U : \mathbf{Comonad}(\mathbf{Set}) \to [\mathbf{Set}, \mathbf{Set}]$ and the category **DCont** is isomorphic to the category of comonoids in $(\mathbf{Cont}, \mathbf{ld}^c, \cdot^c)$.

<figure><img src="image_2.png" /></figure>

Here are some standard examples of directed containers and corresponding comonads.

*Nonempty list functor (free semigroup functor)* Let $DX = \mathrm{NEList} X = \mu Z \cdot X \times (1 + Z) \cong \Sigma s : \mathbb{N} \cdot [0..s] \to X$. We have $DX \cong [[S, P]]^c X$ for $S = \mathbb{N}, P s = [0..s]$.

The container $(S, P)$ carries a directed container structure given by $s \downarrow p = s - p, \mathbf{o}_s = 0, p \oplus_s p' = p + p'$. Note that all three operations are well-defined: $p \le s$ implies that $s - p$ is well-defined; $0 \le s$; and $p \le s$ and $p' \le s - p$ imply $p + p' \le s$.

The corresponding comonad has $\varepsilon(x : xs) = x$ (the head of $xs$), $\delta[x] = [[x]]$, $\delta(x : xs) = (x : xs) : \delta xs$ (the nonempty list of all nonempty suffixes of $xs$).

There are other directed container structures on $(S, P)$. One is given by $s \downarrow p = s, \mathbf{o}_s = 0, p \oplus_s p' = (p + p') \mod s$. This directed container interprets into the comonad defined by $\varepsilon xs = \mathbf{hd} \, xs, \delta xs = \mathbf{shifts} \, xs$ (the nonempty list of all cyclic shifts of $xs$).

*Exponent functor* Let $DX = U \to X \cong 1 \times (U \to X)$ for some set $U$. We have $DX \cong [[S, P]]^c X$ for $S = 1, P^* = U$.

Directed container structures on $[[S, P]]^c$ are in a bijection with monoid structures on $U$. Given a monoid structure $(\mathbf{i}, \otimes)$, the corresponding directed container structure is given by $\mathbf{i} \downarrow p = \mathbf{i}, \mathbf{o}_\mathbf{i} = \mathbf{i}, p \oplus_\mathbf{i} p' = p \otimes p'$.

The corresponding comonad has $\varepsilon f = f \mathbf{i}, \delta f = \lambda p. \lambda p'. f (p \otimes p')$.

Via the isomorphism $\mathrm{Str} X = \nu Z \cdot X \times Z \cong \mathbb{N} \to X$, the special case of $(U, \mathbf{i}, \otimes) = (\mathbb{N}, 0, +)$ corresponds to the familiar stream comonad defined by $DX = \mathrm{Str} X, \varepsilon xs = \mathbf{hd} \, xs$ (the head of $xs$), $\delta xs = xs : \delta (\mathrm{tl} \, xs)$ (the stream of all suffixes of $xs$). A different special case $(U, \mathbf{i}, \otimes) = (\mathbb{N}, 1, \cdot)$ corresponds to a different stream comonad given by $\varepsilon xs = \mathbf{hd} (\mathrm{tl} \, xs), \delta xs = \mathrm{samplings} \, xs$ (the stream of all samplings of $xs$, where by the sampling of a stream $[x_0, x_1, x_2, \dots]$ at rate $p$ we mean the stream $[x_0, x_p, x_{p*2}, \dots]$).
*Product functor* Let $DX = V \times X = V \times (1 \to X)$ for some set $V$. We have that $TX \cong [S, P]^c X$ for $S = V$, $P_- = 1$.

Evidently there is exactly one directed container structure on $(S, P)$; it is
given by $s \downarrow * = s, o_s = *, s \oplus s = *$.

The corresponding comonad has $\varepsilon(v, x) = x$, $\delta(v, x) = (v, (v, x))$.

We defined directed containers as containers with specific additional struc-
ture. But they are in a bijection (up to isomorphism) with something much more
familiar—small categories. Indeed, a directed container $(S, P, \downarrow, \mathbf{o}, \oplus)$ defines a
small category as follows: the set of objects is $S$, the set of maps between $s$ and
$s'$ is $\Sigma p : P s . (s \downarrow p = s')$; the identities and composition are given by $\mathbf{o}$ and
$\oplus$. Any small category arises from a directed container uniquely in this fashion.
The free category on a set $V$ of objects (the discrete category with $V$ as the
set of objects), for example, arises from the directed container for the product
comonad for $V$. However, directed container morphisms do not correspond to
functors, since the shape map and position map of a container morphism go
in opposite directions. A directed container morphism is reminiscent of a split
opcleavage, except that, instead of a functor, it relies on an object mapping
without an accompanying functorial action and accordingly the lift maps cannot
be required to be opCartesian. A directed container morphism is a cofunctor
(in the opposite direction) in the sense of Aguiar [2]. The category of directed
containers is equivalent to the opposite of the category of small categories and
cofunctors.

3 Containers ∩ Monads

There is no reason why the analysis of container functors with comonad structure
could not be repeated for other types of functors with structure, the most obvious
next candidate target being monads. The additional structure on containers
corresponding to monads was sketched already in the original directed containers
work [3]. Here we discuss the same characterization in detail.

We define an *mnd-container* to be a container (*S*, *P*) with operations

$$
- e : S
$$

$$
- \bullet : \Pi s : S. (P s \to S) \to S
$$

$$
- q_0 : \Pi s : S. \Pi v : P s \to S. P (s \bullet v) \to P s
$$

$$
- q_1 : \Pi s : S. \Pi v : P s \to S. \Pi p : P (s \bullet v) \cdot P (v (v \hat{s} p))
$$

where we write $q_0 s v p$ as $v \hat{s} p$ and $q_1 s v p$ as $p \hat{v} s$, satisfying

$$
- s = s \bullet (\lambda_{-}. e)
$$

$$
- e \bullet (\lambda_{-} s) = s
$$

$$
- (s \bullet v) \bullet (\lambda p''. w (v \hat{s} p'') (p'' \hat{v} s)) = s \bullet (\lambda p' \cdot v p' \bullet w p')
$$

$$
- p = (\lambda_{-}. e) \wedge_{s} p
$$

$$
- p \hat{\vee} \lambda_{-} s \mathbf{e} = p
$$

$$
- v \wedge_s ((\lambda p'' . w (v \wedge_s p'') (p'' \wedge_v s)) \wedge_{s \circ v} p) = (\lambda p' . v p' \bullet w p') \wedge_s p
$$
$$- ((\lambda p'' . w(v \hat{s} p'') (p'' \hat{\vee} v s)) \hat{s} \circ v p') \hat{\vee} v s = \\ \text{let } u p' \leftarrow v p' \bullet w p' \text{ in } w(u \hat{s} p) \hat{v}(u \hat{s} p) (p \hat{\vee} u s)$$

$$- p \hat{\vee} \lambda p'', w(v \hat{s} p'') (p'' \hat{\vee} v s) (s \bullet v) = \\ \text{let } u p' \leftarrow v p' \bullet w p' \text{ in } (p \hat{\vee} u s) \hat{\vee} w(u \hat{s} p) v (u \hat{s} p)$$

We can see that the data $(e, \bullet)$ are like a monoid structure on $S$ modulo the 2nd argument of the multiplication being not an element of $S$, but a function from $Ps$ to $S$ where $s$ is the 1st argument. Similarly, introducing the visual $\hat{s}$, $\hat{\vee}$ notation for the data $q_0$, $q_1$ helps us see that they are reminiscent of a biaction (a pair of agreeing right and left actions) of this monoid-like structure on $P$. But a further difference is also that $P$ is not a set, but a $S$-indexed family of sets.

We also define an *mnd-container morphism* between $(S, P, e, \bullet, \hat{s}, \hat{\vee})$ and $(S', P', e', \bullet', \hat{s}', \hat{\vee}')$ to be a container morphism $(t, q)$ between $(S, P)$ and $(S', P')$ such that

$$- t e = e'$$

$$- t(s \bullet v) = t s \bullet' (t \circ v \circ q_s)$$

$$- v \hat{s} q_{s \circ v} p = q_s ((t \circ v \circ q_s) \hat{s}' p)$$

$$- q_{s \circ v} p \hat{\vee} v s = q_v(v \hat{s} q_{s \circ v} p) (p \hat{\vee}'_{t \circ v \circ q_s} (t s))$$

Mnd-containers form a category **MCont** whose identity and composition are inherited from **Cont**.

Every mnd-container $(S, P, e, \bullet, \hat{s}, \hat{\vee})$ interprets into a monad $[[S, P, e, \bullet, \hat{s}, \hat{\vee}]^{\text{mc}} = (T, \eta, \mu)$ where

$$- T = [[S, P]]^c$$

$$- \eta x = (e, \lambda p . x)$$

$$- \mu(s, v) = \text{let } (v_0 p, v_1 p) \leftarrow v p \text{ in } (s \bullet v_0, \lambda p . v_1 (v_0 \hat{s} p) (p \hat{\vee} v_0 s))$$

Every mnd-container morphism $(t, q)$ between $(S, P, e, \bullet, \hat{s}, \hat{\vee})$ and $(S', P', e', \bullet', \hat{s}', \hat{\vee}')$ interprets into a monad morphism $[[t, q]]^{\text{mc}} = [[t, q]]^c$ between $[[S, P, e, \bullet, \hat{s}, \hat{\vee}]^{\text{mc}}$ and $[[S', P', e', \bullet', \hat{s}', \hat{\vee}']^{\text{mc}}$.

$[[\cdot]]^{\text{mc}}$ is a fully-faithful functor between **MCont** and **Monad(\text{Set})**. Moreover, the functor $[[\cdot]]^{\text{mc}}$ is the pullback of the fully-faithful functor $[[\cdot]]^c : \text{Cont} \to [\text{Set, Set}]$ along $U : \text{Monad(\text{Set})} \to [\text{Set, Set}]$ and the category **MCont** is isomorphic to the category of monoids in $(\text{Cont}, \text{Id}^c, \cdot^c)$.

<figure><img src="image_3.png" /></figure>

We consider as examples some containers interpreting into functors with a monad structure used in programming language semantics or functional programming.
**Coproduct functor** Let $TX = X + E$ for some set $E$. We have that $TX \cong [[S, P]]^c X$ for $S = 1 + E$, $P(\text{inl}*) = 1$, $P(\text{inr}_-) = 0$.

In a hypothetical mnd-container structure on $(S, P)$, we cannot have $e = \text{inr}e_0$ for some $e_0 : E$, since then $Pe = 0$, but all elements of $0 \to S \cong 1$ are equal, in particular, $\lambda_- \text{ inl} * = \lambda_- \text{ inr} e_0 : 0 \to S$, so the 2nd mnd-container equation $e \bullet (\lambda_- s) = s$ cannot hold for both $s = \text{inl} *$ and $s = \text{inr} e_0$.

Therefore it must be that $e = \text{inl} *$. By the 2nd mnd-container equation then $\text{inl} * \bullet v = e \bullet (\lambda * v * ) = v * (\text{since } P(\text{inl}*) = 1)$ whereas $\text{inr} e \bullet v = \text{inr} e \bullet (\lambda_- e) = \text{inr} e$ by the 1st mnd-container equation (since $P(\text{inr} e) = 0$).

To have $p : P(s \bullet v)$ is only possible, if $s = \text{inl} *$, $v = \lambda * \text{inl} *$. In this case, $P(s \bullet v) = 1$ and $p = *$, and we can define $v \lnot_s p = *$ and $p \lceil_v s = *$.

This choice of $(e, \bullet, \lnot, \lceil)$ satisfies all 8 equations of a mnd-container.

We see that the container $(S, P)$ carries exactly one mnd-container structure. The corresponding monad structure on $T$ is that of the exception monad, with $\eta x = \text{inl} x$, $\mu (\text{inl} c) = c$, $\mu (\text{inr} e) = \text{inr} e$.

**List functor (free monoid functor)** Let $T$ be the list functor: $TX = \text{List} X = \mu Z. 1 + X \times Z \cong \Sigma s : \mathbb{N}. [0..s) \to X$. We have that $TX \cong [[S, P]]^c X$ for $S = \mathbb{N}$, $Ps = [0..s)$.

The container $(S, P)$ carries the following mnd-container structure:

$$-e = 1$$

$$-s \bullet v = \sum_{p: [0..s)} v p$$

$$-v \lnot_s p = \text{greatest } p_0 : [0..s) \text{ such that } \sum_{p': [0..p_0)} v p' \le p$$

$$-p \lceil_v s = p - \sum_{p': [0..v \lnot_s p)} v p'$$

The corresponding monad structure on $T$ is the standard list monad with $\eta x = [x]$, $\mu xss = \text{concat} xss$.

This is not the only mnd-container structure available on $(S, P)$. Another is $e = 1, s \bullet \lambda_-. 1 = s, 1 \bullet \lambda_0. s = s, s \bullet v = 0$ otherwise, $\lambda_- . 1 \lnot_s p = p, \lambda_0. s \lnot_1 p = 0$, $p \lceil_{\lambda_-. 1} s = 0, p \lceil_{\lambda_0.} s = p$.

The corresponding monad structure on $T$ has $\eta x = [x]$, $\mu [[x_0], \dots, [x_{v_0-1}]] = [x_0, \dots, x_{v_0-1}]$, $\mu [xs] = xs$, $\mu xss = []$ otherwise.

**Exponent functor** Let $TX = U \to X$ for some set $U$ and $S = 1$, $P* = U$.

There is exactly one mnd-container structure on $(S, P)$ given by

$$-e = *$$

$$-* \bullet (\lambda_- * ) = *$$

$$-(\lambda_- * ) \lnot_* p = p$$

$$-p \lceil_{\lambda_- * } * = p$$

Indeed, first note that the 1st to 3rd equations of an mnd-container are trivialized by $S = 1$. Further, $S = 1$ and the 4th and 5th equations force the definitions of $\lnot$ and $\lceil$ and the remaining equations hold.

The corresponding monad structure on $T$ is given by $\eta x = \lambda u. x$, $\mu f = \lambda u. f uu$. This is the well-known reader monad.
Product functor Let $T X = V \times X$ for some set $V$ and $S = V$, $P_-= 1$.

Any mnd-container structure on $(S, P)$ must be of the form

$$-e=i$$

$$-s \bullet (\lambda*. s') = s \otimes s'$$

$$-(\lambda*. s') \wedge_s * = *$$

$$-* \nabla_{\lambda*, s'} s = *$$

for some $i: V$ and $\otimes: V \to V \to V$. The 1st to 3rd equations of an mnd-container reduce to the equations of a monoid while the remaining equations are trivialized by $P_- = 1$. So mnd-container structures on $(S, P)$ are in a bijective correspondence with monoid structures on $V$.

The corresponding monad structures on $T$ have $\eta x = (i, x)$, $\mu(p, (p', x)) = (p \otimes p', x)$. They are the writer monads for the different monoid structures on $V$.

Underlying functor of the state monad Let $T X = U \to U \times X \cong (U \to U) \times (U \to X)$ for some set $U$. We have $T X \cong \llbracket S, P \rrbracket^c X$ for $S = U \to U$ and $P_- = U$.

The container $(S, P)$ admits the mnd-container structure defined by

$$-e = \lambda p. p$$

$$-s \bullet v = \lambda p. v p (s p)$$

$$-v \wedge_s p = p$$

$$-p \nabla_v s = s p$$

The corresponding monad structure on $T$ is that of the state monad for $U$, given by $\eta x = \lambda u. (u, x)$ and $\mu f = \lambda u. \text{let } (u', g) \leftarrow f u'$ in $g u'$.

This mnd-container structure is not unique; as a simplest variation, one can alternatively choose $s \bullet v = \lambda p. v p (s^n p)$, $p \nabla_v s = s^n p$ for some fixed $n: \mathbb{N}$, with $s^n$ denoting $n$-fold iteration of $s$.

Underlying functor of update monads Let $T X = U \to V \times X \cong (U \to V) \times (U \to X)$ for some sets $U$ and $V$. We have $T X \cong \llbracket S, P \rrbracket^c X$ for $S = U \to V$ and $P_- = U$.

If $(i, \otimes)$ is a monoid structure on $V$ and $\downarrow$ its right action on $U$, then the container $(S, P)$ admits the mnd-container structure defined by

$$-e = \lambda_. i$$

$$-s \bullet v = \lambda p. s p \otimes v p (s p)$$

$$-v \wedge_s p = p$$

$$-p \nabla_v s = p \downarrow s p$$

The corresponding monad structure on $T$ is that of the update monad [5] for $U$, $(V, i, \otimes)$ and $\downarrow$ given by $\eta x = \lambda u. (i, x)$ and $\mu f = \lambda u. \text{let } (p, g) \leftarrow f u; (p', x) \leftarrow g (u \downarrow p)$ in $(p \otimes p', x)$.

It should be clear that not every monad structure on $T$ arises from some $(i, \otimes)$ and $\downarrow$ in this manner.

The list functor example can be generalized in the following way. Let $(O, #, \mathrm{id}, \circ)$ be some non-symmetric operad, i.e., let $O$ be a set of operations,
\# : O \to \mathbb{N} a function fixing the arity of each operation and id : O and
\circ : \Pi_o : O. (\#o \to O) \to O an identity operation and a parallel composition
operator, with \#id = 1 and \#(o \circ v) = \sum_{i:[0,\#o)} \#(vi), satisfying the equations
of a non-symmetric operad. We can take S = O, Po = [0..\#o), e = id, \bullet = \circ
and \wedge, \uparrow as in the definition of the (standard) list mnd-container. This choice
of (S, P, e, \bullet, \wedge, \uparrow) gives an mnd-container. The list mnd-container corresponds
to a special case where there is exactly one operation for every arity, in which
situation we can w.l.o.g. take O = \mathbb{N}, \#o = o. Keeping this generalization of
the list monad example in mind, we can think of mnd-containers as a version of
non-symmetric operads where the argument places of an operation are identified
nominally rather than positionally and operations may also have infinite arities.

Altenkirch and Pinyo [6] have proposed to think of an mnd-container
$(S, P, e, \bullet, \wedge, \uparrow)$ as a “lax” $(1, \Sigma)$-type universe à la Tarski, namely, to view $S$
as a set of types (“codes for types”), $P$ as an assignment of a set to each type,
$e$ as a type 1, $\bullet$ as a $\Sigma$-type former, $\wedge$ and $\uparrow$ as first and second projections
from the denotation of a $\Sigma$-type. The laxity is that there are no constructors
for the denotations of 1 and $\Sigma$-types, and of course the equations governing the
interaction of the constructors and the eliminators are then not enforced either.
Thus 1 need not really denote the singleton set and $\Sigma$-types need not denote
dependent products.

## 4 Containers ∩ Lax Monoidal Functors

We proceed to analyzing containers whose interpretation carries a lax monoidal
functor structure wrt. the (1, ×) monoidal category structure on **Set**. We will
see that the corresponding additional structure on containers is very similar to
that for monads, but simpler.

Recall that a *lax monoidal functor* between monoidal categories (*C*, *I*, ⊗) and (*C*', *I*', ⊗') is defined as a functor *F* between *C* and *C*' with a map *m*⁰ : *I*' → *FI* and a natural transformation with components *m*<sub>*X*,*Y*</sub> : *FX* ⊗' *FY* → *F*(*X* ⊗ *Y*) cohering with the unitors and associators of the two categories. A *lax monoidal transformation* between two lax monoidal functors (*F*, *m*⁰, *m*) and (*F*', *m*⁰', *m*') is a natural transformation *τ* : *F* → *F*' such that *τ*ᵢ ⊙ *m*⁰ = *m*⁰' and *τ*<sub>*X*⊗*Y*</sub> ⊙ *m*<sub>*X*,*Y*</sub> = *m*'<sub>*X*,*Y*</sub> ⊙ *τ*<sub>*X*</sub> ⊗' *τ*<sub>*Y*</sub>.

We define an *lmf-container* as a container (*S*, *P*) with operations

$$
\text{e} : S
$$

$$
\bullet : S \to S \to S
$$

$$
- q_0 : \Pi s : S. \Pi s' : S. P (s \bullet s') \to P s
$$

$$
- q_1 : \Pi s : S. \Pi s' : S. P (s \bullet s') \to P s'
$$

where we write $q_0 s s' p$ as $s' \wedge_s p$ and $q_1 s s' p$ as $p \vee_{s'} s$, satisfying

$$
- e \bullet s = s
$$

$$
- s = s \bullet e
$$

$$
- (s \bullet s') \bullet s'' = s \bullet (s' \bullet s'')
$$
$$-e \hat{\wedge}_s p = p$$

$$-p \hat{\to}_s e = p$$

$$-s' \hat{\wedge}_s (s'' \hat{\wedge}_{s \bullet s'} p) = (s' \bullet s'') \hat{\wedge}_s p$$

$$-(s'' \hat{\wedge}_{s \bullet s'} p) \hat{\to}_{s'} s = s'' \hat{\wedge}_{s'} (p \hat{\to}_{s' \bullet s''} s)$$

$$-p \hat{\to}_{s''} (s \bullet s') = (p \hat{\to}_{s' \bullet s''} s) \hat{\to}_{s''} s'$$

Differently from the mnd-container case, the data $(S, e, \bullet)$ of a lmf-container form a proper monoid. The data $(\wedge, \to)$ resemble a biaction of $(S, e, \bullet)$.

We also define an *lmf-container morphism* between $(S, P, e, \bullet, \wedge, \to)$ and $(S', P', e', \bullet', \wedge', \to')$ to be a container morphism $(t, q)$ between $(S, P)$ and $(S', P')$ such that

$$-t e = e'$$

$$-t(s \bullet s') = t s \bullet' t s'$$

$$-s' \wedge_s q_{s \bullet s'} p = q_s (t s' \wedge'_{t s} p)$$

$$-q_{s \bullet s'} p \wedge'_{s'} s = q_{s'} (p \wedge'_{t s'} t s)$$

Lmf-containers form a category **LCont** whose identity and composition are inherited from **Cont**.

Every lmf-container $(S, P, e, \bullet, \wedge, \to)$ interprets into a lax monoidal endofunctor $[[S, P, e, \bullet, \wedge, \to]]^{\text{lc}} = (F, \mathbf{m}^0, \mathbf{m})$ on $(\mathbf{Set}, 1, \times)$ where

$$-F = [[S, P]]^c$$

$$-\mathbf{m}^0 * = (e, \lambda_{\cdot} * )$$

$$-\mathbf{m}((s, v), (s', v')) = (s \bullet s', \lambda p. (v (s' \wedge_s p), v' (p \wedge'_{s'} s)))$$

Every lmf-container morphism $(t, q)$ between $(S, P, e, \bullet, \wedge, \to)$ and $(S', P', e', \bullet', \wedge', \to')$ interprets into a lax monoidal transformation $[[t, q]]^{\text{lc}} = [[t, q]]^c$ between $[[S, P, e, \bullet, \wedge, \to]]^{\text{mc}}$ and $[[S', P', e', \bullet', \wedge', \to']^{\text{lc}}$.

$[[\cdot]]^{\text{lc}}$ is a fully-faithful functor between **LCont** and the category **LMF**(Set) of lax endofunctors on $(\mathbf{Set}, 1, \times)$. The functor $[[\cdot]]^{\text{lc}}$ is the pullback of the fully-faithful functor $[[\cdot]]^c : \mathbf{Cont} \to [\mathbf{Set}, \mathbf{Set}]$ along $U : \mathbf{LMF}(\mathbf{Set}) \to [\mathbf{Set}, \mathbf{Set}]$. The category **LCont** is isomorphic to the category of monoids in $(\mathbf{Cont}, \mathbf{Id}^c, \otimes^c)$.

<figure><img src="image_4.png" /></figure>

The similarity between the additional structures on containers for monads and lax monoidal functors may at first appear unexpected, but the reasons become clearer, if one compares the types of the “accumulating” Kleisli extension $\lambda(c, f)$. $\mu(T(\lambda x. T(\lambda y. (x, y)) (f x)) c) : T X \times (X \to T Y) \to T(X \times Y)$ and the monoidality constraint $\mathbf{m} \cdot F X \times F Y \to F(X \times Y)$.

It is immediate from the definitions that any mnd-container $(S, P, e, \bullet, \wedge, \to)$ carries an lmf-container structure $(e', \bullet', \wedge', \to')$ given by
$$-e' = e$$

$$-s \bullet' s' = s \bullet (\lambda_{-} s')$$

$$-s' \hat{\wedge}'_s p = (\lambda_{-} s') \wedge'_s p$$

$$-p \nolimits_{s'} s = p \nolimits_{\lambda_{-} s'} s$$

This is in agreement with the theorem that any strong monad defines a strong lax monoidal functor. Since any set functor is uniquely strong and all natural transformations between set functors are strong, the strength assumption and conclusion trivialize in our setting.

Another immediate observation is that, for any lmf-container structure $(e, \bullet, \wedge, \nolimits)$ on $(S, P)$, there is also a reverse lmf-container structure $(e', \bullet', \wedge', \nolimits')$ given by

$$-e' = e$$

$$-s \bullet' s' = s' \bullet s$$

$$-s' \wedge'_s p = p \nolimits_s s'$$

$$-p \nolimits_{s'} s = s \wedge_{s'} p$$

The corresponding statement about lax monoidal functors holds for any symmetric monoidal category.

Let us now revisit our example containers and see which lmf-container structures they admit.

**Coproduct functor** Let $TX = X+E$ for some set $E$ and $S = 1+E$, $P(\text{inl}*) = 1$, $P(\text{inr}_-) = 0$.

Any lmf-container structure on $(S, P)$ must have $e = \text{inl} *$. Indeed, if it were the case $e = \text{inr} e_0$ for some $e_0 : E$, then we would have $\text{inr} e_0 \bullet \text{inl} * = \text{inl} *$ by the 1st lmf-container equation. But then $q_0 (\text{inr} e_0) (\text{inl}*) : 1 \to 0$, which cannot be.

Similarly, for all $e_0 : E, s : S$, it must be that $\text{inr} e_0 \bullet s \neq \text{inl} *$ and $s \bullet \text{inr} e_0 \neq \text{inl} *$. Hence, by the 1st and 2nd lmf-container equations, it must be the case that $\text{inl} * \bullet s = s$, $\text{inr} e \bullet \text{inl} * = \text{inr} e$, $\text{inr} e \bullet \text{inr} e' = \text{inr} (e \otimes e')$. The 3rd lmf-container equation forces that $\otimes$ is a semigroup structure on $E$. The other lmf-container equations hold trivially. Therefore, lmf-container structures on $(S, P)$ are in a bijection with semigroup structures on $E$.

The corresponding lax monoidal functors have $m^0 * = \text{inl} *$, $m(\text{inl} x, \text{inl} x') = \text{inl}(x, x')$, $m(\text{inl} x, \text{inr} e) = \text{inr} e$, $m(\text{inr} e, \text{inl} x) = \text{inr} e$, $m(\text{inr} e, \text{inr} e') = \text{inr}(e \otimes e')$.

The unique mnd-container structure on $(S, P)$ corresponds to the particular case of the left zero semigroup, i.e., the semigroup where $e \otimes e' = e$.

**List functor** Let $TX = \text{List} X$ and $S = \mathbb{N}$, $Ps = [0..s)$.

The standard mnd-container structure on $(S, P)$ gives this lmf-container structure:

$$-e = 1$$

$$-s \bullet s' = s * s'$$

$$-s' \wedge_s p = p \text{ div } s'$$

$$-p \nolimits_{s'} s = p \text{ mod } s'$$
The corresponding lax monoidal functor structure on $T$ is given by $\mathfrak{m}^0 * = [*]$, $\mathfrak{m}(xs, ys) = [(x, y) | x \leftarrow xs, y \leftarrow ys]$.

The other mnd-container structure we considered gives $e = 1$, $s \bullet 1 = s$, $1 \bullet s = s$, $s \bullet s' = 0$ otherwise, $1 \hat{s} p = p$, $s \hat{1} p = 0$, $p \hat{1} s = 0$, $p \hat{s} 1 = p$.

The corresponding lax monoidal functor structure on $T$ is $\mathfrak{m}^0 * = [*]$, $\mathfrak{m}(xs, [y]) = [(x, y) | x \leftarrow xs]$, $\mathfrak{m}([x], ys) = [(x, y) | y \leftarrow ys]$, $\mathfrak{m}(xs, ys) = []$ otherwise.

But there are further lmf-container structures on $(S, P)$ that do not arise from an mnd-container structure, for example this:

$$-e=1$$

$$-s \bullet s' = s \min s'$$

$$-s' \hat{s} p = p$$

$$-p \hat{s'} s = p$$

The corresponding lax monoidal functor structure is $\mathfrak{m}^0 * = [*]$, $\mathfrak{m}(xs, ys) = \text{zip}(xs, ys)$.

*Exponent functor* Let $T X = U \to X$ for some set $U$ and $S = 1$, $P * = U$.

There is exactly one lmf-container structure on $(S, P)$ given by

$$-e = *$$

$$-* \bullet * = *$$

$$-* \hat{s} p = p$$

$$-p \hat{s} * = p$$

and that is the lmf-container given by the unique mnd-container structure.

The corresponding lax monoidal functor structure on $T$ is given by $\mathfrak{m}^0 * = \lambda u. *, \mathfrak{m}(f, f') = \lambda u. (f u, f' u)$.

*Product functor* Let $T X = V \times X$ for some set $V$ and $S = V$, $P_- = 1$.

Any lmf-container structure on $(S, P)$ must be of the form

$$-e = i$$

$$-s \bullet s' = s \otimes s'$$

$$-s' \hat{s} * = *$$

$$-* \hat{s'} s = *$$

for $(i, \otimes)$ a monoid structure on $V$, so the only lmf-container structures are those given by mnd-structures.

The corresponding lax monoidal functor structures on $T$ are given by $\mathfrak{m}^0 * = (i, *), \mathfrak{m}((p, x), (p', x')) = (p \otimes p', (x, x'))$.

Similarly to the monad case, we can generalize the list functor example. Now we are interested in relaxation of non-symmetric operads where parallel composition is only defined when the given $n$ operations composed with the given $n$-ary operation are all the same, i.e., we have $O$ a set of operations, $\# : O \to \mathbb{N}$ a function fixing the arity of each operation and $\text{id} : O$ and $\circ : O \to O \to O$
an identity operation and a parallel composition operator, with #id = 1 and
#(o ◦ o') = #o * #o', satisfying the equations of an ordinary non-symmetric
operad. If we now choose S = O, Po = [0..#o), e = id, • = ◦ and take ⃛, / as in the definition of the standard list lmf-container, we get a non-symmetric
operad in this relaxed sense.

Under the lax type universe view, an lmf-container is a lax (1, ×)-universe, i.e., it is only closed under non-dependent lax Σ-types.

5 Further specializations

There are numerous special types of monads and lax monoidal functors that can
be analyzed similarly. Here are some examples.

The lax monoidal functor interpreting an lmf-container is symmetric (i.e.,
satisfies $F \sigma_{X,Y} \circ m_{X,Y} = m_{Y,X} \circ \sigma_{FX,FY}$) if and only if the lmf-container is
identical to its reverse, i.e., it satisfies

$$
- s \bullet s' = s' \bullet s,
$$

$$
- s' \hat{\lambda}_s p = p \hat{\lambda}_s s'
$$

In this case, the monoid $(S, \mathbf{e}, \bullet)$ is commutative and each of the two action-like operations $\lambda, /$ determines the other.

The monad interpreting an mnd-container is commutative (which reduces to
the corresponding lax monoidal functor being symmetric) if and only if

$$
- s \bullet (\lambda_{-} s') = s' \bullet (\lambda_{-} s)
$$

$$
- (\lambda_{-} s') \wedge_{s} p = p \wedge_{\lambda_{-} s} s'
$$

Note that, in this case, $\lambda$ and $/$ are constrained, but not to the degree of fully
determining each other.

The monad interpreting an mnd-container is Cartesian (which means that
all naturality squares of η and μ are pullbacks) if and only if

- the function $\lambda_{-} * : P \mathbf{e} \to 1$ is an isomorphism

- for any $s: S$ and $v: P s \to S$, the function $\lambda p. (v \wedge_s p, p / v_s s) : P (s \bullet v) \to \Sigma p : P s. P (v p)$ is an isomorphism.

Such mnd-containers with additional conditions are proper (1, Σ)-type universes:
1 and Σ-types denote the singleton set and dependent products.

6 Conclusion

We showed that the containers whose interpretation into a set functor carries
a monad or a lax monoidal functor structure admit explicit characterizations
similar to the directed container (or small category) characterization of those
containers whose interpretation is a comonad. It was not surprising that such
characterizations are possible, as we could build on the very same observations
that were used in the analysis of the comonad case. But the elaboration of
the characterizations is, we believe, novel. We also believe that it provides useful
insights into the nature of monad or lax monoidal functor structures on container
functors. In particular, it provides some clues on why monads and lax monoidal
functors on **Set** and, more generally, in the situation of canonical strengths
enjoy analogous properties. In future work, we would like to reach a better
understanding of the connections of containers to operads.

*Acknowledgments* I am very grateful to Thorsten Altenkirch, Pierre-Louis Curien, Conor McBride, Niccolò Veltri for discussions. Paul-André Melliès pointed me to Aguiar’s work. The anonymous reviewers of TTCS 2017 provided very useful feedback. This work was supported by the Estonian Ministry of Education and Research institutional research grant IUT33-13.

References

1. Abbott, M., Altenkirch, A., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci., 342(1), 3-27 (2005) doi: 10.1016/j.tcs.2005.06.002

2. Aguiar, M.: Internal Categories and Quantum Groups. PhD thesis. Cornell University, Ithaca, NY (1997) http://www.math.cornell.edu/~maguiar/thesis2.pdf

3. Ahman, D., Chapman, J., Uustalu, T.: When is a container a comonad? Log. Methods Comput. Sci., 10(3), article 14 (2014) doi: 10.2168/lmcs-10(3:14)2014

4. Ahman, D., Uustalu, T.: Directed containers as categories. In: Atkey, R., Krishnaswami, N. (eds.) Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016, Electron. Proc. in Theor. Comput. Sci., vol. 207, pp. 89-98. Open Publishing Assoc., Sydney (2016) doi: 10.4204/eptcs.207.5

5. Ahman, D., Uustalu, T.: Update monads: cointerpreting directed containers. In: Matthes, R., Schubert, A. (eds.) Proc. of 19th Conf. on Types for Proofs and Programs, Leibniz Int. Proc. in Inf., vol. 26, pp. 1-23. Dagstuhl Publishing, Saarbrücken/Wadern (2014) doi: 10.4230/lipics.types.2013.1

6. Altenkirch, T., Pinyo, G.: Monadic containers and universes (abstract). In: Kaposi, A. (ed.) Abstracts of 23rd Int. Conf. on Types for Proofs and Programs, TYPES 2017, pp. 20-21. Eötvös Lórand University, Budapest (2017)

7. Capriotti, P., Kaposi, A.: Free applicative functors. In: Levy, P., Krishnaswami, N. (eds.) Proc. of 5th Wksh. on Mathematically Structured Functional Programming, MSFP 2014, Electron. Proc. in Theor. Comput. Sci., vol. 153, pp. 2-30. Open Publishing Assoc., Sydney (2014) doi: 10.4204/eptcs.153.2

8. Curien, P.-L.: Syntactic presentation of polynomial functors. Note (May 2017)

9. Gambino, N, Hyland, M.: Wellfounded trees and dependent polynomial functors. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Revised Selected Papers from Int. Wksh. on Types for Proofs and Programs, TYPES 2003, Lect. Notes in Comput. Sci., vol. 2075, pp. 210-225. Springer (2004) doi: 10.1007/978-3-540-24849-1_14

10. Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Math. Proc. Cambridge Philos. Soc. 154(1), 153-192 (2013) doi: 10.1017/s0305004112000394

11. Girard, J.-Y.: Normal functors, power series and lambda-calculus. Ann. Pure Appl. Log., 37(2), pp. 129-177 (1988) doi: 10.1016/0168-0072(88)90025-5

12. McBride, C. Paterson, R.: Applicative programming with effects. J. Funct. Program., 18(1), 1-13 (2008) doi: 10.1017/s0956796807006326

13. Weber, M.: Polynomials in categories with pullbacks. Theor. Appl. Categ., 30, pp. 533-598 (2015) http://www.tac.mta.ca/tac/volumes/30/16/30-16abs.html