Distributive Laws of Monadic Containers

Purdy, Chris; Damato, Stefania

doi:10.4230/LIPIcs.CALCO.2025.4

Distributive Laws of Monadic Containers

Chris Purdy

Royal Holloway University of London, Egham, UK Stefania Damato

School of Computer Science, University of Nottingham, UK

Abstract

Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose.

In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu’s characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the “zoo” of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.

Keywords and phrases:

distributive laws, monadic containers, monads, dependent types, cubical agda

DOI:

10.4230/LIPIcs.CALCO.2025.4

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Categorical semantics ; Theory of computation

\rightarrow

Type structures

Acknowledgements:

The authors would like to thank Thorsten Altenkirch, Dan Marsden, Stiéphen Pradal, and Reuben Rowe for helpful discussions on this work, Tom de Jong for inspiring our use of the

symbol for formalised statements, and the anonymous reviewers for their suggestions.

Supplementary Material:

Software (Source Code): https://github.com/chrisjpurdy/distr-laws-of-monadic-containers [26]
archived at

swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a

Software (Source Code): https://stefaniatadama.com/distr-law-mnd-cont-html/ [27]

Software (Source Code): https://github.com/stefaniatadama/cubical/tree/distr-laws [28]

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Containers, introduced by Abbott et al. [3], give an algebraic presentation of a wide class of strictly positive data types. Often, reasoning about strictly positive data types in terms of their container representation is simpler than their functorial representation – for example, transformations between container functors constructed from container morphisms are automatically natural.

Monads have received a lot of attention in functional programming [18] and denotational semantics for their ability to model a wide range of programmatic side-effects [25]. In practice, it is rare for side-effects to appear individually – developing a way of composing monads is useful for situations where multiple effects are interleaved. In general, however, the composition of two monads need not result in another monad. Distributive laws [11] were developed as a sufficient condition for such a composition to form a monad, thereby ensuring that the corresponding side-effects are interleaved in a coherent way. Constructing distributive laws is known to be quite difficult due to the complexities involved in checking their axioms, besides the fact that some monads, even if they are composable, do not admit a distributive law in the first place [34, Remark 4.19]. As a result, various work has been done on different approaches for constructing distributive laws [23, 24], and for identifying cases where there are none [34, 20].

In this paper, we develop a characterisation of distributive laws of monadic containers [31], i.e. containers whose interpretation carries a monad structure, with the goal of providing an algebraic way of reasoning about distributive laws between strictly positive data types. We build on similar characterisations in the literature; Ahman, Chapman, and Uustalu develop directed containers [5], i.e. containers whose interpretation carries a comonad structure, and the first and last authors provide a characterisation of their distributive laws [6]. Uustalu also develops monadic containers [31], but to our knowledge, no work has been done on characterising their distributive laws. Our work parallels the development in [6] for monadic containers and therefore closes this gap. Furthermore, by combining our work with [6], we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the “zoo” of container characterisations of (co)monads and their distributive laws.

Formalisation

Since our representation of distributive laws involves a list of highly dependent equalities, it lends itself well to formalisation in a proof assistant such as Cubical Agda [32], in which we have formalised our characterisations as well as those in [5, 6]. The formalised statements are annotated by a symbol, which is a clickable link to the corresponding statement in the formalisation. The code can be found at github.com/chrisjpurdy/distr-laws-of-monadic-containers, and an HTML rendered version can be found at stefaniatadama.com/distr-law-mnd-cont-html/. While the aformentioned code implicitly assumes that we are dealing with h-sets throughout, we are currently working on a version of this code that makes this explicit and uses definitions from the Cubical library [29]. This version can be found at github.com/stefaniatadama/cubical/tree/distr-laws.

Setting of our work & Notation

We work in cubical type theory [14, 32] but our work holds in any intensional Martin-Löf type theory by assuming extensionality principles that are provable in cubical type theory, namely function extensionality (in particular, we do not use univalence). Throughout the paper, we use several type-theoretic notations made explicit below.

$\blacksquare$

We use $\sum_{a:A}B\,a$ for dependent sums and $\prod_{a:A}B\,a$ for dependent products, their non-dependent counterparts represented as $A\times B$ and $A\to B$ respectively. $A+B$ denotes the sum type of $A$ and $B$ . The notation $(a,b)$ refers to an element of a product type, $\lambda x.f\,x$ an element of a function type, and $\mathsf{inl}\,a$ and $\mathsf{inr}\,b$ elements of a sum. $\pi_{1}$ and $\pi_{2}$ are the first and second projections out of a product type.
$\blacksquare$

The symbol $\coloneqq$ refers to definitional equality, $=$ refers to propositional equality, and $\cong$ refers to isomorphism of types.
$\blacksquare$

The empty type is denoted by $\bot$ and the unit type by $\top$ with element $\star$ . $\mathsf{Fin}\;n$ is the type of finite sets of size $n$ .
$\blacksquare$

The category whose objects are (small) sets and whose morphisms are functions is denoted by Set, while $\mathsf{Set}$ denotes the universe of homotopy-sets (h-sets), or 0-types.
$\blacksquare$

The category of endofunctors on Set is denoted by $[\textul{\textbf{Set}},\textul{\textbf{Set}}]$ .
$\blacksquare$

A few times we mention that an equality “holds up to” another equality, by which we mean that we have a heterogenous equality, or a path “lying over” another path. For more details on this, see [30, Section 2.3].

Organisation of the paper

The paper is organised as follows. After mentioning some related work in Section 2, we briefly review containers and monadic containers in Section 3. In Section 4, we characterise distributive laws of monadic containers and provide some examples using this characterisation, and in Section 5 we look at compatible composites of monadic containers. In Section 6, we use an existing characterisation of distributive laws of directed containers to characterise mixed distributive laws. In Section 7 we provide a starting point for using this characterisation to prove no-go theorems for monadic containers, before concluding in Section 8.

2 Related work

Containers are related to polynomial functors, as studied by Gambino and Hyland [15]. Specifically, polynomial functors on the LCCC of $\mathsf{Set}$ s are equivalent to indexed container functors, and in a special case we get (ordinary) container functors (when the object $I$ in [15, Section 5] is the terminal object). Polynomial monads (polynomial functors equipped with cartesian monad maps) have been studied by Gambino and Kock [16], but to our knowledge there is no characterisation of when polynomial monads can be composed via a distributive law or otherwise. Monadic containers fail to be a special case of polynomial monads, as monadic containers are not required to be cartesian. However, we do have that cartesian monadic containers, referred to as $\Sigma$ -universes by Altenkirch and Pinyo [9], are special cases of polynomial monads. Awodey first mentions the connection between lax $\Sigma$ -universes and a monad structure on polynomial functors in [10, Remark 13].

Manes and Mulry [23, 24] have developed general theorems concerning the existence of distributive laws. Zwart and Marsden [34, 33] have developed “no-go theorems” for monads that can be represented as algebraic theories, filling many holes in an extended version of the Boom hierarchy [13]. Algebraic theories are disjoint from monadic containers in the sense that all monads representable by algebraic theories are finitary. On the other hand, the container $\top\triangleleft\lambda\_.A$ can be uniquely equipped with monadic container data, and the extension of this container is not finitary if $A$ is non-finite [21]. Ahman, Chapman, and Uustalu’s characterisation of directed containers [5] has been used by Karamlou and Shah to develop no-go theorems relevant to finite model theory [20].

Directed containers and certain theorems in [5] have already been formalised in vanilla Agda [4], but to our knowledge their distributive laws have not. We formalise directed containers and their distributive laws alongside our own developments in Cubical Agda, but do not recreate all proofs included in [4].

3 Monadic containers

In this section, we briefly review containers and their functor representation, we state the definition of monadic containers we will be using, and provide some examples of both.

3.1 Containers

The purpose of containers [3, 2, 1, 8] is to provide a uniform way to represent strictly positive data types. By a “strictly positive type” we roughly mean a type $X$ whose constructors are only allowed to have $X$ appear in input types that are arrows if it appears on their right. Allowing non-strictly positive types in our theories can be problematic and potentially lead to contradictions [30, Section 5.6]. In this sense, containers carve out a class of nicely behaved types, and they express the fact that any such type can be fully represented by a set of “shapes” $S$ and a family of “positions” $P$ over those shapes, at which data can be stored.

Definition 1.

A container is given by a type $S:\mathsf{Set}$ and a family of types $P:S\to\mathsf{Set}$ , which we write as $S\triangleleft P$ .

Example 2 ( ).

The container representation of the maybe type, which can either contain a value or indicate that there is no value, is the following.

\top+\top\triangleleft\lambda\begin{cases}\mathsf{inl}\,\star\to\bot\\ \mathsf{inr}\,\star\to\top\end{cases}

The shape $\top+\top$ represents a choice between having a value or not. If the shape is $\mathsf{inl}\,\star$ , this represents the absence of a value, so the type of positions is $\bot$ as there is no more data to supply. If the shape is $\mathsf{inr}\,\star$ , we do have a value, so the type of positions is $\top$ since there is one position for a singular piece of data.

Example 3 ( ).

The container representation of the list type is $\mathbb{N}\triangleleft\mathsf{Fin}$ . The shape of a list is a natural number $n$ representing its length, and there are $n$ -many positions for data to be stored in a list of length $n$ , represented by the set $\mathsf{Fin}\;n$ .

Containers together with the following morphisms form a category Cont.

Definition 4.

A container morphism $(S\triangleleft P)\to(T\triangleleft Q)$ is a pair

	$\displaystyle u$	$\displaystyle\colon S\to T$
	$\displaystyle f$	$\displaystyle\colon\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod% $}}}_{s:S}Q\,(u\,s)\to P\,s$

written as $u\triangleleft f$ .

Example 5.

There is a container morphism $\mathbb{N}\triangleleft\mathsf{Fin}\to(\top+\mathbb{N})\triangleleft\lambda x.% \begin{cases}\mathsf{inl}\,\star\to\bot\\ \mathsf{inr}\,n\to\mathsf{Fin}\;n\end{cases}$ that “takes the tail” of a list container, given by

	$\displaystyle u\,0$	$\displaystyle\coloneqq\mathsf{inl}\,\star$
	$\displaystyle u\,(n+1)$	$\displaystyle\coloneqq\mathsf{inr}\,n\qquad\qquad\qquad\qquad f\,(n+1)\,p% \coloneqq p+1$

The function $u$ describes the change to the length of the list (“failing” if the list is empty), and $f$ maps positions in the tail of the list to positions in the original list.

Every container has a functorial interpretation in the category $[\textul{\textbf{Set}},\textul{\textbf{Set}}]$ .

Definition 6.

The container functor associated to a container $S\triangleleft P$ is the functor denoted by $\llbracket S\triangleleft P\rrbracket\colon\mathsf{Set}\to\mathsf{Set}$ , with the following actions on objects and morphisms.

$\blacksquare$

Given an $X:\mathsf{Set},\llbracket S\triangleleft P\rrbracket\,X\coloneqq\underset{s:S}% {\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\sum$}}}}(P\,s\to X)$ .
$\blacksquare$

Given $X,Y:\mathsf{Set}$ and a morphism $f\colon X\to Y$ , for $s : S$ and $g\colon P\,s\to X$ ,

$\llbracket S\triangleleft P\rrbracket\,f\,(s,g)\coloneqq(s,f\circ g).$

The map $\llbracket\_\rrbracket\colon\textul{\textbf{Cont}}\to[\textul{\textbf{Set}},% \textul{\textbf{Set}}]$ is extended to a fully-faithful functor by taking $\llbracket u\lhd f\rrbracket\,(s,g):=(u\,s,g\circ f)$ as the action on container morphisms. Crucially for us, the category Cont is monoidal, with the composition of containers as the monoidal product and $\top\triangleleft\lambda\_.\top$ as the unit.

Definition 7.

Given containers $S\triangleleft P$ and $T\triangleleft Q$ , their composite, denoted $(S\triangleleft P)\circ(T\triangleleft Q)$ , is defined as the container

(S\triangleleft P)\circ(T\triangleleft Q):=[\![S\triangleleft P]\!]\,\,T% \triangleleft\Big{(}\lambda(s,f).\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\sum$}}}_{p:P\,s}Q\,(f\,p)\Big{)}

The functor $\llbracket\_\rrbracket$ is monoidal, i.e. it preserves monoidal multiplication and unit.

3.2 Monadic containers

Monadic containers were developed by Uustalu [31] as a characterisation of monads whose underlying functors are container functors. We adopt conventions used by Altenkirch and Pinyo in [9], referring to them as monadic containers (rather than mnd-containers) and using their presentation as lax $\Sigma$ -universes.

Definition 8 ( ).

Let $S\triangleleft P$ be a container. A monadic container on $S\triangleleft P$ is a tuple $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ where

	$\displaystyle\iota:S$
	$\displaystyle\sigma:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}(P\,s\to S)\to S$
	$\displaystyle\mathsf{pr}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s:S\}}}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f:P\,s\to S\}}}P\,(\sigma\,s\,f)\to\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\sum$}}}_{p:P\,s}\,P\,(f\,p)$

satisfying the following equations:

	$\displaystyle\sigma\,\iota\,(\lambda\_.s)$	$\displaystyle=s$	$\displaystyle\sigma\,s\,(\lambda\_.\iota)$	$\displaystyle=s$
	$\displaystyle\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\iota\}}\,{\color[rgb]{.5,.5,.5}\definecolor[% named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\lambda\_.s\}}\,p$	$\displaystyle=p$	$\displaystyle\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\lambda\_.\iota\}}\,p$	$\displaystyle=p$

	$\displaystyle\sigma\,s\,(\lambda p.\,\sigma\,(f\,p)\,(g\circ(p,-)))=\sigma\,(% \sigma\,s\,f)\,(g\circ\mathsf{pr})$
	$\displaystyle\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\lambda p.\sigma\,(f\,p)\,(g\circ(p,-))\}}\,p=% \mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,(\mathsf{pr}_{% 1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\sigma\,s\,f\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{g\circ\mathsf{pr}\}}% \,p)$
	$\displaystyle\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\,(\mathsf{pr}_{1}\,p)\}}\,{\color[rgb]{.5,.5,.5% }\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.% 5}\pgfsys@color@gray@fill{.5}\{\lambda p^{\prime}.g\,(\mathsf{pr}_{1}\,p,p^{% \prime})\}}\,(\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\lambda p.\sigma\,(f\,p)\,(g\circ(p,-))\}}\,p)=$
	$\displaystyle\hskip 224.7766pt\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}% \definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5% }\pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,(\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}% \definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5% }\pgfsys@color@gray@fill{.5}\{\sigma\,s\,f\}}\,{\color[rgb]{.5,.5,.5}% \definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5% }\pgfsys@color@gray@fill{.5}\{g\circ\mathsf{pr}\}}\,p)$
	$\displaystyle\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\,(\mathsf{pr}_{1}\,p)\}}\,{\color[rgb]{.5,.5,.5% }\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.% 5}\pgfsys@color@gray@fill{.5}\{\lambda p^{\prime}.g\,(\mathsf{pr}_{1}\,p,p^{% \prime})\}}\,(\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\lambda p.\sigma\,(f\,p)\,(g\circ(p,-))\}}\,p)=% \mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\sigma\,s% \,f\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{g\circ% \mathsf{pr}\}}\,p$

where we use the shorthands $\mathsf{pr}_{i}:=\pi_{i}\circ\mathsf{pr}$ , and $(p,-):=\lambda p^{\prime}.(p,p^{\prime})$ . The equalities for $\mathsf{pr}$ hold up to the corresponding equalities for $\sigma$ above them.

For clarity we include all implicit arguments in grey in the equations above, but we will often omit them when they can be inferred from the context. For example, given $p:P\,(\sigma\,(\sigma\,s\,f)\,(g\circ\mathsf{pr}))$ , we can write the last three equalities for $\mathsf{pr}$ as

\displaystyle\mathsf{pr}_{1}\,p

\displaystyle=\mathsf{pr}_{1}\,(\mathsf{pr}_{1}\,p)

\displaystyle\mathsf{pr}_{1}\,(\mathsf{pr}_{2}\,p)

\displaystyle=\mathsf{pr}_{2}\,(\mathsf{pr}_{1}\,p)

\displaystyle\mathsf{pr}_{2}\,(\mathsf{pr}_{2}\,p)

\displaystyle=\mathsf{pr}_{2}\,p

Abusing notation, we will refer to a monadic container $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ by its container $S\triangleleft P$ , when $\iota,\sigma$ and $\mathsf{pr}$ are clear from the context.

Monadic containers can be thought of as containers whose sets of shapes are pointed, and closed under taking “container-fulls” of shapes, in the sense that any element $(s,f):\llbracket S\triangleleft P\rrbracket\,S$ gives a new shape $\sigma\,s\,f:S$ . The role of $\mathsf{pr}$ is to specify how positions $p:P\,(\sigma\,s\,f)$ map to positions $p_{1}:P\,s$ and $p_{2}:P\,(f\,p_{1})$ .

Every monadic container can be interpreted as a monad on Set, this interpretation being an extension of the usual interpretation of containers as functors.

Definition 9.

The monad interpretation of a monadic container $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ is defined as the monad $(\llbracket S\triangleleft P\rrbracket,\eta,\mu)$ on Set, denoted by $\llbracket S\triangleleft P,\iota,\sigma,\mathsf{pr}\rrbracket^{\text{mc}}$ , or simply $\llbracket S\triangleleft P\rrbracket^{\text{mc}}$ when the monadic container structure is clear from the context, where

	$\displaystyle\eta:\text{Id}\Rightarrow\llbracket S\triangleleft P\rrbracket$	$\displaystyle\mu:\llbracket S\triangleleft P\rrbracket\circ\llbracket S% \triangleleft P\rrbracket\Rightarrow\llbracket S\triangleleft P\rrbracket$
	$\displaystyle\eta_{A}\,a:=(\iota,\lambda\_.a)$	$\displaystyle\mu_{A}\,(s,f):=(\sigma\,s\,(\pi_{1}\circ f),\lambda p.\pi_{2}\,(% f\,(\mathsf{pr}_{1}\,p))\,(\mathsf{pr}_{2}\,p))$

Monadic containers can also be seen as lax versions of (Tarski-style) type universes closed under singleton and dependent sum types [9]. Shapes are interpreted as codes for types, and the position family is the map that interprets each code as a concrete type. $\iota$ is the code for the singleton type, and $\sigma$ constructs codes for $\Sigma$ -types.

Definition 10.

A $\Sigma$ -universe $(S\triangleleft P,\iota,\mathsf{un},\sigma,\mathsf{pr})$ is given by a monadic container $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ with the isomorphisms

	$\displaystyle\mathsf{un}:P\,\iota\cong\top$
	$\displaystyle\mathsf{pr}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s:S\}}}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f:P\,s\to S\}}}P\,(\sigma\,s\,f)\cong\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\sum$}}}_{p:P\,s}\ P\,(f\,p)$

i.e. where for all $s$ and $f$ , $\mathsf{pr}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}$ is an isomorphism, and $P\,\iota$ is isomorphic to $\top$ .

The container examples we describe at the start of this section can each be equipped with monadic container structure.

Example 11.

The list container $\mathbb{N}\triangleleft\mathsf{Fin}\;$ can be extended to a monadic container by taking

	$\displaystyle\iota$	$\displaystyle:=1$
	$\displaystyle\sigma\,n\,f$	$\displaystyle:=f\,0+\dots+f\,(n-1)$
	$\displaystyle\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{n\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,p$	$\displaystyle:=\max\,\{i\in[0..n)\ \|\ f\,0+\dots+f\,(i-1)\leq p\}$
	$\displaystyle\mathsf{pr}_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{n\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,p$	$\displaystyle:=p-(f\,0+\dots+f\,((\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}% \definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5% }\pgfsys@color@gray@fill{.5}\{n\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,p)-1)).$

This is also an example of a $\Sigma$ -universe. The monad interpretation of this container is isomorphic to the list monad with concatenation.

Example 12 ( ).

Given some set $S$ , the container $(S\to S)\triangleleft\lambda\_.S$ can be extended to a monadic container by taking

	$\displaystyle\iota$	$\displaystyle:=\lambda x.x$
	$\displaystyle\sigma\,f\,g$	$\displaystyle:=\lambda x.g\,x\,(f\,x)$
	$\displaystyle\mathsf{pr}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,x$	$\displaystyle:=(x,f\,x).$

The monad interpretation of this is the well-known state monad from functional programming.

Example 13 ( ).

The container $(\top+E)\triangleleft\text{Tr}$ of coproducts with $E$ , where

	$\displaystyle\text{Tr}\,(\mathsf{inl}\,\star)$	$\displaystyle\coloneqq\top$
	$\displaystyle\text{Tr}\,(\mathsf{inr}\,e)$	$\displaystyle\coloneqq\bot$

can be extended to a monadic container by taking

	$\displaystyle\iota$	$\displaystyle:=\mathsf{inl}\,\star$
	$\displaystyle\sigma\,(\mathsf{inl}\,\star)\,f$	$\displaystyle\coloneqq f\,\star$
	$\displaystyle\sigma\,(\mathsf{inr}\,e)\,\_$	$\displaystyle\coloneqq\mathsf{inr}\,e$
	$\displaystyle\mathsf{pr}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{\mathsf{inl}\,\star\}}\,\star$	$\displaystyle:=(\star,\star).$

This is another example of a $\Sigma$ -universe. The monad interpretation of this is known to the functional programming community as the exception monad.

Example 14 ( ).

Given a monoid $(A,\otimes,e)$ , the container $A\triangleleft\lambda\_.\top$ can be extended to a monadic container by taking

	$\displaystyle\iota$	$\displaystyle:=e$
	$\displaystyle\sigma\,a\,f$	$\displaystyle:=a\otimes f\,\star$
	$\displaystyle\mathsf{pr}\,\star$	$\displaystyle:=(\star,\star).$

The monadic container equalities hold as a consequence of the monoid equalities. We call this the writer monadic container. Monadic containers on $A\triangleleft\lambda\_.\top$ are in bijection with monoids on $A$ . The monad interpretation of this is typically called the writer monad.

We recall the definition of directed containers [5], for use in later sections of the paper.

Definition 15 ( ).

Let $S\triangleleft P$ be a container. A directed container on $S\triangleleft P$ is a tuple $(S\triangleleft P,o,\oplus,\downarrow)$ where

\displaystyle\begin{aligned} o&:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s:S\}}}P\,s\\ {\downarrow}&:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_% {s:S}P\,s\to S\\ \oplus&:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{p:P\,s}P\,(s% \downarrow p)\to P\,s\end{aligned}\qquad\qquad\begin{aligned} s\downarrow o&=s% \\ s\downarrow(p\oplus p^{\prime})&=(s\downarrow p)\downarrow p^{\prime}\\ p\oplus o&=p\\ o\oplus p&=p\\ (p\oplus p^{\prime})\oplus p^{\prime\prime}&=p\oplus(p^{\prime}\oplus p^{% \prime\prime}).\end{aligned}

(1)

4 Distributive laws

The question of whether two monads compose has applications in many areas. In functional programming and denotational semantics of effectful languages, for example, one might consider composition of two (or more) notions of side effect. As remarked in [34, Remark 1.1], distributive laws provide a particularly nice way to compose monads, that imbue the resulting composite monad with a variety of desirable properties.

Distributive laws were first introduced by Beck [11] as a sufficient condition for the composition of the underlying functors of two monads to carry a monad structure.

Definition 16.

Let $\mathbf{S}=(S,\eta^{S},\mu^{S})$ and $\mathbf{T}=(T,\eta^{T},\mu^{T})$ be monads. A distributive law of $\mathbf{S}$ over $\mathbf{T}$ is a natural transformation $\gamma:TS\Rightarrow ST$ such that the following diagrams commute.

In our approach, we specialise Definition 16 to the case when $S$ and $T$ are container functors, making $\mathbf{S}$ and $\mathbf{T}$ monads on container functors. We rely on the fact that both the container interpretation functor $\llbracket\_\rrbracket\colon\textul{\textbf{Cont}}\to[\textul{\textbf{Set}},% \textul{\textbf{Set}}]$ and the monadic container interpretation functor $\llbracket\_\rrbracket^{\text{mc}}\colon\textul{\textbf{MCont}}\to\textul{% \textbf{Monad}}(\textul{\textbf{Set}})$ are fully-faithful [3, 31], as well as monoidality of Cont and $\llbracket\_\rrbracket$ . This lets us directly interpret the diagrams in Definition 16 as diagrams in Cont, and gives us that each monadic container distributive law of $S\triangleleft P$ over $T\triangleleft Q$ corresponds to a unique monad distributive law of $\llbracket S\triangleleft P\rrbracket^{\text{mc}}$ over $\llbracket T\triangleleft Q\rrbracket^{\text{mc}}$ .

Definition 17 ( ).

Let $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ and $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ be monadic containers. A monadic container distributive law of $T\triangleleft Q$ over¹¹1The ordering of the monadic containers in this terminology follows that used by Beck. $S\triangleleft P$ is given by the data

	$\displaystyle u_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}(P\,s\to T)\to T$
	$\displaystyle u_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}% _{f:P\,s\to T}Q\,(u_{1}\,s\,f)\to S$
	$\displaystyle v_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}P\,(u_{2}\,s\,f\,q)\to P\,s$
	$\displaystyle v_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{p:P\,(u% _{2}\,s\,f\,q)}Q\,(f\,(v_{1}\,q\,p))$

which satisfy the following equalities.

$\displaystyle u_{1}\,\iota^{S}\,(\lambda\_.t)$	$\displaystyle=t$	(unit- $\iota S$ - $s_{1}$ )
$\displaystyle u_{2}\,\iota^{S}\,(\lambda\_.t)$	$\displaystyle=\lambda\_.\iota^{S}$	(unit- $\iota S$ - $s_{2}$ )
$\displaystyle v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\iota% ^{S}\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.t% \}}\,q\,p$	$\displaystyle=p$	(unit- $\iota S$ - $p_{1}$ )
$\displaystyle v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\iota% ^{S}\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.t% \}}\,q\,p$	$\displaystyle=q$	(unit- $\iota S$ - $p_{2}$ )
$\displaystyle u_{1}\,s\,(\lambda\_.\iota^{T})$	$\displaystyle=\iota^{T}$	(unit- $\iota T$ - $s_{1}$ )
$\displaystyle u_{2}\,s\,(\lambda\_.\iota^{T})$	$\displaystyle=\lambda\_.s$	(unit- $\iota T$ - $s_{2}$ )
$\displaystyle v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.\iota^{T}% \}}\,q\,p$	$\displaystyle=p$	(unit- $\iota T$ - $p_{1}$ )
$\displaystyle v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.\iota^{T}% \}}\,q\,p$	$\displaystyle=q$	(unit- $\iota T$ - $p_{2}$ )
$\displaystyle u_{1}\,(\sigma^{S}\,s\,f)\,(g\circ\mathsf{pr}^{S})$	$\displaystyle=u_{1}\,s\,(\lambda p.u_{1}\,(f\,p)\,(g\circ(p,-)))$	(mul- $S$ - $s_{1}$ )
$\displaystyle u_{2}\,(\sigma^{S}\,s\,f)\,(g\circ\mathsf{pr}^{S})\,q$	$\displaystyle=\sigma^{S}\,(u_{2}\,s\,(\lambda p.u_{1}\,(f\,p)\,(g\circ(p,-)))% \,q)$
	$\displaystyle\qquad\;\;\,(\lambda p.u_{2}\,(f\,(v_{1}\,q\,p))\,(g\circ(v_{1}\,% q\,p,-))\,(v_{2}\,q\,p))$	(mul- $S$ - $s_{2}$ )
$\displaystyle\mathsf{pr}^{S}_{1}\,(v_{1}\,q\,p)$	$\displaystyle=v_{1}\,q\,(\mathsf{pr}^{S}_{1}\,p)$	(mul- $S$ - $p_{1}$ )
$\displaystyle\mathsf{pr}^{S}_{2}\,(v_{1}\,q\,p)$	$\displaystyle=v_{1}\,(v_{2}\,q\,(\mathsf{pr}^{S}_{1}\,p))\,(\mathsf{pr}^{S}_{2% }\,p)$	(mul- $S$ - $p_{21}$ )
$\displaystyle v_{2}\,q\,p$	$\displaystyle=v_{2}\,(v_{2}\,q\,(\mathsf{pr}^{S}_{1}\,p))\,(\mathsf{pr}^{S}_{2% }\,p)$	(mul- $S$ - $p_{22}$ )
$\displaystyle u_{1}\,s\,(\lambda p.\sigma^{T}\,(f\,p)\,(g\circ(p,-)))$	$\displaystyle=\sigma^{T}\,(u_{1}\,s\,f)\,(\lambda q.u_{1}\,(u_{2}\,s\,f\,q)\,(% g\circ v\,q))$	(mul- $T$ - $s_{1}$ )
$\displaystyle u_{2}\,s\,(\lambda p.\sigma^{T}\,(f\,p)\,(g\circ(p,-)))\,q$	$\displaystyle=u_{2}\,(u_{2}\,s\,f\,(\mathsf{pr}^{T}_{1}\,q))\,(g\circ v\,q)\,(% \mathsf{pr}^{T}_{2}\,q)$	(mul- $T$ - $s_{2}$ )
$\displaystyle v_{1}\,(\mathsf{pr}^{T}_{1}\,q)\,(v_{1}\,(\mathsf{pr}^{T}_{2}\,q% )\,p)$	$\displaystyle=v_{1}\,q\,p$	(mul- $T$ - $p_{1}$ )
$\displaystyle v_{2}\,(\mathsf{pr}^{T}_{1}\,q)\,(v_{1}\,(\mathsf{pr}^{T}_{2}\,q% )\,p)$	$\displaystyle=\mathsf{pr}^{T}_{1}\,(v_{2}\,q\,p)$	(mul- $T$ - $p_{21}$ )
$\displaystyle v_{2}\,(\mathsf{pr}^{T}_{2}\,q)\,p$	$\displaystyle=\mathsf{pr}^{T}_{2}\,(v_{2}\,q\,p)$	(mul- $T$ - $p_{22}$ )

We will use the shorthands

	$\displaystyle u\,s\,f$	$\displaystyle\coloneqq(u_{1}\,s\,f,u_{2}\,s\,f)$
	$\displaystyle v\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,q\,p$	$\displaystyle\coloneqq(v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,q\,p,v_{2}\,{\color[rgb]{.5,.5,.5}% \definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5% }\pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{f\}}\,q\,p),$

primarily to simplify stating examples of distributive laws.

We refer to equalities whose names end in $s_{1}$ or $s_{2}$ collectively as “shape” equalities. The ones ending with names in $p_{1}$ , $p_{2}$ , $p_{21}$ , or $p_{22}$ are referred to collectively as “position” equalities.

These may seem rather unwieldy, but often in applications of this characterisation many of the equations simplify considerably. For example, when constructing a distributive law, if we define a $u_{1},u_{2}$ such that we can take $v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5% }\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,q\,p=p$ and $v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5% }\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,q\,p=q$ , then all the position equalities hold definitionally, and only the shape equalities must be proven (like in Example 18). The distributive law uniqueness lemmas (Lemmas 19, 21, and 31) and no-go theorem in Section 7 only require consideration of a few of these equalities.

While Definition 16 is a concise way of stating what a distributive law is, expanding this definition to check the naturality of $\gamma$ and commutativity of the 4 diagrams turns out to be cumbersome in practice. Further, our phrasing of distributive laws lends itself to formalisation in a proof assistant. In Cubical Agda, the dependencies between equations can be explicitly stated in terms of dependent paths, and we can prove properties of distributive laws without descending into “transport hell”.

Example 18 ( ).

There is a monadic container distributive law of $S\triangleleft P$ over $(\top+E)\triangleleft\text{Tr}$ , for any $E$ , $S$ , and $P$ , given by

	$\displaystyle u\,(\mathsf{inl}\,\star)\,f$	$\displaystyle\coloneqq(f\,\star,\lambda\_.\mathsf{inl}\,\star)$
	$\displaystyle u\,(\mathsf{inr}\,e)\,\_$	$\displaystyle\coloneqq(\iota^{S},\lambda\_.\mathsf{inr}\,e)$
	$\displaystyle v\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\mathsf{% inl}\,\star\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}% {.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,p\,\star$	$\displaystyle\coloneqq(\star,p).$

In fact, this is the only monadic container distributive law of this type, and the characterisation in Definition 17 offers a succinct proof of this:

Lemma 19 ( ).

The distributive law in Example 18 is the unique one of $S\triangleleft P$ over $(\top+E)\triangleleft\text{Tr}$ for any $E$ , $S$ , and $P$ .

Proof.

We first note that $(\top\to S)\cong S$ , and that $\bot\to S$ is contractible ( $(\bot\to S)\cong\top$ , since it has a point $\lambda\_.\iota^{S}$ ). Using these facts and the equalities unit- $\iota S$ - $s_{1}$ , unit- $\iota S$ - $s_{2}$ , unit- $\iota T$ - $s_{1}$ , and unit- $\iota T$ - $s_{2}$ , $u$ is uniquely specified up to function extensionality. We can use the same reasoning and laws unit- $\iota S$ - $p_{1}$ and unit- $\iota S$ - $p_{2}$ to see that $v$ is also uniquely specified up to function extensionality. $\hfill\blacktriangleleft$

Example 20 ( ).

There is a monadic container distributive law of $\top\triangleleft\lambda\_.A$ over $S\triangleleft P$ for any $A$ , $S$ , and $P$ given by

	$\displaystyle u\,s\,f$	$\displaystyle\coloneqq(\star,\lambda\_.s)$
	$\displaystyle v\,a\,p$	$\displaystyle\coloneqq(p,a).$

Lemma 21 ( ).

The distributive law in Example 20 is the unique one of $\top\triangleleft\lambda\_.A$ over $S\triangleleft P$ for any $A$ , $S$ , and $P$ .

Proof.

Follows from the isomorphisms $\top\cong(P\,s\to\top)$ for any $s : S$ , and the unit- $\iota T$ - $\dots$ equalities for monadic container distributive laws. $\hfill\blacktriangleleft$

Ahman and Uustalu in [6] noticed that distributive laws of directed containers generalise matching pairs of monoid actions, and the composition of directed containers via a distributive law generalises the Zappa-Szép product of monoids [12]. The following example shows how distributive laws and composition of monadic containers generalise the same constructions, but in a slightly different way, which is unsurprising but nice to see.

Example 22.

Given monoids $(A,\otimes^{A},\iota^{A})$ and $(B,\otimes^{B},\iota^{B})$ , and a matching pair of monoid actions $(\alpha:A\times B\to A,\beta:A\times B\to B)$ , there is a distributive law of $B\triangleleft\lambda\_.\top$ over $A\triangleleft\lambda\_.\top$ given by

	$\displaystyle u\,a\,b$	$\displaystyle\coloneqq(\beta\,(a,b\,\star),\lambda\_.\alpha\,(a,b\,\star))$
	$\displaystyle v\,\star\,\star$	$\displaystyle\coloneqq(\star,\star)$

where the distributive law equalities follow from the equalities for the matching pair of monoid actions (up to the isomorphism $(\top\to B)\cong B$ ). Conversely, any distributive law of this type specifies a matching pair of monoid actions for the relevant monoids.

5 Composing with distributive laws

Along with distributive laws, Beck also introduced the equivalent notion of compatible composites [11], as a way to specify when a given monad can be considered a composite of two others. In this section, we characterise these in terms of monadic containers. Often, we will use the shorthand $\Diamond^{P}_{Q}:=\lambda(s,f).\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\sum$}}}_{p:P\,s}Q\,(f\,p)$ to simplify the presentation of nested $\Sigma$ -types.

Definition 23 ( ).

A compatible composite monadic container of $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ over $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ is a pair of maps

	$\displaystyle\sigma:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{x:[\![S\triangleleft P]\!]\,T}(\Diamond^{P}_{Q}\,x\to[\![S% \triangleleft P]\!]\,\,T)\to[\![S\triangleleft P]\!]\,\,T$
	$\displaystyle\mathsf{pr}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$% \displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{x:[\![S\triangleleft P]\!]\,T\}}}\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{.5,.5,.5% }\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.% 5}\pgfsys@color@gray@fill{.5}\{f:\Diamond^{P}_{Q}\,x\to[\![S\triangleleft P]\!% ]\,\,T\}}}\Diamond^{P}_{Q}\,(\sigma\,x\,f)\to\mathop{\raisebox{0.0pt}{% \scalebox{1.0}{$\displaystyle\sum$}}}_{p:\Diamond^{P}_{Q}\,x}\Diamond^{P}_{Q}% \,(f\,p)$

where:

$\blacksquare$

$((S\triangleleft P)\circ(T\triangleleft Q),(\iota^{S},\lambda\_.\iota^{T}),% \sigma,\mathsf{pr})$ is a monadic container
$\blacksquare$

the container morphisms $\lambda s.(s,\lambda\_.\iota^{T})\lhd\pi_{1}$ and $\lambda t.(\iota^{S},\lambda\_.t)\lhd\pi_{2}$ are monadic container morphisms, as defined in [31]
$\blacksquare$

the middle unitary laws hold:

$\displaystyle(s,f)$ $\displaystyle=\sigma\,(s,\lambda\_.\iota^{T})\,(\lambda p.(\iota^{S},\lambda\_% .f\,(\pi_{1}\,p)))$

$\displaystyle(q,p)$ $\displaystyle=(\pi_{1}\,(\mathsf{pr}_{1}\,(q,p)),\pi_{2}\,(\mathsf{pr}_{2}\,(q% ,p)))$

where the second equality is dependent on the first.

Distributive laws of monadic containers and their interpreting monads are in bijection due to $\llbracket\_\rrbracket\colon\textul{\textbf{Cont}}\to[\textul{\textbf{Set}},% \textul{\textbf{Set}}]$ being full and faithful. Compatible composite monadic containers and their interpreting monads are also in bijection, since $\sigma\triangleleft\mathsf{pr}$ is a container morphism, the collection of which is in bijection with natural transformations between container functors, again by $\llbracket\_\rrbracket$ being full and faithful. Therefore, Beck’s result that in the monad setting distributive laws and compatible composites are equivalent also immediately implies that they are equivalent in the monadic container setting. However, we would still like to give a direct construction of the compatible composite monadic container we obtain from a monadic container distributive law, and vice versa.

Proposition 24 (Compatible composite from a distributive law, partially formalised ).

Given monadic containers $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ and $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ , and a monadic container distributive law $(u_{1},u_{2},v_{1},v_{2})$ of $S\triangleleft P$ over $T\triangleleft Q$ , we have a compatible composite monadic container given by

$\displaystyle\sigma\,(s,f)\,g$	$\displaystyle\coloneqq\$	$\displaystyle($	$\displaystyle\sigma^{S}\,s\,(\lambda p.u_{1}\,(f\,p)\,(g_{1}\circ(p,-))),$
	$\displaystyle\lambda p.\sigma^{T}\,(u_{2}\,(f\,(\mathsf{pr}^{S}_{1}\,p))\,(g_{% 1}\circ(\mathsf{pr}^{S}_{1}\,p,-))\,(\mathsf{pr}^{S}_{2}\,p))$
	$\displaystyle\quad\;(\lambda q.g_{2}\,(\mathsf{pr}^{S}_{1}\,p,v_{1}\,(\mathsf{% pr}^{S}_{2}\,p)\,q)\,(v_{2}\,(\mathsf{pr}^{S}_{2}\,p)\,q)))$
$\displaystyle\mathsf{pr}\,(p,q)$	$\displaystyle\coloneqq\$	$\displaystyle($	$\displaystyle(\mathsf{pr}^{S}_{1}\,p,v_{1}\,(\mathsf{pr}^{S}_{2}\,p)\ (\mathsf% {pr}^{T}_{1}\,q)),$
	$\displaystyle(v_{2}\,(\mathsf{pr}^{S}_{2}\,p)\,(\mathsf{pr}^{T}_{1}\,q),% \mathsf{pr}^{T}_{2}\,q))$

where $g_{i}\coloneqq\pi_{i}\circ g$ .

Proof.

Derivations of the “associativity” equalities are in Appendix A. Proofs of the remaining equalities are included in the Cubical Agda formalisation. $\hfill\blacktriangleleft$

Proposition 25 (Distributive law from a compatible composite).

Given monadic containers $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ and $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ , and a compatible composite monadic container $(\sigma,\mathsf{pr})$ of $S\triangleleft P$ over $T\triangleleft Q$ , then we have a monadic container distributive law given by

	$\displaystyle u\,s\,f$	$\displaystyle\coloneqq\sigma\,(\iota^{T},\lambda\_.s)\,(\lambda\,p.(f\,(\pi_{2% }\,p),\lambda\_.\iota^{S}))$
	$\displaystyle v\,q\,p$	$\displaystyle\coloneqq(\pi_{2}\,(\mathsf{pr}_{1}\,(q,p)),\pi_{1}\,(\mathsf{pr}% _{2}\,(q,p))).$

To see that Proposition 24 generalises the Zappa-Szép product of monoids, we consider the case in Example 22 of a distributive law between two writer monadic containers $A\triangleleft\lambda\_.\top$ and $B\triangleleft\lambda\_.\top$ . The resulting compatible composite monadic container (constructed using Proposition 24) is again a writer monadic container $(A\times B)\triangleleft\lambda\_.\top$ , whose corresponding monoid is a Zappa-Szép product of the monoids corresponding to $A\triangleleft\lambda\_.\top$ and $B\triangleleft\lambda\_.\top$ .

Example 26.

Given a set $A$ and monadic container $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ , the compatible composite monadic container of $\top\triangleleft\lambda\_.A$ over $S\triangleleft P$ arising from the distributive law in Example 20 is given by

	$\displaystyle\sigma\,(\star,f)\,g$	$\displaystyle\coloneqq(\star,\lambda a.\sigma^{S}\,(f\,a)\,(\lambda p.\pi_{2}% \,(g\,(a,p)\,a)))$
	$\displaystyle\mathsf{pr}\,(a,p)$	$\displaystyle\coloneqq((a,\mathsf{pr}^{S}_{1}\,p),(a,\mathsf{pr}^{S}_{2}\,p)).$

On a different note, composite monadic containers can be useful for considering extensions of $(1,\Sigma)$ type universes (modelled by $\Sigma$ -universes [9]). As an example, we consider how to augment a $\Sigma$ -universe $(\mathcal{U}\triangleleft\text{El},\iota^{\mathcal{U}},\mathsf{un}^{\mathcal{U% }},\sigma^{\mathcal{U}},\mathsf{pr}^{\mathcal{U}})$ with codes for refinement types [19]. This can be done by considering compatible composites of $\mathcal{U}\triangleleft\text{El}$ over the “Maybe” $\Sigma$ -universe (Example 13 where $E=\top$ ).

Example 27.

Given a $\Sigma$ -universe $(\mathcal{U}\triangleleft\text{El},\iota^{\mathcal{U}},\mathsf{un}^{\mathcal{U% }},\sigma^{\mathcal{U}},\mathsf{pr}^{\mathcal{U}})$ , the composite monadic container corresponding to Example 18 when $E=\top$ is

	$\displaystyle\hskip-7.0pt\iota$	$\displaystyle\coloneqq(\iota^{\mathcal{U}},\lambda\_.\text{true})$
	$\displaystyle\hskip-7.0pt\sigma\,(s,f)\,g$	$\displaystyle\coloneqq\Big{(}\sigma^{\mathcal{U}}\,s\,\Big{(}\lambda p.\begin{% cases}g_{1}\,(p,\star)&\text{if }f\,p=\text{true}\\ \iota^{\mathcal{U}}&\text{otherwise}\end{cases}\Big{)},\lambda p.\begin{cases}% g_{2}\,(\mathsf{pr}_{1}^{\mathcal{U}}\,p,\star)\,(\mathsf{pr}_{2}^{\mathcal{U}% }\,p)&\text{if }f\,(\mathsf{pr}_{1}^{\mathcal{U}}\,p)=\text{true}\\ \text{false}&\text{otherwise}\end{cases}\Big{)}$
	$\displaystyle\hskip-7.0pt\mathsf{pr}\,(p,\star)$	$\displaystyle\coloneqq((\mathsf{pr}^{\mathcal{U}}_{1}\,p,\star),(\mathsf{pr}^{% \mathcal{U}}_{2}\,p,\star))$

where $\text{true}:=\mathsf{inl}\,\star$ and $\text{false}:=\mathsf{inr}\,\star$ . This composite monadic container is also a $\Sigma$ -universe, as $\mathsf{pr}$ is an isomorphism (since $\mathsf{pr}^{\mathcal{U}}$ is an iso) and we have that $\Diamond^{\text{El}}_{\text{Tr}}\,\iota\cong\top$ (since $\mathsf{un}^{\mathcal{U}}$ is an iso).

To see how shapes in the above composite encode refinement types, consider a shape $(s,f):\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\sum$}}}_{s:% \mathcal{U}}\text{El}\,{s}\to(\top+\top)$ . The shape $s$ is a code for the type $\text{El}\,{s}$ , and we can see $f$ as a predicate on elements of $\text{El}\,{s}$ . The type that $(s,f)$ encodes is $\Diamond^{\text{El}}_{\text{Tr}}\,(s,f)\coloneqq\mathop{\raisebox{0.0pt}{% \scalebox{1.0}{$\displaystyle\sum$}}}_{x:\text{El}\,{s}}\text{Tr}\,(f\,x)$ , whose elements are essentially the elements of $\text{El}\,{s}$ for which the predicate $f$ holds.

This is an “augmentation” in the sense that all types encoded by $\mathcal{U}$ have unique codes in the composite universe. Given a shape $s:\mathcal{U}$ , the composite shape $(s,\lambda\_.\text{true})$ codes for the type with elements from $\text{El}\,{s}$ that satisfy the “always true” predicate – this is clearly isomorphic to the type $\text{El}\,{s}$ .

6 Mixed distributive laws

By combining our characterisation of monadic container distributive laws with Ahman and Uustalu’s directed container distributive laws [6, Section 4] ( ), it is straightforward to obtain a characterisation of mixed container distributive laws.

Definition 28 ( ).

Let $(T\triangleleft Q,\iota,\sigma,\mathsf{pr})$ be a monadic container and $(S\triangleleft P,o,\oplus,\downarrow)$ be a directed container. We define a monadic-directed container distributive law of $T\triangleleft Q$ over $S\triangleleft P$ as the data

	$\displaystyle u_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}(P\,s\to T)\to T$
	$\displaystyle u_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}% _{f:P\,s\to T}Q\,(u_{1}\,s\,f)\to S$
	$\displaystyle v_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}P\,(u_{2}\,s\,f\,q)\to P\,s$
	$\displaystyle v_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{p:P\,(u% _{2}\,s\,f\,q)}Q\,(f\,(v_{1}\,q\,p))$

which satisfy the following equalities.

$\displaystyle u_{1}\,s\,f$	$\displaystyle=f\,(o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}})$	(unit- $o S$ - $s$ )
$\displaystyle v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,q\,(o\,{\color% [rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{u_{2}\,s\,f\,q\}})$	$\displaystyle=o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}$	(unit- $o S$ - $p_{1}$ )
$\displaystyle v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f\}}\,q\,(o\,{\color% [rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{u_{2}\,s\,f\,q\}})$	$\displaystyle=q$	(unit- $o S$ - $p_{2}$ )
$\displaystyle u_{2}\,s\,f\,q\downarrow p$	$\displaystyle=u_{2}\,(s\downarrow v_{1}\,q\,p)\,(\lambda p^{\prime}.f\,(v_{1}% \,q\,p\oplus p^{\prime}))\,(v_{2}\,q\,p)$	(mul- $S$ - $s_{3}$ )
$\displaystyle v_{1}\,q\,(p\oplus p^{\prime})$	$\displaystyle=v_{1}\,q\,p\oplus v_{1}\,(v_{2}\,q\,p)\,p^{\prime}$	(mul- $S$ - $p_{1}$ )
$\displaystyle v_{2}\,q\,(p\oplus p^{\prime})$	$\displaystyle=v_{2}\,(v_{2}\,q\,p)\,p^{\prime}$	(mul- $S$ - $p_{2}$ )
$\displaystyle u_{2}\,s\,(\lambda\_.\iota^{T})$	$\displaystyle=\lambda\_.s$	(unit- $\iota T$ - $s_{2}$ )
$\displaystyle v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.\iota^{T}% \}}\,q\,p$	$\displaystyle=p$	(unit- $\iota T$ - $p_{1}$ )
$\displaystyle v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}% \,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.\iota^{T}% \}}\,q\,p$	$\displaystyle=q$	(unit- $\iota T$ - $p_{2}$ )
$\displaystyle u_{2}\,s\,(\lambda p.\sigma^{T}\,(f\,p)\,(g\circ(p,-)))\,q$	$\displaystyle=u_{2}\,(u_{2}\,s\,f\,(\mathsf{pr}^{T}_{1}\,q))\,(g\circ v\,q)\,(% \mathsf{pr}^{T}_{2}\,q)$	(mul- $T$ - $s_{2}$ )
$\displaystyle v_{1}\,(\mathsf{pr}^{T}_{1}\,q)\,(v_{1}\,(\mathsf{pr}^{T}_{2}\,q% )\,p)$	$\displaystyle=v_{1}\,q\,p$	(mul- $T$ - $p_{1}$ )
$\displaystyle v_{2}\,(\mathsf{pr}^{T}_{1}\,q)\,(v_{1}\,(\mathsf{pr}^{T}_{2}\,q% )\,p)$	$\displaystyle=\mathsf{pr}^{T}_{1}\,(v_{2}\,q\,p)$	(mul- $T$ - $p_{21}$ )
$\displaystyle v_{2}\,(\mathsf{pr}^{T}_{2}\,q)\,p$	$\displaystyle=\mathsf{pr}^{T}_{2}\,(v_{2}\,q\,p)$	(mul- $T$ - $p_{22}$ )

Notice that the first six equations are taken from directed container distributive laws, and the remaining equations from monadic container distributive laws. As in directed container distributive laws, the unit- $o S$ - $s$ equality fully determines $u_{1}$ .

Directed-monadic container distributive laws (of a directed container over a monadic container) can be derived in a similar fashion.

Definition 29 ( ).

Let $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ be a monadic container and $(T\triangleleft Q,o,\oplus,\downarrow)$ be a directed container. We define a directed-monadic container distributive law of $T\triangleleft Q$ over $S\triangleleft P$ as the data

	$\displaystyle u_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}(P\,s\to T)\to T$
	$\displaystyle u_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{s:S}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}% _{f:P\,s\to T}Q\,(u_{1}\,s\,f)\to S$
	$\displaystyle v_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}P\,(u_{2}\,s\,f\,q)\to P\,s$
	$\displaystyle v_{2}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle% \prod$}}}_{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s:S\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:P\,s\to T\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{q:Q\,(u_{1}\,% s\,f)}\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{p:P\,(u% _{2}\,s\,f\,q)}Q\,(f\,(v_{1}\,q\,p))$

which satisfy the following equalities.

$\displaystyle u_{1}\,\iota^{S}\,(\lambda\_.t)$	$\displaystyle=t$	(unit- $\iota S$ - $s_{1}$ )
$\displaystyle u_{2}\,\iota^{S}\,(\lambda\_.t)$	$\displaystyle=\lambda\_.\iota^{S}$	(unit- $\iota S$ - $s_{2}$ )
$\displaystyle v_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\iota% ^{S}\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.t% \}}\,q\,p$	$\displaystyle=p$	(unit- $\iota S$ - $p_{1}$ )
$\displaystyle v_{2}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}% {rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\iota% ^{S}\}}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{% .5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\lambda\_.t% \}}\,q\,p$	$\displaystyle=q$	(unit- $\iota S$ - $p_{2}$ )
$\displaystyle u_{1}\,(\sigma^{S}\,s\,f)\,(g\circ\mathsf{pr}^{S})$	$\displaystyle=u_{1}\,s\,(\lambda p.u_{1}\,(f\,p)\,(g\circ(p,-)))$	(mul- $S$ - $s_{1}$ )
$\displaystyle u_{2}\,(\sigma^{S}\,s\,f)\,(g\circ\mathsf{pr}^{S})\,q$	$\displaystyle=\sigma^{S}\,(u_{2}\,s\,(\lambda p.u_{1}\,(f\,p)\,(g\circ(p,-)))% \,q)$
	$\displaystyle\qquad\;\;\,(\lambda p.u_{2}\,(f\,(v_{1}\,q\,p))\,(g\circ(v_{1}\,% q\,p,-))\,(v_{2}\,q\,p))$	(mul- $S$ - $s_{2}$ )
$\displaystyle\mathsf{pr}^{S}_{1}\,(v_{1}\,q\,p)$	$\displaystyle=v_{1}\,q\,(\mathsf{pr}^{S}_{1}\,p)$	(mul- $S$ - $p_{1}$ )
$\displaystyle\mathsf{pr}^{S}_{2}\,(v_{1}\,q\,p)$	$\displaystyle=v_{1}\,(v_{2}\,q\,(\mathsf{pr}^{S}_{1}\,p))\,(\mathsf{pr}^{S}_{2% }\,p)$	(mul- $S$ - $p_{21}$ )
$\displaystyle v_{2}\,q\,p$	$\displaystyle=v_{2}\,(v_{2}\,q\,(\mathsf{pr}^{S}_{1}\,p))\,(\mathsf{pr}^{S}_{2% }\,p)$	(mul- $S$ - $p_{22}$ )
$\displaystyle u_{2}\,s\,f\,(o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{u_{1}\,s\,f\}})$	$\displaystyle=s$	(unit- $o T$ - $s$ )
$\displaystyle v_{1}\,(o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{u_{1}\,s\,f\}})\,p$	$\displaystyle=p$	(unit- $o T$ - $p_{1}$ )
$\displaystyle v_{2}\,(o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{% pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}% \pgfsys@color@gray@fill{.5}\{u_{1}\,s\,f\}})\,p$	$\displaystyle=o\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}$	(unit- $o T$ - $p_{2}$ )
$\displaystyle u_{1}\,s\,f\downarrow q$	$\displaystyle=u_{1}\,(u_{2}\,s\,f\,q)\,(\lambda p.f\,(v_{1}\,q\,p)\downarrow v% _{2}\,q\,p)$	(mul- $T$ - $s_{1}$ )
$\displaystyle u_{2}\,s\,f\,(q\oplus q^{\prime})$	$\displaystyle=u_{2}\,(u_{2}\,s\,f\,q)\,(\lambda p.f\,(v_{1}\,q\,p)\downarrow v% _{2}\,q\,p)\,q^{\prime}$	(mul- $T$ - $s_{2}$ )
$\displaystyle v_{1}\,(q\oplus q^{\prime})\,p$	$\displaystyle=v_{1}\,q\,(v_{1}\,q^{\prime}\,p)$	(mul- $T$ - $p_{1}$ )
$\displaystyle v_{2}\,(q\oplus q^{\prime})\,p$	$\displaystyle=v_{2}\,q\,(v_{1}\,q^{\prime}\,p)\oplus v_{2}\,q^{\prime}\,p$	(mul- $T$ - $p_{2}$ )

Example 30 ( ).

There is a monadic-directed distributive law of the reader monadic container $\top\triangleleft\lambda\_.B$ over the writer directed container $A\triangleleft\lambda\_.\top$ for any sets $A$ and $B$ , given by

	$\displaystyle u\,a\,f:=(\star,\lambda\_.a)$
	$\displaystyle v\,b\,\star:=(\star,b).$

Lemma 31 ( ).

The mixed distributive law in Example 30 is the unique one of $\top\triangleleft\lambda\_.B$ over $A\triangleleft\lambda\_.\top$ .

Proof.

Follows from the isomorphism $(\top\to\top)\cong\top$ and then directly from the unit- $\iota T$ equations of monadic-directed distributive laws. $\hfill\blacktriangleleft$

It is thematically appropriate to check if these mixed distributive laws correspond to any known constructions on monoids.

For monadic-directed distributive laws, we can do this by specialising the mixed distributive law to the case of $B\lhd\lambda\_.\top$ over $\top\lhd\lambda\_.A$ , where $\top\lhd\lambda\_.A$ is the reader directed container for a monoid $(A,e^{A},\oplus^{A})$ , and $B\lhd\lambda\_.\top$ is the writer monadic container for a monoid $(B,e^{B},\oplus^{B})$ . $u_{2}$ and $v_{2}$ trivialise, $u_{1}$ is uniquely defined as $u_{1}\,s\,f=f\,e^{A}$ , and the only parameter we are left with is

v_{1}:\mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color% [rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{\star:\top\}}}% \mathop{\raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{{\color[rgb]{% .5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f:A\to B\}}}\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{\star:\top}\,\mathop{% \raisebox{0.0pt}{\scalebox{1.0}{$\displaystyle\prod$}}}_{a:A}\,A.

Possible values of $v_{1}$ in this case are in bijection with functions $\alpha:(A\to B)\to A\to A$ , satisfying the equations:

	$\displaystyle\alpha\,f\,e^{A}$	$\displaystyle=e^{A}$
	$\displaystyle\alpha\,f\,(a\oplus^{A}a^{\prime})$	$\displaystyle=\alpha\,f\,a\oplus^{A}\alpha\,(\lambda x.f\,(\alpha\,f\,a\oplus^% {A}x))\,a^{\prime}$
	$\displaystyle\alpha\,(\lambda\_.e^{B})\,a$	$\displaystyle=a$
	$\displaystyle\alpha\,(\lambda x.f\,x\oplus^{B}g\,x)\,a$	$\displaystyle=\alpha\,f\,(\alpha\,(\lambda x.g\,(\alpha\,f\,x))\,a).$

Counterintuitively, we do not end up with a matching pair of monoid actions! Instead we have something that we could call a “functional monoid action” ( ) of the function space $A\to B$ on the monoid $A$ . We have not come across this construction in the literature, but we would not be surprised if it was already known to algebraists.

Despite this, when we specialise directed-monadic container distributive laws to those between writer monadic containers and reader directed containers, we find that they are in bijection with matching pairs of monoid actions.

In summary, by restricting distributive laws to those between certain monadic and directed containers (those that are in bijection with monoids), we obtain corresponding constructions on monoids. The table below records the constructions obtained by considering distributive laws of each row container over each column container.

	Writer monadic container	Reader directed container
Writer monadic container	Matching pairs	Functional monoid actions
Reader directed container	Matching pairs	Matching pairs

This highlights an interesting asymmetry, however the reason for this asymmetry is not immediately obvious to us.

7 A no-go theorem

To show that our characterisation in Definition 17 is amenable to developing theorems concerning non-existence of distributive laws, we look to Zwart and Marsden [34] for approaches to developing no-go theorems that we may be able to emulate.

To do this, we first need to translate properties of and statements about algebraic theories, into those for monadic containers. Our strategy for this translation was to very loosely view aspects of a monadic container as analogous to aspects of an algebraic theory:

$\blacksquare$

shapes are “terms”
$\blacksquare$

positions are “variables within a term”
$\blacksquare$

$\sigma$ is the “substitution operator”
$\blacksquare$

$\iota$ is a “variable placeholder”
$\blacksquare$

$\mathsf{pr}$ is a map from “variable positions in a term resulting from a substitution” to “variable positions in the terms that were involved in that substitution”.

The point of this is not to form a rigorous connection between monadic containers and algebraic theories, but to see if there are common patterns that can be quickly taken advantage of. As it turns out, this loose perspective provides sufficient intuition to emulate the “too many constants” theorem about non-existence of certain composite algebraic theories in [34, Theorem 4.6] in our setting.

Definition 32 ( ).

Given a monadic container $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ we call any shape $s : S$ where $P\,s\cong\bot$ a constant shape.

Definition 33 ( ).

A monadic container $(S\triangleleft P,\iota,\sigma,\mathsf{pr})$ satisfies the (S3) property if there exist $s : S$ and $f:P\,s\to S$ such that $P\,s$ is non-empty, equality on $P\,s$ is decidable, and for any $p:P\,s$

\sigma\,s\,f^{p}=\iota

and for any $p^{\prime}:P\,(\sigma\,s\,f^{p})$ we have

\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{s\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f^{p}\}}\,p^{\prime}=p

where we use the notation

f^{p}:=\lambda p^{\prime}.\begin{cases}\iota&\text{if }p=p^{\prime}\\ f\,p^{\prime}&\text{otherwise}\end{cases}

The name of this property is taken from the analogous property of algebraic theories in [34, Section 4]. In particular, the list monadic container $\mathbb{N}\triangleleft\mathsf{Fin}\;$ satisfies (S3) by taking any $n:\mathbb{N}$ except $0$ , and taking $f:=\lambda\_.0$ . Since you can pick any $n:\mathbb{N}$ where $\mathsf{Fin}\;\,n$ is non-empty, this container actually satisfies a stronger property, directly analogous to (S4) in [34, Section 4]. An interesting almost-example is the state monadic container $(S\to S)\triangleleft\lambda\_.S$ for $S$ with decidable equality, which satisfies the shape equation of (S3) by taking $s:=\lambda x.x$ and $f:=\lambda xy.y$ , but not the position equation (unless $S$ is trivial).

Lemma 34 (Composite (S3), ).

Let $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ be a monadic container satisfying (S3) for some $s : S$ and $f:P\,s\to S$ , and $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ be a monadic container. Assume we have a monadic container distributive law $(u_{1},u_{2},v_{1},v_{2})$ of $S\triangleleft P$ over $T\triangleleft Q$ . Then, for any $t : T$ and $p:P\,s$ ,

u_{1}\,s\,\Big{(}\lambda p^{\prime}.\begin{cases}t&\text{if }p^{\prime}=p\\ \iota^{T}&\text{otherwise}\end{cases}\Big{)}=t.

Proof.

Proof included in Appendix B. $\hfill\blacktriangleleft$

Theorem 35 (Too many constants, ).

Let $(S\triangleleft P,\iota^{S},\sigma^{S},\mathsf{pr}^{S})$ be a monadic container satisfying (S3) for some $s : S$ and $f:P\,s\to S$ , such that we have two distinct positions $p,p^{\prime}:P\,s$ , and let $(T\triangleleft Q,\iota^{T},\sigma^{T},\mathsf{pr}^{T})$ be a monadic container. Assume we have a monadic container distributive law $(u_{1},u_{2},v_{1},v_{2})$ of $S\triangleleft P$ over $T\triangleleft Q$ . Then $T\triangleleft Q$ cannot have more than one distinct constant shape.

Proof.

Proof included in Appendix B. $\hfill\blacktriangleleft$

With this theorem we can obtain the known result that there are no distributive laws of the list monad over the coproduct monad.

Example 36.

Let $E$ be a set with at least two elements $e_{1},e_{2}:E$ such that $e_{1}\neq e_{2}$ . By Theorem 35, there is no monadic container distributive law of the list monadic container $\mathbb{N}\triangleleft\mathsf{Fin}\;$ over the coproduct monadic container $(\top+E)\triangleleft\text{Tr}$ .

The scope of this theorem is slightly different to Zwart and Marsden’s theorem of the same name, as it concerns a different class of monads – those presentable as monadic containers, rather than algebraic theories. It is possible to represent any monad on Set as a generalised algebraic theory [22], but it is not immediately clear how to transfer no-go theorems for compositions of algebraic theories into that setting.

8 Conclusion

We have characterised monadic, monadic-directed, and directed-monadic container distributive laws, and have motivated their use for development of uniqueness and existence proofs. Further, we have shown such proofs to be amenable to mechanisation in a proof assistant.

Looking at the constructions on monoids that each of these distributive laws generalise, we note a curious asymmetry. Monadic-directed container distributive laws correspond to the notion of “functional monoid action”, as opposed to matching pairs of monoid actions, which all other kinds of distributive law we consider correspond to.

Our work dualises that of Ahman and Uustalu in [6], completing the set of characterisations for container (co)monads and their distributive laws, but there are clearly further directions to explore. All of our characterisations and those in [5, 6, 31] could be extended to symmetric (or groupoid) containers [17], or further to categorified containers [17, 7] to describe a larger class of (co)monads and their distributive laws. For example, it seems possible to represent the finite multiset monad using groupoid containers. We intend to explore this direction in future work.

In Example 27, we touch on the connection between type universes and monadic containers. This perspective could be further explored, using this work as a starting point. For example, one could consider developing a notion of composition for type universes with not only codes for $\top$ and $\Sigma$ , but also for $\Pi$ types.

References

[1] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of containers. In Andrew D. Gordon, editor, Foundations of Software Science and Computation Structures, pages 23–38, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.
[2] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Representing nested inductive types using W-types. In Automata, Languages and Programming, 31st International Colloqium (ICALP), pages 59–71, 2004. doi:10.1007/978-3-540-27836-8_8.
[3] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3–27, September 2005. doi:10.1016/j.tcs.2005.06.002.
[4] Danel Ahman. An Agda formalisation of the theory of directed containers. https://github.com/danelahman/Directed-Containers, 2011. Online.
[5] Danel Ahman, James Chapman, and Tarmo Uustalu. When is a container a comonad? In Lars Birkedal, editor, Foundations of Software Science and Computational Structures, pages 74–88, Berlin, Heidelberg, 2012. Springer. doi:10.1007/978-3-642-28729-9_5.
[6] Danel Ahman and Tarmo Uustalu. Distributive laws of directed containers. Progress in Informatics, (10):3–18, March 2013. doi:10.2201/NiiPi.2013.10.2.
[7] Thorsten Altenkirch. Quotient inductive types as categorified containers. https://hott-uf.github.io/2024/abstracts/HoTTUF_2024_paper_10.pdf, 2024. HoTT/UF 2024 abstract.
[8] Thorsten Altenkirch and Peter Morris. Indexed containers. In 2009 24th Annual IEEE Symposium on Logic In Computer Science, pages 277–285, 2009. doi:10.1109/LICS.2009.33.
[9] Thorsten Altenkirch and Gun Pinyo. Monadic containers and $\Sigma$ -universes. https://types2017.elte.hu/proc.pdf#page=28, https://people.cs.nott.ac.uk/psztxa/talks/types-17-cont.pdf, 2017. TYPES 2017 abstract and slides.
[10] Steve Awodey. Natural models of homotopy type theory. Math. Struct. Comput. Sci., 28(2):241–286, 2018. doi:10.1017/S0960129516000268.
[11] Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. doi:10.1007/BFb0083084.
[12] Matthew G. Brin. On the Zappa-Szép Product. Communications in Algebra, 33(2):393–424, February 2005. doi:10.1081/agb-200047404.
[13] Alexander Bunkenburg. The Boom Hierarchy, pages 1–8. Springer London, London, 1994. doi:10.1007/978-1-4471-3236-3_1.
[14] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.TYPES.2015.5.
[15] Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, pages 210–225, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-24849-1_14.
[16] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, January 2013. arXiv:0906.4931 [math]. doi:10.1017/S0305004112000394.
[17] Håkon Robbestad Gylterud. Symmetric containers. Master’s thesis, University of Oslo, 2011.
[18] Paul Hudak, Simon Peyton Jones, Philip Wadler, Brian Boutel, Jon Fairbairn, Joseph Fasel, María M. Guzmán, Kevin Hammond, John Hughes, Thomas Johnsson, Dick Kieburtz, Rishiyur Nikhil, Will Partain, and John Peterson. Report on the programming language haskell: a non-strict, purely functional language version 1.2. SIGPLAN Not., 27(5):1–164, May 1992. doi:10.1145/130697.130699.
[19] Ranjit Jhala and Niki Vazou. Refinement types: A tutorial, 2020. arXiv:2010.07763.
[20] Amin Karamlou and Nihil Shah. No go theorems: Directed containers that do not distribute over distribution monads. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, pages 1–13, New York, NY, USA, July 2024. Association for Computing Machinery. doi:10.1145/3661814.3662137.
[21] Joachim Kock. Notes on polynomial functors, 2009. Unpublished notes.
[22] E.G. Manes. Algebraic Theories. Springer Science & Business Media, 2012. doi:10.1007/978-1-4612-9860-1.
[23] Ernie Manes and Philip Mulry. Monad compositions I: General constructions and recursive distributive laws. Theory and Applications of Categories, 18:172–208, 2007.
[24] Ernie Manes and Philip Mulry. Monad compositions II: Kleisli strength. Mathematical Structures in Computer Science, 18(3):613–643, June 2008. doi:10.1017/S0960129508006695.
[25] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991. Selections from 1989 IEEE Symposium on Logic in Computer Science. doi:10.1016/0890-5401(91)90052-4.
[26] Chris Purdy and Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers. Software, swhId: swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a (visited on 2025-07-21). URL: https://github.com/chrisjpurdy/distr-laws-of-monadic-containers, doi:10.4230/artifacts.24062.
[27] Chris Purdy and Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers HTML rendering. Software (visited on 2025-07-21). URL: https://stefaniatadama.com/distr-law-mnd-cont-html/, doi:10.4230/artifacts.24064.
[28] Chris Purdy and Stefania Damato. stefaniatadama/cubical. Software (visited on 2025-07-21). URL: https://github.com/stefaniatadama/cubical/tree/distr-laws, doi:10.4230/artifacts.24065.
[29] The Agda Community. Cubical Agda Library, May 2025. URL: https://github.com/agda/cubical.
[30] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
[31] Tarmo Uustalu. Container combinatorics: Monads and lax monoidal functors. In Mohammad Reza Mousavi and Jiří Sgall, editors, Topics in Theoretical Computer Science, pages 91–105, Cham, 2017. Springer International Publishing. doi:10.1007/978-3-319-68953-1_8.
[32] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3(ICFP), July 2019. doi:10.1145/3341691.
[33] Maaike Zwart. On the Non-Compositionality of Monads via Distributive Laws. PhD thesis, University of Oxford, 2020.
[34] Maaike Zwart and Dan Marsden. No-go theorems for distributive laws. Logical Methods in Computer Science, Volume 18, Issue 1:6253, January 2022. doi:10.46298/lmcs-18(1:13)2022.

Appendix A Appendix

Associativity proofs of Proposition 24.

Almost all parts of Proposition 24 have been formalised and can be found here: , aside from the associativity equalities (for technical reasons), which we prove below instead. Sub-expressions with the same colour were rewritten by applying the same position equality.

$\hfill\blacktriangleleft$

Appendix B Appendix

The proofs in this appendix are for Section 7.

Proof of Lemma 34.

By the chain of equalities:

$\hfill\blacktriangleleft$

Proof of Theorem 35.

Assume we have two distinct constant shapes $t_{0},t_{1}:T$ . We first have the chain of equalities:

Using the same steps, we can derive:

and by composing these two equalities, we get that $t_{0}=t_{1}$ . This contradicts our assumption that $t_{0}$ and $t_{1}$ were distinct. $\hfill\blacktriangleleft$

Proof that the list monadic container in Example 11 satisfies the (S3) property (Definition 33), for any $n:\mathbb{N}$ where $f=\lambda\_.0$ .

Proof.

First notice that $\sigma\,n\,f^{p}=1$ for any $p:\mathsf{Fin}\;\,n$ . This means that the shape equality is satisfied, and also that we only have to consider $p^{\prime}=0$ for the position equality.

The sum $f^{p}\,0+\dots+f^{p}\,(i-1)$ becomes $1$ exactly when $i=p$ , which gives us that $\max\,\{i\in[0..n)\ |\ f^{p}\,0+\dots+f^{p}\,(i-1)\leq 0\}=p$ . Therefore, by definition, we have $\mathsf{pr}_{1}\,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb% }{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{n\}}\,{% \color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}% \pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\{f^{p}\}}\,p^{\prime}=p$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of containers. In Andrew D. Gordon, editor, Foundations of Software Science and Computation Structures, pages 23–38, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.

[bib.bib2] [2] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Representing nested inductive types using W-types. In Automata, Languages and Programming, 31st International Colloqium (ICALP), pages 59–71, 2004. doi:10.1007/978-3-540-27836-8_8.

[bib.bib3] [3] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3–27, September 2005. doi:10.1016/j.tcs.2005.06.002.

[bib.bib4] [4] Danel Ahman. An Agda formalisation of the theory of directed containers. https://github.com/danelahman/Directed-Containers, 2011. Online.

[bib.bib5] [5] Danel Ahman, James Chapman, and Tarmo Uustalu. When is a container a comonad? In Lars Birkedal, editor, Foundations of Software Science and Computational Structures, pages 74–88, Berlin, Heidelberg, 2012. Springer. doi:10.1007/978-3-642-28729-9_5.

[bib.bib6] [6] Danel Ahman and Tarmo Uustalu. Distributive laws of directed containers. Progress in Informatics, (10):3–18, March 2013. doi:10.2201/NiiPi.2013.10.2.

[bib.bib7] [7] Thorsten Altenkirch. Quotient inductive types as categorified containers. https://hott-uf.github.io/2024/abstracts/HoTTUF_2024_paper_10.pdf, 2024. HoTT/UF 2024 abstract.

[bib.bib8] [8] Thorsten Altenkirch and Peter Morris. Indexed containers. In 2009 24th Annual IEEE Symposium on Logic In Computer Science, pages 277–285, 2009. doi:10.1109/LICS.2009.33.

[bib.bib9] [9] Thorsten Altenkirch and Gun Pinyo. Monadic containers and $\Sigma$ -universes. https://types2017.elte.hu/proc.pdf#page=28, https://people.cs.nott.ac.uk/psztxa/talks/types-17-cont.pdf, 2017. TYPES 2017 abstract and slides.

[bib.bib10] [10] Steve Awodey. Natural models of homotopy type theory. Math. Struct. Comput. Sci., 28(2):241–286, 2018. doi:10.1017/S0960129516000268.

[bib.bib11] [11] Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. doi:10.1007/BFb0083084.

[bib.bib12] [12] Matthew G. Brin. On the Zappa-Szép Product. Communications in Algebra, 33(2):393–424, February 2005. doi:10.1081/agb-200047404.

[bib.bib13] [13] Alexander Bunkenburg. The Boom Hierarchy, pages 1–8. Springer London, London, 1994. doi:10.1007/978-1-4471-3236-3_1.

[bib.bib14] [14] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.TYPES.2015.5.

[bib.bib15] [15] Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, pages 210–225, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. doi:10.1007/978-3-540-24849-1_14.

[bib.bib16] [16] Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, January 2013. arXiv:0906.4931 [math]. doi:10.1017/S0305004112000394.

[bib.bib17] [17] Håkon Robbestad Gylterud. Symmetric containers. Master’s thesis, University of Oslo, 2011.

[bib.bib18] [18] Paul Hudak, Simon Peyton Jones, Philip Wadler, Brian Boutel, Jon Fairbairn, Joseph Fasel, María M. Guzmán, Kevin Hammond, John Hughes, Thomas Johnsson, Dick Kieburtz, Rishiyur Nikhil, Will Partain, and John Peterson. Report on the programming language haskell: a non-strict, purely functional language version 1.2. SIGPLAN Not., 27(5):1–164, May 1992. doi:10.1145/130697.130699.

[bib.bib19] [19] Ranjit Jhala and Niki Vazou. Refinement types: A tutorial, 2020. arXiv:2010.07763.

[bib.bib20] [20] Amin Karamlou and Nihil Shah. No go theorems: Directed containers that do not distribute over distribution monads. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, pages 1–13, New York, NY, USA, July 2024. Association for Computing Machinery. doi:10.1145/3661814.3662137.

[bib.bib21] [21] Joachim Kock. Notes on polynomial functors, 2009. Unpublished notes.

[bib.bib22] [22] E.G. Manes. Algebraic Theories. Springer Science & Business Media, 2012. doi:10.1007/978-1-4612-9860-1.

[bib.bib23] [23] Ernie Manes and Philip Mulry. Monad compositions I: General constructions and recursive distributive laws. Theory and Applications of Categories, 18:172–208, 2007.

[bib.bib24] [24] Ernie Manes and Philip Mulry. Monad compositions II: Kleisli strength. Mathematical Structures in Computer Science, 18(3):613–643, June 2008. doi:10.1017/S0960129508006695.

[bib.bib25] [25] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991. Selections from 1989 IEEE Symposium on Logic in Computer Science. doi:10.1016/0890-5401(91)90052-4.

[bib.bib26] [26] Chris Purdy and Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers. Software, swhId: swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a (visited on 2025-07-21). URL: https://github.com/chrisjpurdy/distr-laws-of-monadic-containers, doi:10.4230/artifacts.24062.

[bib.bib27] [27] Chris Purdy and Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers HTML rendering. Software (visited on 2025-07-21). URL: https://stefaniatadama.com/distr-law-mnd-cont-html/, doi:10.4230/artifacts.24064.

[bib.bib28] [28] Chris Purdy and Stefania Damato. stefaniatadama/cubical. Software (visited on 2025-07-21). URL: https://github.com/stefaniatadama/cubical/tree/distr-laws, doi:10.4230/artifacts.24065.

[bib.bib29] [29] The Agda Community. Cubical Agda Library, May 2025. URL: https://github.com/agda/cubical.

[bib.bib30] [30] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.

[bib.bib31] [31] Tarmo Uustalu. Container combinatorics: Monads and lax monoidal functors. In Mohammad Reza Mousavi and Jiří Sgall, editors, Topics in Theoretical Computer Science, pages 91–105, Cham, 2017. Springer International Publishing. doi:10.1007/978-3-319-68953-1_8.

[bib.bib32] [32] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical agda: a dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3(ICFP), July 2019. doi:10.1145/3341691.

[bib.bib33] [33] Maaike Zwart. On the Non-Compositionality of Monads via Distributive Laws. PhD thesis, University of Oxford, 2020.

[bib.bib34] [34] Maaike Zwart and Dan Marsden. No-go theorems for distributive laws. Logical Methods in Computer Science, Volume 18, Issue 1:6253, January 2022. doi:10.46298/lmcs-18(1:13)2022.

	$\displaystyle(s,f)$	$\displaystyle=\sigma\,(s,\lambda\_.\iota^{T})\,(\lambda p.(\iota^{S},\lambda\_% .f\,(\pi_{1}\,p)))$
	$\displaystyle(q,p)$	$\displaystyle=(\pi_{1}\,(\mathsf{pr}_{1}\,(q,p)),\pi_{2}\,(\mathsf{pr}_{2}\,(q% ,p)))$