No-Go Theorems for Distributive Laws
Maaike Zwart Dan Marsden
cs.LO math.CT 18C15


No-Go Theorems]No-Go Theorems for Distributive Laws
* This is an extended version of <cit.>.

M. Zwart]Maaike Zwart
D. Marsden]Dan Marsden
Department of Computer Science
 University of Oxford
maaike.annebeth@gmail.com, daniel.marsden@cs.ox.ac.uk






 
Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some general principles for constructing distributive laws. However, until now there have been no such techniques for establishing when no distributive law exists.

We present three families of theorems for showing when there can be no distributive law between two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second and third families are entirely novel, encompassing various new practical situations. For example, they negatively resolve the open question of whether the list monad distributes over itself, reveal a previously unobserved error in the literature, and confirm a conjecture made by Beck himself in his first paper on distributive laws. In addition, we establish conditions under which there can be at most one possible distributive law between two monads, proving various known distributive laws to be unique.



[
    [
    December 30, 2023
=====================





§ INTRODUCTION

Monads have become a key tool in computer science. They are, amongst other things, used to provide semantics for computational effects such as state, exceptions, and I/O <cit.>. They are also used to structure functional programs <cit.>, and even appear explicitly in the standard library of the Haskell programming language <cit.>. As such, it is important to fully understand and characterise their behaviour.

Monads are a categorical concept. A monad on a category 𝒞 is a triple ⟨ T, η, μ⟩ consisting of an endofunctor T:𝒞→𝒞 and two natural transformations η: 1 ⇒ T and μ: T ∘ T ⇒ T satisfying axioms described in  <ref>. Given two monads with underlying functors S and T, it is natural to ask if T ∘ S always carries the structure of a monad. This would, for example, provide a way to combine simple monads together to model more complex computational effects.

Unfortunately, composing the functor parts of two monads does not, in general, result in a new monad. Beck has shown that the existence of a distributive law provides sufficient (but not necessary) conditions for such a composition to form a monad <cit.>. A distributive law between monads S and T is a natural transformation of type:

    S ∘ T ⇒ T ∘ S,

satisfying four equations described in  <ref> below. This important idea has since been generalised to notions of distributive laws for combining monads with comonads, monads with pointed endofunctors, endofunctors with endofunctors and various other combinations, see for example the work by Lenisa et al. <cit.>.

General-purpose techniques have been developed to construct distributive laws <cit.>. These methods are highly valuable, for, in the words of Bonsangue et al.: “It can be rather difficult to prove the defining axioms of a distributive law.” <cit.>. In fact, it can be so difficult that on occasion a distributive law has been published which later turned out to be incorrect; Klin and Salamanca have made an overview of such cases involving the powerset monad <cit.>.

The literature has tended to focus on positive results, either demonstrating specific distributive laws, or developing general-purpose techniques for constructing them. By comparison, there is a relative paucity of negative results, showing when no distributive law can exist. The most well-known result of this type appears in the paper Distributing probability over non-determinism <cit.>, where it is shown that there is no distributive law combining the powerset and probability distribution monads, via a proof credited to Plotkin. This result was strengthened by Dahlqvist and Neves to show that the composite functor carries no monad structure at all <cit.>. Recently, the same proof technique was used by Klin and Salamanca to show that composing the covariant powerset functor  with itself yields an endofunctor that does not carry any monad structure <cit.>, correcting an earlier error in the literature <cit.>. To the best our knowledge, these are currently the only published impossibility results.

In this paper we present several theorems for proving the absence of distributive laws for large classes of monads on the category  of sets and functions. These theorems significantly extend the current understanding of distributive laws.
Our results can roughly be divided into three classes:



  * Firstly, we generalize Plotkin's method to general-purpose theorems covering all the previously
  published no-go results about distributive laws, and yielding new results as well.

  * Secondly, we develop a completely new family of no-go theorems, emphasising unitality axioms rather than the idempotence central to Plotkin's argument.

  * Finally, we prove two further no-go theorems, motivated by a question in Beck's original paper <cit.>. Here we introduce further novel techniques, based on the ability to judiciously “make variables disappear” in terms.


As one application of our new methods, we show that the list monad cannot distribute over itself,
resolving an open question <cit.> and previous error <cit.> in the literature.
Another open question we resolve is a conjecture made by Beck in 1969 <cit.>, stating that the Abelian group monad does not distribute over the list monad. In addition to answering open questions, the no-go theorems produced by these methods reveal yet another faulty distributive law in the literature, involving the list and exception monads.

Apart from our negative results, we also prove a uniqueness result. Under certain conditions, we prove that there is only one possible distributive law facilitating monad compositions, namely the distributive law resembling the times over plus distributivity. This proves that several known distributive laws, such as the distributive law for the multiset monad over itself, are unique.

Monads have deep connections with universal algebra. We fully embrace this algebraic viewpoint on monads, basing our proofs on an explicit algebraic equivalent of distributive laws formulated by Piróg and Staton <cit.>, which was inspired by the work of Cheng <cit.>. Formulating our results in algebraic form is a key contribution of our work, simplifying and clarifying the essentials of our proofs, which can be obscured by more direct calculations.

In physics, theorems proving the impossibility of certain things are called no-go theorems, because they clearly identify theoretical directions that cannot succeed. We follow this example, and hope that by sharing our results, we prevent others from wasting time on forlorn searches for distributive laws that do not exist.



 §.§ Contributions

We briefly outline our contribution. By taking an algebraic perspective, we demonstrate the non-existence of distributive laws for large classes of monads:
  
  
  * In  <ref>  we widely generalize the essentials of a counterexample due to Plotkin <cit.>:
    
    
  * We establish in  <ref> purely algebraic conditions under which a no-go result holds. This theorem recovers all the known negative results we are aware of, and many useful new results. The key ingredients for this theorem are binary terms that are idempotent and commutative.
    
  * In  <ref> we generalize  <ref> further, showing there is nothing essential about binary terms.
    
  *  <ref> eliminates commutativity assumptions, yielding more useful insights.
    
  * Finally, in  <ref> we replace one of the idempotent terms from  <ref> with a unital one, still following the same general proof technique, yielding  <ref>.
    

  * In  <ref> we present three entirely new no-go theorems:
     
     
  * Theorem <ref> states conditions under which algebraic theories with more than one constant do not combine well with other theories. The usefulness of this theorem is demonstrated by  <ref>, which identifies a previously unnoticed error in a theorem in the literature.
     
  * Theorem <ref> is a general no-go theorem for monads that do not satisfy the so-called abides equation <cit.>. One of its applications is that it negatively answers the open question of whether the list monad distributes over itself.
     
  * Theorem <ref> is a general no-go theorem focussing on the combination of idempotence and units. From this theorem it follows that there is no distributive law for the powerset monad over the multiset monad: P ∘ M ⇒ M ∘ P.
     
  * Section <ref> also contains two characterization results, giving insights into how a distributive law has to behave, if it exists at all. Proposition <ref> identifies when the unit of one algebraic theory, presenting a monad, acts as an annihilator when another monad is distributed over it. For example, this characterizes the behaviour of empty lists and sets in certain composite monads. Theorem <ref> gives conditions under which at most one distributive law can exist, and what form it must take. For example, the well-known distributive law for the multiset monad over itself is unique.
     
   
  * In  <ref> a second new family of no-go theorems is presented,
     based on another new approach to yielding no-go results within our algebraic framework:
     
     
  * Theorem <ref> confirms a negative conjecture of Beck from the original paper on distributive laws <cit.>.
     
  * Theorem <ref> provides further new results, showing there is no distributive law bL ∘ P ⇒ P ∘ bL between the powerset and bounded distributive lattice monads.
     
   
  * In  <ref> we provide a detailed analysis of the availability of distributive laws for some natural families of monads.
     This includes many examples of applications of our theorems, as well as results from elsewhere in the literature to provide a detailed picture.
     
     
  * We examine distributive laws between monads in the so-called Boom hierarchy,
       a small family of monads representing data structures, which are studied in the functional programming community.
     
  * To gain more examples of existing/non-existing distributive laws, we consider an extension of the Boom hierarchy previously studied by Uustalu <cit.>.
     
  * Finally, we consider possible iterations of compositions in the Boom hierarchy.
     
   
  * In  <ref>, we provide a summary of all axioms used for the various theorems in this paper, together with an overview of which theorem uses which axioms.


Throughout this paper we restrict our attention to monads on the category  of sets and functions, as this is already an incredibly rich setting. Our results are general-purpose in the sense that they are phrased in terms of abstract properties of the algebraic theories corresponding to both monads.

   To compose monads ⟨ S,η,μ⟩ and ⟨ T,η,μ⟩ one may ask if all we really want is some arbitrary monad structure on the functor TS, rather than the specific structure given by a distributive law? Generally, a monad structure arising from a distributive law is vastly preferable to an arbitrary one, as it has many desirable properties. For example, there are canonical monad morphisms S ⇒ T ∘ S and T ⇒ T ∘ S inducing functors between both the Eilenberg-Moore and Kleisli categories of the corresponding monads. Furthermore, T lifts to a monad on the Eilenberg-Moore category of S, and S lifts to a monad on the Kleisli category of T. More succinctly, a distributive law ensures that there is a strong relationship between the parts and the whole.




 §.§ Additional Material

This paper is an extended version of our LiCS2019 conference paper <cit.>. Besides providing detailed proofs and more discussion of the original results, the following additions have been made:


  * Section <ref> extends our Plotkin style counterexamples with a new theorem, bringing more monads within the scope of our techniques.

  *  <ref> introduces a third family of theorems, not present in the original conference paper. These theorems preclude the possibility of distributive laws between additional naturally occurring monads.

  *  <ref> provides detailed analysis of when distributive laws are available for many common monads. These concrete applications further illustrate the use of our main theorems, and situate our results in the broader understanding of distributive laws in the community.

  *  <ref> includes an overview of the axioms used in this paper, and which theorem uses which axioms.




§ PRELIMINARIES




 §.§ Monads and Distributive Laws

We introduce monads, distributive laws, and various examples that will recur in later sections, primarily to fix notation. The material is standard, and may be skipped by the expert reader.
[Monad]
  
For any category 𝒞, a monad ⟨ T,η, μ⟩ on 𝒞 consists of an endofunctor T: 𝒞→𝒞, and natural transformations η: 1 ⇒ T and μ: T ∘ T ⇒ T referred to as the unit and multiplication, satisfying the following axioms:

    μ· Tη    = id unit 1
    μ·η T     = id unit 2
    μ· Tμ    = μ·μ Tassociativity

Or, as commuting diagrams:
 

  
       T [rd, "ηT"][ld, "Tη"'] [d, equal]         TTT [r, "μT"][d, "T μ"']     TT [d, "μ"] 

   TT [r, "μ"']     T     TT [l, "μ"]     TT [r, "μ"']     T
  
 


We will restrict ourselves to monads on the category  of sets and functions. In addition, if there is a finitary version and a full version of a monad, we mean the finitary one unless otherwise specified. We list a few examples of monads on , which we will use throughout this paper.

  
  For any set E, the exception monad (-+E) is given by:
  
  
  * (-+E) maps a set X to the disjoint union X+E.
  
  * η^E_X is the left inclusion morphism.
  
  * μ^E_X is the identity on X, and collapses the two copies of E down to a single copy. That is, μ: (X + E) + E ⇒ X + E.
  
  When E is a singleton set, this monad is also known as the maybe monad, written as (-)_.


  
  The list monad L is given by:
  
  
  * L(X) is the set of all finite lists of elements of X.
  
  * η^L_X(x) is the singleton list [x].
  
  * μ^L_X concatenates a list of lists.
  
  This monad is also known as the free monoid monad, in acknowledgement of its connection to the algebraic theory of monoids, see  <ref> below.


  
  The multiset monad M is given by:
  
  
  * M(X) is the set of all finite multisets[by which we mean: multisets in which only finitely many elements have a non-zero multiplicity. In other words: multisets with finite support. We assume the multiplicities are in the natural numbers. Multisets are also known as `bags'.] of elements of X.
  
  * η^M_X(x) is the singleton multiset x.
  
  * μ^M_X takes a union of multisets, adding multiplicities.
  
  We can generalise the notion of multiset to take multiplicities in the integers rather than the natural numbers. This results in the Abelian group monad. This monad is again named after its algebraic presentation, see  <ref>.


  
  The finite powerset monad P is given by:
  
  
  * P(X) is the set of all finite subsets of X.
  
  * η^P_X(x) is the singleton set {x}.
  
  * μ^P_X takes a union of sets.
  

[Binary Tree Monad]
  
  The binary tree monad  is given by:
  
  
  * (X) is the set of all binary trees with leaves labelled by elements from X.
  
  * η^_X(x) is the tree consisting of a single leaf labelled with x.
  
  * μ^_X flattens a tree of trees.
  


  
  The probability distribution monad D is given by:
  
  
  * D(X) is the set of all finitely supported probability distributions over X.
  
  * η^D_X(x) is the point distribution at x.
  
  * μ^D(e)(x) is the weighted average ∑_d ∈(e) e(d)d(x).
  


  
  For any set of states R, the reader monad (-)^R is given by:
  
  
  * X^R is the set of functions from R to X.
  
  * η^R_X(x) is constantly x.
  
  * μ^R_X(f)(r) = f(r)(r).
  


Given a pair of monads, sufficient conditions for the composite functor to form a monad are given by Beck's distributive laws <cit.>:
[Distributive Law]
Given monads S and T, a distributive law for monad composition T∘ S is a natural transformation λ: S ∘ T ⇒ T ∘ S satisfying the following axioms:

    λ·η^S T     = Tη^S unit1
    λ· Sη^T      = η^T S unit2
    λ·μ^S T     = Tμ^S ·λ S · Sλmultiplication1
    λ· Sμ^T      = μ^T S · Tλ·λ T multiplication2

Or, as commuting diagrams:



    T [dl, "η^S T"'][dr, "T η^S"]         SST [d, "μ^S T"'] [r, "S λ"]     STS [r, "λS"]     TSS [d, "T μ^S"] 

ST [rr, "λ"]        TS     ST [rr,"λ"]         TS 

    S [dl, "Sη^T"'] [dr, "η^T S"]         STT [d, "S μ^T"'] [r, "λT"]     TST [r, "Tλ"]     TTS [d, "μ^T S"] 

 ST [rr, "λ"]         TS     ST [rr,"λ"]         TS 






For a pair of monads S, T the expression “S distributes over T” is often used. This phrasing is somewhat ambiguous and prone to errors. We will therefore explicitly state the type of the natural transformation, for example “there is a distributive law of type S ∘ T ⇒ T ∘ S”.


  Let 𝒞 be a category, and ⟨ S, η^S, μ^S ⟩ and ⟨ T, η^T, μ^T ⟩ two monads on 𝒞. If λ: S ∘ T ⇒ T ∘ S is a distributive law, then T ∘ S carries a monad structure with unit η^Tη^S and multiplication μ^Tμ^S · Tλ S.

[Ring Monad <cit.>]
  
  The motivating example of a distributive law involves the list monad and the Abelian group monad, and has type λ: L ∘ A ⇒  A ∘ L. It captures exactly the distributivity of multiplication over addition:
  
    λ( a · (b + c) ) = (a · b) + (a · c)

  The term `distributive law' is derived from this example, and many other distributive laws exploit similar algebraic properties.
  However, as we will see in  <ref>, caution is needed: the validity of an equation such as (<ref>) does not automatically imply the existence of a distributive law.

[Multiset Monad]
  The multiset monad distributes over itself in a manner analogous to distributing multiplication over addition.



 §.§ Algebraic Theories and Composite Theories

We now outline the connections between algebras, monads, and distributive laws that we require in later sections.
[Algebraic Theory]
  An algebraic signature is a set of operation symbols Σ, each with an associated natural number referred to as its arity. The set of Σ-terms over a set X contains X as variables and is inductively closed under forming terms σ(t_1,…,t_n) for an n-ary operation symbol σ and terms t_1,…,t_n.

  An algebraic theory T consists of a signature , and a set  of pairs of Σ-terms referred to as equations or axioms. We will often write a pair (s,t) ∈ as s T t or simply s = t when convenient. For a subset Y ⊆ X and a term t we write Y ⊢_T t or Y ⊢ t to indicate that the variables appearing in t are contained in the variable context Y. The precise set of variables appearing in t will be denoted (t), and #(t) denotes the cardinality of this set.

The following is well-known <cit.>:

  Given a theory (, ), the free model monad over that signature maps X to the set of -terms over X, quotiented by provable equality in equational logic from the axioms . The unit maps a variable to its corresponding equivalence class, and the multiplication flattens a term-of-terms to a term in the obvious way. If a monad is isomorphic to a free model monad, it is said to be presented by the corresponding theory.

[Monoids]
  
  The algebraic theory of monoids has a signature containing a constant and a binary operation, satisfying left and right unitality and associativity.
  The theory of commutative monoids extends this theory with the commutativity equation.
  The theory of join semilattices further extends the theory of commutative monoids with an additional idempotence axiom.

  The corresponding free model monads are the list, multiset and finite powerset monads respectively.

In the paper Notions of computation determine monads, Plotkin and Power show that many monads describing computational effects have natural algebraic presentations <cit.>.

  
  An algebraic presentation of the reader monad of  <ref>, with state space {0,1}, has a signature containing a single binary operation. Intuitively, x * y is a process that proceeds as x if the state is 0, and y otherwise. This operation should satisfy:
  
    x * x = x   and  
        (w * x) * (y * z) = w * z

  These axioms generalize naturally to larger state spaces.


  
The distribution monad  <ref> can be presented by a family of binary operations +^p, for p ∈ (0,1), satisfying the following axioms <cit.>:
    
    x +^p x     = x
    
          x +^p y    = y +^1-p x 
    
          x +^p (y +^r z)    = (x +^p/p + (1-p)r y) +^p +(1-p)r z



In addition to an algebraic equivalent of monads, we require an algebraic version of distributive laws. This key notion is provided in the form of composite theories, which were introduced by Piróg and Staton <cit.>.
[Composite Theory]
Let U be an algebraic theory that contains two theories S and T.


  * A term in U is separated if it is of the form t[s_x/x], where X ⊢_T t is a T-term and s_x is a family of S-terms indexed by x ∈ X.

  * Two separated terms r_1 = t[s_x/x] and r_2 = t'[s'_x'/x'] in U are equal modulo (T,S) if there are functions

: X → Y, : X' → Y and terms s̅_y, such that:
    
    
  * t[(x)/x] T t'[(x')/x']
    
  * ∀ x ∈ X : s_x Ss̅_(x)
    
  * ∀ x' ∈ X' : s'_x'Ss̅_(x')
    

The theory U is said to be a composite of T after S, if every term u in U is equal to a separated term, and moreover this term is essentially unique in the sense that if v,v' are separated and v U u U v' then v and v' are equal modulo (T,S). Note that this is an oriented notion, a composite of T after S is not equivalent to a composite of S after T.


Note that a decomposition of a separated term r in U into its T and S components, r = t[s_x/x], is not necessarily unique: the term t(s, s) can be written both as t(x,y)[s/x, s/y] and t(x,x)[s/x]. We prove that all possible decompositions of a term are necessarily equal modulo (T,S), and therefore the possible choice in decomposition in the definition above does not matter.


If two separated terms t[s_x/x] and t'[s'_x'/x'] are syntactically equal to each other, t[s_x/x] = t'[s'_x'/x'], then they are equal modulo (T,S). Moreover, all equalities in conditions (a), (b), and (c) above are syntactic equalities in this case.



Suppose that t[s_x/x] = t'[s'_x'/x'], where `=' denotes syntactic equality. We consider the syntactic trees of these terms, which must be equal. We conclude that the terms t and t' have the same syntactic tree, except for possibly their variables. That means that there are variable substitutions : X → Y, : X' → Y such that t[(x)/x] = t'[(x')/x'], which proves condition (a).

Furthermore, again looking at the syntactic tree t[s_x/x] and t'[s'_x'/x'], we see that the s_x and s_x' that appear in the same place in the tree must be syntactically equal. Hence we can choose the terms s̅_y to be those terms that already appear in the tree. That is, s̅_(x) = s_x and s̅_(x') = s_x'. This proves conditions (b) and (c).


In this paper, we shall use an equivalent definition of equality modulo (T,S).

  Let S and T be two algebraic theories, and let U be an algebraic theory that contains both S and T. For terms X ⊢_T t, X'⊢_T t' and families of S-terms {s_x  |  x ∈ X} and {s'_x' |  x' ∈ X'}, the following are equivalent:
  
  
  *  The terms t[s_x/x] and t'[s'_x'/x'] are equal modulo (T,S).
  
  *  There are functions : X → Z, : X' → Z satisfying:
    
    
  * t[(x)/x] T t'[(x')/x'].
    
  * (x_1)  = (x_2)   ⇔  s_x_1S s_x_2.
    
  * (x'_1) = (x'_2)  ⇔  s'_x'_1S s'_x'_2.
    
  * (x)  = (x')   ⇔   s_x S s'_x'.
    
  


  Showing that condition <ref> implies condition <ref> is straightforward. Taking Y to be the union of the ranges of  and , requirements <ref>-<ref> ensure that we can choose s̅_y such that:
  
    s̅_y = 
                    s_x,    (x) = y 
    
                    s_x',    (x') = y.


  To show that condition <ref> implies condition <ref>, notice that by transitivity of equality,  and  from  <ref> already have the properties:
      
        
  * t[(x)/x] T t'[(x')/x'].
        
  * (x_1)  = (x_2)  ⇒  s_x_1S s_x_2.
        
  * (x'_1) = (x'_2) ⇒  s'_x'_1S s'_x'_2.
        
  * (x)   = (x')  ⇒   s_x S s'_x'.
      
  So all we need to show are the reverse implications of the latter three points. To this end, pick a function g: Y → Z such that:
  
  
  * If s_x_1S s_x_2, then g((x_1))   = g((x_2))
  
  * If s'_x'_1S s'_x'_2, then g((x'_1)) = g((x'_2))
  
  * If s_x S s'_x', then g((x))   = g((x'))
  
  The function g effectively takes a quotient of Y, defined by the three conditions above. Transitivity of equality ensures that the compositions = g ∘ and = g ∘ preserve properties <ref>-<ref>. By definition, they also satisfy the reverse implications, and so they satisfy condition <ref>.
  


We may assume that a composite theory is never inconsistent:

If U is a composite theory of theories T after S, and both S and T are consistent, then U is consistent.


  Suppose for contradiction that U is an inconsistent theory. Then for each pair of variables x,y we have x U y. Since both x and y are separated terms, essential uniqueness gives us two substitutions f: {x}→ Z and g:{y}→ Z such that:
  
    x[f] T y[g]    
    
      f(x) = g(y)      ⇔    x S y

  For the first equation to be satisfied without violating the consistency of T, we must have that f(x) = g(y). This implies, however, that x S y, which contradicts the consistency of S. We hence conclude that if U is a composite theory of T after S, U must be consistent.


The following theorem shows that composite theories are indeed the algebraic equivalent of distributive laws.

  
  Let S and T be -monads presented by theories S and T. There is a distributive law of type S∘ T ⇒ T ∘ S if and only if there is a composite theory of T after S.

We will frequently exploit  <ref> by showing that no composite theory exists, and therefore no distributive law.

For positive results it will be useful to know the actual action of the distributive law promised by  <ref>, if we know the composite theory. Conversely, when a distributive law is known to exist, it is useful to have an algebraic presentation for the resulting composite monad. The following theorems provide us with just that. Similar observations have been made by Lack <cit.>, written up more explicitly by Zanasi in his thesis <cit.>. Their results hold for symmetric monoidal theories.


 Let S and T be algebraic theories presenting monads S and T, and let U be a composite theory of T after S. Then the free model monad U is isomorphic to the composition of T∘ S via the distributive law mapping the equivalence class of representative s[t_x/x] to the suitable equivalence class of a separated term in U equal to s[t_x/x].

The proof of this proposition is straightforward but tedious. We give a sketch of the main ideas below, but for full details we refer to <cit.>.

We first establish that the functor U is isomorphic to the functor T ∘ S by finding an explicit natural isomorphism ϕ: U ⇒ T ∘ S. We conclude that the functor T ∘ S has a monad structure, which is given by the monad structure of the free model monad U of theory U. To prove that this structure comes from a distributive law, we prove the following three statements. Together, these statements are equivalent to having a distributive law <cit.>:


  * ⟨ TS, η^Tη^S, μ^TS⟩ is a monad, with multiplication μ^TS = ϕ·μ^U · (ϕ^-1) TS(ϕ^-1).

  * The natural transformations η^T S and Tη^S are monad maps.

  * The middle unitary law holds: μ^TS· Tη^Sη^TS = id_TS.


The distributive law is then given by: λ = μ^TS·η^T ST η^S


Knowing how to construct a distributive law from a composite theory, we will now do the reverse: constructing a composite theory from a known distributive law. To do this, we first define a set of equations derived from the distributive law.


Let S and T be the free model monads of algebraic theories S and T. If there is a distributive law λ: S ∘ T ⇒ T ∘ S, then we define the set of λ-equations E^λ as follows:
Let s[t_x/x] be a representative of an element in STX, and t[s_y/y] a representative of an element in TSX. Then s[t_x/x] = t[s_y/y] ∈ E^λ iff λ maps the equivalence class of s[t_x/x] to the equivalence class of t[s_y/y].



Let S and T be the free model monads of algebraic theories S and T. If there is a distributive law λ: S ∘ T ⇒ T ∘ S, then the following theory is a composite of T after S, and the monad ⟨ TS, η^Tη^S, μ^Tμ^S · Tλ S⟩ is the free model monad of this theory:

    Σ^TS^λ    = Σ^S⊎Σ^T
    
    E^TS^λ    = E^S ∪ E^T ∪ E^λ

We call the composite theory hence constructed TS^λ.


Again the proof is straightforward but tedious. We give a proof sketch below, but for full details we refer to <cit.>.

 From Piróg and Staton's theorem <cit.>, we already know that λ induces a monad that is the free model monad of a composite of T after S. What is left to show is that TS^λ is indeed this composite theory. We prove this by establishing an isomorphism between the Eilenberg-Moore category of the monad TS and the category of algebras for TS^λ.


Propositions <ref> and <ref> together give us a concrete presentation for composite theories:

 Let S and T be algebraic theories presenting monads S and T, and let TS be a composite theory of T after S. Then the following gives a presentation of TS:

    Σ^TS    = Σ^S⊎Σ^T
    
    E^TS^λ    = E^S∪ E^T∪ E^λ

where E^λ consists of all provable equations in TS of form s[t_x/x] = t[s_y/y].





§ GENERAL PLOTKIN THEOREMS
 

In this section we develop algebraic generalizations of the counterexample attributed to Gordon Plotkin <cit.>, which showed that there is no distributive law of type D ∘ P ⇒ P ∘ D,
where D is the distribution monad of  <ref> and P is the finite powerset monad of  <ref>. We present a slight rephrasing of this counterexample, augmented with commentary indicating the main proof ideas that will be used in the later generalizations. Throughout this section we adopt the notational conventions of <cit.> whenever possible to ease comparison with those papers.
[Probability does not distribute over non-determinism]
  Assume, for contradiction, that there is a distributive law of type λ : D ∘ P ⇒ P ∘ D. Fix the set X = { a, b, c, d }, and consider the element ∈ DP(X) defined by:
  
    = { a, b } +^1/2{c, d }.

  We define three functions f_1, f_2, f_3 : X → X:
  
        f_1(a) = a         f_2(a) = a         f_3(a) = a

        f_1(b) = b         f_2(b) = b         f_3(b) = a

        f_1(c) = a         f_2(c) = b         f_3(c) = c

        f_1(d) = b         f_2(d) = a         f_3(d) = c
  
  The plan of the proof is to analyze how  travels around the naturality square for λ, for each of the three functions. The element  and the three functions have been carefully chosen so that the distributive law unit axioms can be applied during the proof.
  
    [scale=0.5, node distance=2cm, ->]
             (tl) DP(X);
            [below of=tl, node distance=1.5cm] (bl) DP(X);
            [right of=tl] (tr) PD(X);
            [right of=bl] (br) PD(X);
             (tl) to node[above]λ_X (tr);
             (bl) to node[below]λ_X (br);
             (tl) to node[left]DP(f_i) (bl);
             (tr) to node[right]PD(f_i) (br);

  We proceed as follows:
  
  
  * Trace  around the naturality square (<ref>) for both f_1 and f_2. We note that as {-,-} is commutative, and +^1/2 is idempotent:
    
    DP(f_1)() = η^D_PX{ a, b } = DP(f_2)().

    Commutativity, and particularly idempotence, will be important ideas for our subsequent generalizations. For both f_1 and f_2 we can apply the first distributive law unit axiom to conclude that:
    
    λ_X ∘ DP(f_1)() = {η^D_X(a), η^D_X(b) } = λ_X ∘ DP(f_2)().

    Now a careful consideration of the actions PD(f_1) and PD(f_2) allows us to deduce that λ_X() must be a subset of:
    
    {η^D_X(a), η^D_X(b), η^D_X(c), η^D_X(d) }.

    This part is less straightforward to generalize. In principle it involves inverse images of equivalence classes of terms in one algebraic theory, with variables labelled by equivalence classes of terms in a second algebraic theory. This motivates our move to an explicitly algebraic formulation. We can see this whole step as establishing an upper bound on the set of variables appearing in λ_X().
  
  * We then trace  around the naturality square (<ref>) for f_3. In this case, we exploit the idempotence of the operation {-, -} to conclude:
    
    DP(f_3)() = {a} +^1/2{ c }.

    This indicates idempotence is actually an important aspect of both monads for this argument to work. Equation (<ref>) allows us to apply the second unit axiom for λ to conclude:
    
    λ_X ∘ DP(f_3)() = { a +^1/2  c }.

    By considering the action of PD(f_3) as before, we conclude that λ_X() must contain an element mapped onto a +^1/2 c by PD(f_3), placing a lower bound on the set of variables that appear in λ_X().
  
  * The lower and upper bounds established in the previous two steps contradict each other, and so no distributive law of type D ∘ P ⇒ P ∘ D can exist.
  


In summary, the argument requires two components:


  * Some operations satisfying certain algebraic equational properties such as idempotence and commutativity.

  * Some slightly more mysterious properties of our monads, making the “inverse image” parts of the argument work correctly.


  The original counterexample is actually shown for what is known as the free real cone or finite valuation monad, as this requires slightly weaker assumptions. We state it here for the distribution monad simply to avoid the distraction of introducing yet another monad. This is essentially a cosmetic decision, and our later results are equally applicable to the original counterexample for the free real cone monad.


Our aim in this section is to extract general methods for showing no-go results for constructing distributive laws, derived from the essential steps in this counterexample.
In order to do this, we isolate sufficient conditions on algebraic theories inducing two monads, such that there can be no distributive law between them. Earlier generalizations of this counterexample have appeared in <cit.>. All the existing approaches involve direct calculations with the distributive law axioms, leading to somewhat opaque conditions. They also remain limited to the case where one of the two monads is the powerset monad, restricting their scope of application.

We introduce terminology for some special sets of terms in an algebraic theory. The theorems are stated in terms of these special sets, which in some cases can restrict the scope for which certain “global” conditions need to apply, broadening the range of applicability.
[Universal Terms]
  For an algebraic theory, we say that a set of terms T is:
  
  
  * Universal if every term is provably equal to a term in T.
  
  * Stable if T is closed under substitution of variables for variables.
  


  Some examples of universal and stable sets:
  
  
  * For any theory, the set of all terms is a stable universal set.
  
  * For the theory of real vector spaces, every term is equal to a term in which scaling by the zero element does not appear. Terms that do not contain the scale by zero operation are clearly also stable under variable renaming. Therefore the terms not containing the scale by zero operation are a stable universal set.
  
  * In the theory of groups, every term is equal to a term in which no subterm and its inverse are “adjacent”. This set is therefore universal. It is not stable, as variable renaming may introduce a subterm adjacent to its inverse.
  


  On first reading, it is probably easiest to take the universal stable sets required in subsequent theorems to be the set of all terms in a theory. This is by far the most common case.


Throughout this section, the variable labels for any algebraic theory will range over the natural numbers.
We will also write n for the set {1,…,n}, so for example, 2 ⊢ t



means t is a term containing at most two variables.

We proceed in four steps. Theorem <ref> is an algebraic generalization of Plotkin's counterexample, capturing the algebraic properties required of both theories in order for a proof of this type to work. In  <ref> we generalize further, removing the restriction to binary terms that was sufficient for the original application. This generalization complicates the proof slightly, and so to clarify the methods involved we present two separate theorems. Finally,  <ref> and <ref> address the need for commutativity-like axioms and idempotency axioms respectively, and bring further combinations of monads into scope.


  
  Let ℙ and 𝕍 be two algebraic theories, T_ℙ a stable universal set of ℙ-terms, and T_𝕍 a stable universal set of 𝕍-terms. If there are terms:
  
    2 ⊢_ℙ p      and      2 ⊢_𝕍 v

  such that:
  
  
  *  p is commutative:
    
    2 ⊢ p(1,2) P p(2,1)

  
  *  p is idempotent:
    
    1 ⊢ p(1,1) P 1

  
  *  For all p' ∈ T_ℙ:
    
    Γ⊢ p(1,2) P p'   ⇒   2 ⊢ p'

  
  
  
  *  v is idempotent:
    
    1 ⊢ v(1,1) V 1

  
  *  For all v' ∈ T_𝕍, and any variable x:
    
    Γ⊢ x V v'   ⇒  {x}⊢ v'

  
  *  For all v' ∈ T_𝕍:
    
    Γ⊢ v(1,2) V v'   ⇒   ({ 1 }⊢ v'∨{ 2 }⊢ v')

  
  Then there is no composite theory of ℙ after 𝕍.


Properties <ref>, <ref>, and <ref> are constraints on the variables appearing in certain terms, which are needed for the “inverse image” part of  <ref>. Property <ref> states that any term equal to the special binary term p can have at most two free variables. Property <ref> states that any term equal to a variable can only contain that variable, and property <ref> states that any term equal to the special binary term v must have at least two free variables. Notice that the upper/lower bound principle from the original argument is reflected in these conditions.


  Assume by way of a contradiction that a composite theory 𝕌 of ℙ after 𝕍 exists.
  Consider the term v(p(1,2),p(3,4)). Then as 𝕌 is composite, there exist X ⊢ p' and Γ⊢ v'_x for each x ∈ X such that:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x].

  Without loss of generality, we may assume that p' ∈ T_ℙ and v'_x ∈ T_𝕊 by universality.
  Define partial function f_1 as follows:
  
    f_1(1)    = f_1(3) = 1
    
        f_1(2)    = f_1(4) = 2

  Then, using this substitution of variables and assumption <ref>:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    substitution
       Γ⊢ v(p(1,2),p(3,4))[f_1] U p'[v'_x[f_1]/x] 
    ⇒    applying the substitution on the left hand side
       Γ⊢ v(p(1,2),p(1,2)) U p'[v'_x[f_1]/x] 
    ⇒    assumption <ref>:  v  is idempotent
       Γ⊢ p(1,2) U p'[v'_x[f_1]/x].

  We now have two separated terms that are equal to each other, so we can apply essential uniqueness. This gives us that there are functions g_1: 2 → Z and g_2: X → Z such that:
  
    p[g_1] P p'[g_2]    Thm <ref>, <ref>
    
        g_1(1) ≠ g_1(2)    Thm <ref>, <ref>
    
        g_1(1) = g_2(x)    ⇔ 1 V v'_x[f_1] Thm <ref>, <ref>
    
        g_1(2) = g_2(x)    ⇔ 2 V v'_x[f_1] Thm <ref>, <ref>.

  As T_ℙ is stable, any variable renaming of p' is also in T_ℙ. And so, by assumption <ref> we must have for all x ∈(p'): g_2(x) = g_1(1) or g_2(x) = g_1(2), which means for each v'_x:
  
    Γ⊢ 1 V v'_x[f_1]   ∨  Γ⊢ 2 V v'_x[f_1].

  Then, using assumption <ref> and the preimage of f_1, we conclude that for all v'_x:
  
    {1,3}⊢ v'_x   ∨  {2,4}⊢ v'_x.


  We use the same strategy again, but with a different substitution. Define a second partial function f_2 as follows:
  
    f_2(1)    = f_2(4) = 1
    
        f_2(2)    = f_2(3) = 2

  Using this substitution and assumptions <ref> and <ref>:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    substitution
       Γ⊢ v(p(1,2),p(3,4))[f_2] U p'[v'_x[f_2]/x] 
    ⇒    applying the substitution on the left hand side
       Γ⊢ v(p(1,2),p(2,1)) U p'[v'_x[f_2]/x] 
    ⇒    assumption <ref>:  p  is commutative
       Γ⊢ v(p(1,2),p(1,2)) U p'[v'_x[f_2]/x] 
    ⇒    assumption <ref>:  v  is idempotent
       Γ⊢ p(1,2) U p'[v'_x[f_2]/x].

  Again we have two separated terms that are equal, so we apply essential uniqueness. This gives us that there are functions g_3: 2 → Z and g_4: X → Z such that:
  
    p[g_3] P p'[g_4]    Thm <ref>, <ref>
    
        g_3(1) ≠ g_3(2)    Thm <ref>, <ref>
    
        g_3(1) = g_4(x)    ⇔ 1 V v'_x[f_2] Thm <ref>, <ref>
    
        g_3(2) = g_4(x)    ⇔ 2 V v'_x[f_2] Thm <ref>, <ref>.

  As T_ℙ is stable, any variable renaming of p' is also in T_ℙ. Therefore, by assumption <ref> we must have for all x ∈(p'): g_4(x) = g_3(1) or g_4(x) = g_3(2), which means for each v'_x:
  
    Γ⊢ 1 V v'_x[f_2]   ∨  Γ⊢ 2 V v'_x[f_2].

  So, using assumption <ref> and the preimage of f_2, we know that for all v'_x:
  
    {1,4}⊢ v'_x     ∨    {2,3}⊢ v'_x.


  We combine the two conclusions (<ref>) and (<ref>), yielding that for all v'_x:
  
    ({1,3}⊢ v'_x  ∨ {2,4}⊢ v'_x)  ∧  ({1,4}⊢ v'_x  ∨ {2,3}⊢ v'_x) 
    ⇒    distributing ∧ over ∨
        ({1,3}⊢ v'_x  ∧ {1,4}⊢ v'_x)  ∨  ({1,3}⊢ v'_x  ∧ {2,3}⊢ v'_x)  ∨
        ({2,4}⊢ v'_x  ∧ {1,4}⊢ v'_x)  ∨  ({2,4}⊢ v'_x  ∧ {2,3}⊢ v'_x) 
    ⇒    this is only possible if
       {1}⊢ v'_x  ∨ {3}⊢ v'_x  ∨ {4}⊢ v'_x  ∨ {2}⊢ v'_x.

  In other words:
  
    ⋁_n ∈ 4{n}⊢ v'_x,

  that is, each v'_x can have at most one variable.

  To get a contradiction, we will now find a v'_x that must have at least two variables. This is where we need assumption <ref>. We make one more substitution. Define a third partial function f_3 as follows:
  
    f_3(1)    = f_3(2) = 1
    
        f_3(3)    = f_3(4) = 2

  Using this final substitution and <ref>:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    substitution
       Γ⊢ v(p(1,2),p(3,4))[f_3] U p'[v'_x[f_3]/x] 
    ⇒    applying the substitution on the left hand side
       Γ⊢ v(p(1,1),p(2,2)) U p'[v'_x[f_3]/x] 
    ⇒    assumption <ref>:  p  is idempotent
       Γ⊢ v(1,2) U p'[v'_x[f_3]/x] 
    ⇒    making it more obvious that  v  is a separated term
       Γ⊢ 5[v(1,2)/5] U p'[v'_x[f_3]/x].

  Again, we arrive at an equality between two separated terms, allowing us to apply essential uniqueness. This gives us that there are functions g_5: {5}→ Z and g_6: X → Z such that:
  
    5[g_5] P p'[g_6]    Thm <ref>, <ref>
    
        g_5(5) = g_6(x)    ⇔ v(1,2) V v'_x[f_3] Thm <ref>, <ref>.

  As ℙ is consistent, the variable 5[g_5] must appear in p'[g_6]. If it did not, we could define a substitution h mapping 5[g_5] to any other variable y, and then conclude y P 5[g_5][h] P p'[g_6][h] P p'[g_6] P 5[g_5], which proves all variables are equal to each other in P, which means P is inconsistent. So by consistency of P, the variable 5[g_5] must appear in p'[g_6]. Hence, there is an x_0 such that g_5(5) = g_6(x_0). And so:
  
    Γ⊢ v(1,2) V v'_x_0[f_3].

  As T_𝕊 is stable, this v'_x_0[f_3] is an element of T_𝕍, and so by <ref>, v'_x_0[f_3] must have at least two variables. Which means v'_x_0 must have at least two variables. This contradicts  (<ref>), which claims that each v'_x can have at most one variable. Therefore the assumed composite theory cannot exist.


The following corollary reflects our real interest in monads:

  
  If monads P and V have presentations ℙ and 𝕍 such that the conditions of  <ref> can be satisfied, then there is no distributive law of type V ∘ P ⇒ P ∘ V.

The subsequent theorems have similar corollaries, which we will not state explicitly.
[Powerset and Distribution Monad]
  Consider the terms 1 ∨ 2 and 1 +^1/2 2 in the theories representing the powerset and distribution monads of  <ref> and <ref>.
  
   Since both of these terms are binary, commutative, and idempotent, and the remaining axioms are satisfied,  <ref> captures the known results that there are no distributive laws of type D ∘ P ⇒ P ∘ D <cit.>, P ∘ P ⇒ P ∘ P <cit.>, or P ∘ D ⇒ D ∘ P <cit.>.
  In addition,  <ref> yields the new result that there is no distributive law of type D ∘ D ⇒ D ∘ D, completing the picture for these monads.

[Powerset and Distribution Monad Again]
  We can also consider the distribution monad to be presented by binary operations +^p with p in the closed interval [0,1], and in fact this is the more common formulation. In this case,  <ref> can still be directly applied, without having to move to the more parsimonious presentation. We simply note that the terms not involving the operations +^1 and +^0 form a stable universal set satisfying the required axioms. The results discussed in the previous example can then be recovered using the conventional presentation of the distribution monad.

[Reader Monad]
It is well known that the reader monad distributes over itself. Looking at the presentation of the reader monad given in  <ref>, we see that although it has idempotent terms, there is no commutative term and hence  <ref> does not apply.

A natural question to ask with regard to  <ref> is whether the choice of binary terms for both p and v is necessary. We thank Prakash Panangaden for posing this question during an informal presentation of an earlier version of this work <cit.>. The answer is that we can generalize to terms with any arities strictly greater than one.  Before we prove this more general statement, we introduce a lemma that is central to establishing the upper bound part of the argument.


  
  Let n,m be strictly positive natural numbers, and σ a fixed-point free permutation of {1,…,m}. For distinct variables a^j_i, 1 ≤ i ≤ m, 1 ≤ j ≤ n, the sets:
  
    { a_i_1^1,a_i_1^2, a_i_1^3, …, a_i_1^n }
       { a_i_2^1,a_σ (i_2)^2, a_i_2^3, …, a_i_2^n }
               ⋮
       { a_i_n^1,a_i_n^2, a_i_n^3, …, a_σ (i_n)^n }

  have at most one common element. Here, each i_k is an element of {i | 1 ≤ i ≤ m}, not necessarily unique.



We proceed by induction on n. The base case n = 1 is trivially true. For n = n' + 1, we consider the first two rows of our table of sets. There are two cases.
  
    
  * If i_1 = σ(i_2), then the first two rows can only agree at their second element, because each a_i^j is distinct, and from the assumption that σ is fixed-point free we know that i_1 is different from i_2 if σ(i_2) = i_1. The claim follows directly from this observation.
    
  * If i_1 ≠σ(i_2) then the first two rows disagree in the second column. Therefore the elements common to all the sets cannot appear in the second column.
      We then remove both row and column 2, and invoke the induction hypothesis for n = n'.
      


We then get a more general variant of  <ref>.

  
  Let ℙ and 𝕍 be two algebraic theories, T_ℙ a stable universal set of ℙ-terms, and T_𝕍 a stable universal set of 𝕍-terms. If there are terms:
  
    m ⊢_ℙ p      and      n ⊢_𝕍 v

  such that:
  
    
  
  *  p is stable under a fixed-point free permutation σ:
    
    m ⊢ p P p[σ]

  
  *  p is idempotent:
    
    1 ⊢ p[1/i] P 1

  
  *  For all p' ∈ T_ℙ:
    
    Γ⊢ p P p'   ⇒   m ⊢ p'

  
  
    
  
  *  v is idempotent:
    
    1 ⊢ v[1/i] V 1

  
  *  For all v' ∈ T_𝕍, and any variable i:
    
    Γ⊢ i V v'   ⇒  { i }⊢ v'

  
  *  For all v' ∈ T_𝕍:
    
    Γ⊢ v V v'   ⇒  (⋁_i ∈Γ{ i }⊢ v' )

  
  Then there is no composite theory of ℙ after 𝕍.


  The required properties are generalizations of the binary conditions in  <ref>. Most are straightforward, but axiom <ref>, the analogue of binary commutativity, is perhaps slightly surprising. Here we only require stability under a single fixed-point free permutation.


  Assume by way of a contradiction that a composite theory 𝕌 of ℙ after 𝕍 exists. Let
  
    a_i^j, 1 ≤ i ≤ m, 1 ≤ j ≤ n

  denote distinct variables. We consider the term
  
    v(p(a_1^1, …, a_m^1), …, p(a_1^n, …, a_m^n)).

  Then as 𝕌 is composite, the separation axiom of composite theories tells us that there exist X ⊢ p' and Γ⊢ v'_x for each x ∈ X such that:
  
    Γ⊢ v(p(a_1^1, …, a_m^1), …, p(a_1^n, …, a_m^n)) U p'[v'_x/x].

  Without loss of generality, we may assume p' ∈ T_ℙ and v'_x ∈ T_𝕍 by universality.

  We use the same approach as in the proof of  <ref>, using substitutions to bound the variables that can appear in each of the v'_x.
  Define substitution f_1 as follows:
  
    f_1(a_i^j) = a_i^1.

  We then have:
  
    Γ⊢ v(p(a_1^1, …, a_m^1), …, p(a_1^1, …, a_m^1)) U p'[v'_x[f_1]/x].

  By assumption <ref>, idempotence of v:
  
    Γ⊢ p(a_1^1, …, a_m^1) U p'[v'_x[f_1]/x].

  As T_ℙ is stable, any variable renaming of p' is also in T_ℙ. Therefore, essential uniqueness tells us that there are substitutions g_1 and g_2 such that:
  
    p[g_1]    P p'[g_2]  Thm <ref>, <ref>
    
        g_1(a_i^1)    ≠ g_1(a_j^1) (i ≠ j) Thm <ref>, <ref>
    
        g_1(a_i^1)     = g_2(x)  ⇔ a_i^1 V v'_x[f_1] Thm <ref>, <ref>,

  and <ref> gives us that:
  
    ∀ x  ∃ i: Γ⊢ a_i^1 V v'_x[f_1].

  Then by assumption <ref>:
  
    ∀ x  ∃ i: {a_i^1}⊢ v'_x[f_1].

  So our first approximation of the variables appearing in v'_x is:
  
    ∀ x  ∃ i:  { a_i^1, …, a_i^n }⊢ v'_x.

  Now we define a family of substitutions for 2 ≤ k ≤ n as follows:
  
    f_k(a_i^j) =
        
          a_σ(i)^k  if  j = k
    
          a_i^k  otherwise .

  If we follow a similar argument as before, using essential uniqueness, <ref>, <ref>, and also exploiting assumption <ref>, we conclude that:
  
    ∀ x,k  ∃ i_k: {a^k_i_k}⊢ v'_x[f_k].

  And so:
  
    ∀ x,k  ∃ i_k:  { a_σ^-1 (i_k)^j | j = k }∪{ a_i_k^j | j ≠ k }⊢ v'_x.

  Then we note that by  <ref>, conditions (<ref>) and (<ref>):
  
    ∀ x  ∃ i,j:  { a_i^j }⊢ v'_x.

  This provides an upper bound on the number of variables appearing in the v'_x, just like the first two substitutions did in the proof of  <ref>. To finish the argument, we define another substitution:
  
    f_n+1(a_i^j) = a_1^j

  Applying this substitution:
  
    Γ⊢ v(p(a_1^1, …, a_1^1), …, p(a_1^n, …, a_1^n)) U p'[v'_x[f_n+1] / x ].

  Using assumption <ref>:
  
    Γ⊢ v(a_1^1, …, a_1^n) U p'[v'_x[f_n+1] / x ].

  By essential uniqueness and consistency:
  
    ∃ x_0:  Γ⊢ v(a_1^1, …, a_1^n) V v'_x_0[f_n+1].

  As T_𝕍 is stable, this v'_x[f_n+1] is an element of T_𝕍. And so, by assumption <ref>, v'_x_0 must contain at least two variables, but this contradicts conclusion (<ref>), and so the assumed composite theory cannot exist.


It is clear that the simpler  <ref> is a special case of  <ref>. Besides providing greater generality, the main point of  <ref> is that it clearly demonstrates that there is nothing special about binary terms. This further clarifies our understanding of what abstract properties make the original counterexample of Plotkin work. By moving to such a high level of abstraction it is also easier to see that our other methods, described in  <ref> and <ref>, are not simply a further generalization of Plotkin's counterexample, as they make fundamentally different assumptions of the underlying algebraic theories.



 §.§ Concerning Commutativity


In  <ref> we require the special term p to be commutative in order to establish that no composite theory exists. In  <ref> this commutativity was generalized to stability under the action of a fixed-point free permutation. This raises the question of whether commutativity-like axioms are essential to this type of proof. In fact, this is not the case, and a similar no-go theorem can be established under modified assumptions that make no use of commutativity.


  
  Let ℙ and 𝕍 be two algebraic theories, T_ℙ a stable universal set of ℙ-terms, and T_𝕍 a stable universal set of 𝕍-terms. If there are terms:
  
    2 ⊢_ℙ p      and      2 ⊢_𝕍 v

  such that axioms <ref>, <ref>, <ref>, <ref> and <ref> hold, and:
  
    
  
  *  For all p' ∈ T_ℙ, and any variable x:
    
    Γ⊢ x P p'   ⇒  {x}⊢ p'

  
  *  For all p' ∈ T_ℙ:
    
    Γ⊢ p(1,2) P p'   ⇒   (∅⊢ p')

  
  Then there is no composite theory of ℙ after 𝕍.



  Axiom <ref> is the same as axiom <ref>, but now we require it to hold for P as well as V. Axiom <ref> states that the term p(1,2) is not equal to a constant in P.



  Assume by way of a contradiction that a composite theory 𝕌 of ℙ after 𝕍 exists. Then as 𝕌 is composite, there exist X ⊢ p' and Γ⊢ v'_x for each variable x ∈(p') such that:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x].

  Without loss of generality, we may assume p' ∈ T_ℙ and all v'_x ∈ T_𝕍 by universality.

   As in previous proofs, we use various substitutions to learn more about the terms p' and all v'_x. The first substitution reduces the left hand side of Equation (<ref>) to a term involving just p(1,2). This allows us to use essential uniqueness to get information about v'_x. Define substitution f_1 as follows:
  
    f_1(1)    = f_1(3) = 1
    
        f_1(2)    = f_1(4) = 2

  Then from  (<ref>) we conclude:
  
    v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    Substitution
        v(p(1,2)[f_1],p(3,4)[f_1]) U p'[v'_x[f_1]/x] 
    ⇒    applying the substitution on the left hand side
        v(p(1,2),p(1,2)) U p'[v'_x[f_1]/x] 
    ⇒    Assumption <ref>: v  is idempotent 
        p(1,2) U p'[v'_x[f_1]/x].

  We now have two separated terms that are equal to each other, so by essential uniqueness, there are functions g_1: 2 → Z and g_2: X → Z such that:
  
    p[g_1] P p'[g_2],

  and, for all x ∈(p'):
  
    g_1(1) = g_2(x)    ⇔ 1 V v'_x[f_1] 
    
        g_1(2) = g_2(x)    ⇔ 2 V v'_x[f_1].

  As T_ℙ is stable, any variable renaming of p' is also in T_ℙ. And so, by assumption <ref>, we must have g_2(x) = g_1(1) or g_2(x) = g_1(2), which means:
  
    Γ⊢ 1 V v'_x[f_1]   ∨  Γ⊢ 2 V v'_x[f_1].

  Then using assumption <ref>, for all v'_x:
  
    {1,3}⊢ v'_x   ∨  {2,4}⊢ v'_x.

We can now split the set of variables (p') into two disjoint subsets:

    X_1     = {x  | {1,3}⊢ v'_x }
    
      X_2     = {x  | {2,4}⊢ v'_x }.

The aim of the rest of the proof will be to show that (p') = ∅, which will give a contradiction with assumption <ref>. For this, we will need some more substitutions.
Define a second partial function f_2 as follows:

    f_2(1)    = f_2(2) = 1
    
        f_2(3)    = f_2(4) = 2

Applying this substitution to  (<ref>):

    v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    Substitution
        v(p(1,2)[f_2],p(3,4)[f_2]) U p'[v'_x[f_2]/x] 
    ⇒    applying the substitution on the left hand side
        v(p(1,1),p(2,2)) U p'[v'_x[f_2]/x] 
    ⇒    Assumption <ref>: p  is idempotent 
        v(1,2) U p'[v'_x[f_2]/x],

which is the same as:

    5[v(1,2)/5] U p'[v'_x[f_2] / x].

Again we have two separated terms that are equal, allowing us to use essential uniqueness. We conclude that there are functions g_3: {5}→ Z and g_4: X → Z such that:
  
    5[g_3] P p'[g_4],

  and, whenever g_3(5) = g_4(x), v(1,2) V v'_x[f_2].
  By assumption <ref>:
  
    {g_3(5)}⊢ p'[g_4].

  And so for all x ∈(p'):
  
    v'_x[f_2] V v(1,2).

That is, under substitution f_2, all the v'_x are equal to v(1,2). The next step is designed to get rid of substitution f_2, and hence fully understand each v'_x. Since we already know from  (<ref>) that the variables appearing in v'_x are different depending on whether x ∈ X_1 or x ∈ X_2, we need to treat those cases separately.
Starting with x ∈ X_1, consider the partial functions f_3:

    f_3(1)     = 1      f_3(3)     = 3
    
        f_3(2)     = 3      f_3(4)     = 4

This substitution will act as an `inverse' for f_2, as will become clear in the following argument.
Combining Equations (<ref>) and (<ref>):

    v'_x[f_2][f_3] 
    
     =    writing out the substitutions
        v'_x[1/1, 1/2, 2/3, 2/4][1/1, 3/2, 3/3, 4/4] 
    
     =    ignoring the identity substitutions
        v'_x[1/2, 2/3, 2/4][3/2] 
    
     =    x ∈ X_1  so {1,3}⊢ v'_x
        v'_x[2/3][3/2] 
    
     =    the second substitution is the inverse of the first
        v'_x.

Since v'_x[f_2] V v(1,2) by  (<ref>), we conclude for all x ∈ X_1:

    v'_x[f_2] V v(1,2) 
    ⇒    substitution
        v'_x[f_2][f_3] V v(1,2)[f_3] 
    ⇒    by the above:  v'_x[f_2][f_3] = v'_x 
        v'_x V v(1,2)[f_3] 
    ⇒    applying  f_3
        v'_x V v(1,3).

So for x ∈ X_1, we know that v'_x V v(1,3).
A similar line of reasoning can be followed for x ∈ X_2. To negate substitution f_2 for these v'_x, we need the following substitution:

    f_4(1)     = 2      f_4(3)     = 3
    
        f_4(2)     = 4      f_4(4)     = 4

The rest of the argument is the same, leading to the conclusion that for all x ∈ X_2, v'_x V v(2,4).
We now have all the information about the v'_x that we need. We start working towards a contradiction with yet another substitution. This time, it is a substitution of terms for variables:

    f_5(1)     = p(1,2)     f_5(3)     = p(1,1) 
    
      f_5(2)     = p(1,2)     f_5(4)     = p(2,2)

These terms are chosen in such a way that the left hand side of Equation (<ref>) reduces to p(1,2) after substitution with f_5, so that we can use essential uniqueness again. On the right hand side, the substitution creates 𝕍-terms with ℙ-terms in them. Separating these terms into ℙ-terms built out of 𝕍-terms will yield new information, and eventually the contradiction.
So, starting from Equation (<ref>):

    v(p(1,2),p(3,4)) U p'[v'_x/x] 
    ⇒    Substitution
        v(p(1,2)[f_5],p(3,4)[f_5]) U p'[v'_x[f_5]/x] 
    ⇒    applying the substitution on the left hand side
        v(p(p(1,2),p(1,2)),p(p(1,1),p(2,2))) U p'[v'_x[f_5]/x] 
    ⇒    p  is idempotent
        v(p(1,2),p(1,2)) U p'[v'_x[f_5]/x] 
    ⇒    v  is idempotent
        p(1,2) U p'[v'_x[f_5]/x].

Before applying essential uniqueness to Equation (<ref>), we need to separate the right hand side of this equation. Remember from Equation (<ref>) that v'_x V v(1,3) or v'_x V v(2,4) depending on whether x ∈ X_1 or x ∈ X_2. And so, for x ∈ X_1:

    v'_x V v(1,3) 
    ⇒    substitution
        v'_x[f_5] U v(1,3)[f_5] 
    ⇒    applying the substitution on the right hand side
        v'_x[f_5] U v(p(1,2),p(1,1)) 
    ⇒    Substitution:  1/3, 1/4 
        v'_x[f_5] U v(p(1,2),p(3,4)[1/3, 1/4]) 
    ⇒    Equation (<ref>)
        v'_x[f_5] U p'[v'_y[1/3, 1/4]/y],

where we know from Equation (<ref>) that for y ∈ X_1, v'_y V v(1,3) and for y ∈ X_2, v'_y V v(2,4).

Similarly, for x ∈ X_2:

    v'_x V v(2,4) 
    ⇒    substitution
        v'_x[f_5] U v(2,4)[f_5] 
    ⇒    applying the substitution on the right hand side
        v'_x[f_5] U v(p(1,2),p(2,2)) 
    ⇒    Substitution:  2/3, 2/4
        v'_x[f_5] U v(p(1,2),p(3,4)[2/3, 2/4]) 
    ⇒    Equation (<ref>)
        v'_x[f_5] U p'[v'_y[2/3, 2/4]/y],

where we know from Equation (<ref>) that for y ∈ X_1, v'_y V v(1,3) and for y ∈ X_2, v'_y V v(2,4).
And so, continuing from Equation (<ref>):

    p(1,2) U p'[v'_x[f_5]/x] 
    ⇒     p(1,2) U p'[p'[v'_y[1/3, 1/4]/y] / x ∈ X_1, 
                             p'[v'_y[2/3, 2/4]/y] / x ∈ X_2],

where v'_y V v(1,3) for y ∈ X_1 and v'_y V v(2,4) for y ∈ X_2.
We can now apply essential uniqueness, and use property <ref> to conclude that both:

    1 V v'_y[1/3, 1/4]   ∨      2 V v'_y[1/3, 1/4]
    
    1 V v'_y[2/3, 2/4]   ∨      2 V v'_y[2/3, 2/4].

For y ∈ X_1, however:

    v'_y[2/3, 2/4]    V v(1,3)[2/3, 2/4] 
        = v(1,2).

So, to satisfy equation (<ref>), we conclude that v(1,2) V 1 or v(1,2) V 2. By property <ref>, this means that {1}⊢ v(1,2) or {2}⊢ v(1,2). This contradicts property <ref>. And so we must conclude that X_1 = ∅.
Similarly, for y ∈ X_2:

    v'_y[1/3, 1/4]    V v(2,4)[1/3, 1/4] 
        = v(2,1).

In order to satisfy equation <ref>, we must have v(2,1) V 1 or v(2,1) V 2. By property <ref>, this means that {1}⊢ v(2,1) or {2}⊢ v(2,1), which contradicts property <ref>. And so we must also conclude that X_2 = ∅.
Therefore:

    (p')     = X_1 ∪ X_2 
        = ∅∪∅
        = ∅.

However, from Equation (<ref>) we know: p[g_1] P p'[g_2], and from property <ref> we know that:

    (∅⊢ p'[g_2]).

And so, (p') cannot be empty. Contradiction! Hence no composite theory of ℙ after 𝕍 can exist.



The proofs in this section require different types of substitutions, and this difference impacts their scope of application. The proofs of  <ref> and <ref> only require variable-for-variable substitutions, and actually preclude the existence of distributive laws for pointed endofunctors, generalizing <cit.>. The proof of  <ref> requires more complex substitutions, implicitly assuming the multiplication axioms. Therefore,  <ref> only applies to distributive laws between monads.



  If we consider the algebraic theory of an idempotent binary operation,  <ref> shows that the induced monad cannot distribute over itself. This remains true if we add either units or associativity, showing various non-commutative variants of non-determinism cannot be distributed over themselves.

  Similarly, if we denote any of these monads by T, there is no distributive law D ∘ T ⇒ T ∘ D, where D is the distribution monad.

[Reader Monad]
  The presentation of the binary reader monad given in  <ref> satisfies:
  
    x = (x * y) * (z * x)

   However, this theory has no term p satisfying both axioms <ref> and <ref>. So as expected, we cannot apply  <ref> to the binary reader monad.




 §.§ Regarding Idempotence


All theorems so far rely heavily on idempotent terms in both theories. The main advantage idempotent terms provide for our proofs is that they can be reduced to a variable in a controlled way. Idempotence is, however, not the only algebraic property with this effect. Compare idempotence:

    x * x = x

to unitality:

    x * 1 = x


Both idempotence and unitality have x as the only variable appearing on either side of the equation, and both equations reduce a more complicated term to a single variable. We can capture this behaviour in slightly more general terms, namely: “There is a term t and a substitution f such that for any variable x ∈(t), t[f(x')/x' ≠ x] = x”. For the idempotence and unitality equations, the term t would be x * y, and the substitution would be f(y) = x for idempotence and f(y) = 1 for unitality.

This generalisation of the idempotence equation leads us to  <ref>. The proof technique used for  <ref> still works with this more general assumption, although extra care needs to be taken when substituting a T-term into an S-term, as this could turn a previously separated term into a term that is no longer separated. As in the previous proofs, we need extra assumptions such as commutativity to make the proof go through. Notice that we only generalise one of the two idempotent terms. For the other term, the current proof method requires the more specific properties of the idempotence equation.


  In  <ref> below we state and prove the theorem for binary terms. This is to make it easier to see where and how the more general assumption replaces the assumption of idempotency in the proof. By copying the strategy from  <ref>, however, it is straightforward to generalise  <ref> to the case where p is an m-ary term and v and n-ary term.



  
  Let ℙ and 𝕍 be two algebraic theories, T_ℙ a stable universal set of ℙ-terms, and T_𝕍 a stable universal set of 𝕍-terms.
  If there are terms:
  
    2 ⊢_ℙ p      and      2 ⊢_𝕍 v

  such that:
  
  
  *  p is commutative:
    
    2 ⊢ p(1,2) P p(2,1)

  
  *  There is a substitution f_p: (p) → T_ℙ, such that:
    
    Γ⊢ p(1,f_p(2)) P 1.

  
   
    
     
  
  *  For all n ⊢ p' ∈ T_ℙ:
   
    n ⊢ p(1,2) P p'   ⇒   2 ⊢ p'

  
   
    
    
  
  
  
  *  v is idempotent:
    
    1 ⊢ v(1,1) V 1

  
  *  For all v' ∈ T_𝕍, and each variable x:
    
    Γ⊢ x V v'   ⇒  {x}⊢ v'

  
  *  For all v' ∈ T_𝕍:
    
    Γ⊢ v(1,2) V v'   ⇒   ({ 1 }⊢ v'∨{ 2 }⊢ v')

  
  Then there is no composite theory of ℙ after 𝕍.



  Assume by way of contradiction that a composite theory U of P after V exists. Then as U is composite, the separation axiom tells us that there exist X ⊢ p' and Γ⊢ v'_x for each x ∈ X such that:
  
    Γ⊢ v(p(1,2),p(3,4)) U p'[v'_x/x].

We make the following substitution of variables:

    f_1(1)     = 1     f_1(3)     = 1 
    
    f_1(2)     = 2     f_1(4)     = 2

This yields:

    v(p(1,2),p(1,2)) U p'[v'_x[f_1]/x] 
    ⇔     v  is idempotent
        p(1,2) U p'[v'_x[f_1]/x].

By essential uniqueness and assumption <ref>, we conclude that for all x:

    v'_x[f_1] V 1   ∨   v'_x[f_1] V 2.

So, using assumption <ref>:

    {1,3}⊢ v'_x   ∨  {2,4}⊢ v'_x.

We make a second substitution:

    f_2(1)     = 1     f_2(3)     = 2 
    
    f_2(2)     = 2     f_2(4)     = 1

This yields:

    v(p(1,2),p(2,1)) U p'[v'_x[f_2]/x] 
    ⇔     p  is commutative
        v(p(1,2),p(1,2)) U p'[v'_x[f_2]/x] 
    ⇔     v  is idempotent
        p(1,2) U p'[v'_x[f_2]/x].

By essential uniqueness and assumption <ref>, we conclude that for all x:

    v'_x[f_2] V 1   ∨   v'_x[f_2] V 2.

So, using assumption <ref>:

    {1,4}⊢ v'_x   ∨  {2,3}⊢ v'_x.

Taking Equations (<ref>) and (<ref>) together, we conclude for all x:

    ⋁_i∈4{i}⊢ v'_x.

This implies that for each x, v'_x is equal to a variable:


  * If {1}⊢ v'_x, then v'_x[f_1] = v'_x. From Equation <ref> we know that v'_x[f_1] V 1 or v'_x[f_1] V 2. And so also v'_x V 1 or v'_x V 2.

  * If {2}⊢ v'_x, then also v'_x[f_1] = v'_x, and so again v'_x V 1 or v'_x V 2.

  * If {3}⊢ v'_x, then v'_x[f_1][3/1, 4/2] = v'_x. From Equation <ref> we know that 
 v'_x[f_1][3/1, 4/2] V 3 or v'_x[f_1][3/1, 4/2] V 4. And so also v'_x V 3 or v'_x V 4.

  * If {4}⊢ v'_x, then also v'_x[f_1][3/1, 4/2] = v'_x, and so again v'_x V 3 or v'_x V 4.

We make a final substitution, using the substitution f_p from property <ref>::

    f_3(1)     = 1     f_3(3)     = 2 
    
    f_3(2)     = f_p(2)     f_3(4)     = f_p(4)

This yields:

    v(p(1,f_p(2)),p(3,f_p(4))) U p'[v'_x[f_3]/x] 
    ⇔     property <ref>
        v(1,3) U p'[v'_x[f_3]/x] 
    ⇒      clarifying that  v(1,3)  is a separated term
        5[v(1,3)/5] U p'[v'_x[f_3]/x].

Notice that the term p'[v'_x[f_3]/x] is separated: since every v'_x is just a variable, the substitution f_3 does not break separation, even though it might insert a P term. We apply essential uniqueness: there are substitutions g_1: {5}→ Z, g_2: X → Z such that:

    5[g_1]    P p'[g_2] 
    
    g_1(5) = g_2(x)    ⇔ v(1,3) V v'_x.

By consistency of P, we know that there is at least one x such that g_1(5) = g_2(x). And hence there is at least one v'_x such that v'_x V v(1,3). But this contradicts assumption <ref>, since for all x, v'_x is equal to a variable. We conclude that no composite theory of P after V can exist.


Theorem <ref> precludes even more distributive laws:

[Multiset and Powerset Monad: Filling in the Gap]
 The theory of commutative monoids, presenting the multiset monad, does not have an idempotent term. Therefore, it has so far been unaffected by our no-go theorems. It does, however, have a unital term, bringing it in scope of  <ref>. From Manes and Mulry <cit.> we know that there are distributive laws M ∘ M ⇒ M ∘ M and M ∘ P ⇒ P ∘ M, where M is the multiset monad and P the powerset monad. We already know that the powerset monad does not distribute over itself, which leaves the combination P ∘ M ⇒ M ∘ P. Theorem <ref> fills this gap, showing there is no distributive law of that type.




§ NO-GO THEOREMS BEYOND PLOTKIN
 
So far, all our impossibility results involve at least one monad with an idempotent term in its corresponding algebraic theory. But the absence of an idempotent term does not guarantee the existence of a distributive law. Consider the list monad for example. This monad is quite similar to the multiset monad, and we observed in  <ref> that the “times over plus” law of  (<ref>) induces a distributive law for the multiset monad over itself. If we assume this also yields a distributive law for the list monad over itself, then from one of the multiplication axioms:

    λ ([[a,b],[c,d]]) = [[a,c],[a,d],[b,c],[b,d]],

whilst from the other:

    λ ([[a,b],[c,d]]) = [[a,c],[b,c],[a,d],[b,d]].

These two statements are incompatible, so the list monad cannot distribute over itself in this way. However, not all distributive laws resemble the distributivity of times over plus, so from this observation alone we cannot yet rule out the possibility of a distributive law for the list monad over itself. In fact, Manes and Mulry found three other distributive laws for the non-empty list monad over itself <cit.>, <cit.>. But despite these distributive laws being good candidates, they fail to extend to distributive laws for the full list monad over itself.

The results in this section build up towards a proof that shows the search for a distributive law for the list monad over itself is futile; no such law exists. As in the previous section, we state our results in general terms, so that they do not only apply to the list monad, but to any monad satisfying the conditions of the theorems.

Firstly, we show in  <ref> that under certain circumstances, constants of one algebraic theory act as `multiplicative zeroes' for terms of the other theory. One application is that any putative distributive law of the list monad over itself must satisfy:

    λ [L_1,…,L_n] = [ ]  if there is an  i  s.t.  L_i = [ ].

When the theory has multiple constants, this observation immediately leads to a contradiction, and hence give us no-go  <ref>.

Building on  <ref>, we then derive conditions under which a distributive law has to behave like the distributivity of times over plus (<ref>), resulting in  <ref>. As a consequence, monads satisfying the conditions of this theorem compose via a unique distributive law, if they compose at all. Again this theorem applies to the list monad, meaning there can be at most one distributive law for the list monad over itself. 

Finally, in  <ref> and <ref> we identify properties that together with  <ref> provide two more no-go theorems:  <ref> and  <ref>. Whereas idempotence was the main property of interest for the no-go theorems in  <ref>, the focus now becomes unitality equations. In addition, the abides equation (above-besides, <cit.>) will be important for  <ref>:

    (a * b) * (c * d) = (a * c) * (b * d).

We will require that this equation does not hold. This is made precise in  <ref> below. From this theorem we can conclude that there is no distributive law for the list monad over itself: the lacking of the abides property is exactly what causes the problem identified at the beginning of this section.

Throughout this section, we will consider two algebraic theories S and T. For S we identify the following properties:

  
  *  For any two terms s', s”:
      
    ∅⊢ s'  ∧ Γ⊢ s' S s”  ⇒  ∅⊢ s”.

  
  *  For any term s' and variable x:
  
    Γ⊢ s' S x   ⇒  {x}⊢ s'.

  
  *  S has an n-ary term  (n≥ 1), for which there is a substitution f: () →S such that for any x ∈():
   
    Γ⊢[f(y)/y ≠ x] S x.

   In addition, we require that the terms f(y) do not contain the variable x.
   
  *  For any n-ary term s' (n≥ 1), there is a substitution f: (s') →S such that for any x ∈(s'):
   
    Γ⊢ s'[f(y)/y ≠ x] S x,

   where the terms f(y) do not contain the variable x.
  
  * S has a binary term  such that:
   
     
  *  e_ is a unit for :
      
    {x}⊢(x,e_) S x S(e_,x).

     
  *   is idempotent:
     
    {x}⊢(x,x) S x.

   

And for T:

  
  *  For all terms X ⊢ t', constant e_T, and any variable substitution f: X → Y:
  
    Y ⊢ t'[f] T e_T  ⇒   X ⊢ t' T e_T.

  
  *  For any two terms t', t”:
      
    ∅⊢ t'  ∧ Γ⊢ t' T t”  ⇒  ∅⊢ t”.

  
  *  For any term t' and variable x:
  
    Γ⊢ t' T x   ⇒  {x}⊢ t'.

  
  *  T has a constant e_T.
  
  * T has a binary term  such that:
    
      
  *  e_ is a unit for :
      
    {x}⊢(x,e_) T x T(e_,x).

      
  *  The abides equation does not hold in T:
   
    Γ⊢((x,y),(z,w)) T((x,z),(y,w)) 
       ⇒   3 ⊢((x,y),(z,w)).

   


  The properties <ref>, <ref>, <ref>, <ref> are all constraints on the variables appearing in terms. <ref> and <ref> read: “Any term provably equal to a constant cannot have any variables itself”. This is, for example, not the case for any theory involving multiplicative zeroes. In the theory of rings, 0 * x = 0, and since the term 0 * x has a variable, it does not satisfy <ref>/<ref>. 

  <ref> and <ref> read: “Any term provably equal to a variable only contains that single variable”. Idempotent terms are examples of terms that equal a variable, satisfying this condition. In theories with absorption axioms, such as the equation x ∨ (x ∧ y) = x from bounded lattices, properties <ref>/<ref> do not hold. 

  Properties <ref> and <ref> are generalizations of unital equations. They require that terms can be reduced to variables via a suitable substitution. However, contrary to the similar requirement <ref> in  <ref>, idempotence is not an instance of properties <ref> and <ref>. Idempotence requires the substitution to change all variables to x: (x,y)[x/y] = (x,x) = x, which is not allowed in this case. Unitality does not use the resulting variable in its substitutions, so unitality is an instance of these properties: (x,y)[e_s/y] = (x,e_s) = x. The difference between <ref> and <ref> is the quantifier.

  Property <ref> is a weaker version of <ref>, focussing on the provability of an equality between a term and a constant, rather than restricting the variables appearing in that term. It reads: “If a variable substitution of term t' is provably equal to a constant, then t' is already provably equal to that constant.” The usefulness of this property compared to <ref> is that is allows for equations such as 0 * x = 0, which were forbidden by <ref>.

  Notice that property <ref> implies <ref>: if t'[f] = e_T then <ref> requires t'[f] to contain no variables. Since f is a variable substitution, this means t' already had no variables, and hence t' = t'[f] = e_T, so <ref> is satisfied. This justifies our claim that one is a weaker version of the other.

  Also notice that <ref> and <ref> both imply <ref>.



If a theory S has a presentation in which all operations are either idempotent or have a unit, then an easy induction shows that S will satisfy <ref>. More precisely, if for every s' ∈Σ^S, either:
  
  
  * s' is idempotent, that is: s'[x/y ≠ x] S x, or:
  
  * s' has a unit e_s': s'[e_s'/y ≠ x] S x,
  
  then S satisfies <ref>.


[Algebraic Properties of Key Monads]
  
  
    
  * The list monad, presented by the theory of monoids, satisfies <ref> and <ref>. The monoid multiplication satisfies <ref> and hence also <ref> and even <ref>,  but the theory of monoids does not satisfy <ref>.
        The equation (x * y) * (z * w) = (x * z) * (y * w) holds in the theory of monoids if and only if y = z, and so it satisfies all of <ref>, <ref>, <ref>, <ref>, <ref>, and <ref>.
    
  * The powerset monad is presented by the theory of join semilattices, which satisfies <ref> in addition to <ref>, <ref>, <ref>, <ref>, and <ref>. However, this theory does not have property <ref> as the join is commutative and associative and so satisfies the abides equation (<ref>). Properties <ref>, <ref>, <ref>, <ref>, and <ref> still hold.
    
  * The exception monad corresponds to an algebraic theory with a signature containing constants for each exception, and no axioms. It satisfies <ref>, <ref>, and <ref>. It does not satisfy <ref>, <ref>, and <ref> as there are no binary terms. Similarly, it satisfies <ref>, <ref>, <ref>, and <ref>, but not <ref> or <ref>.
  




 §.§ Multiplicative Zeroes

Our first focus is on properties <ref> and <ref>. The goal is to prove that in a composite of theories S and T, the constant e_T behaves like a multiplicative zero, consuming any S-term it appears in.


Let S be an algebraic theory satisfying property <ref> for term  in S, and T a theory satisfying properties <ref> and <ref>, giving constant e_T.
If U is a composite theory of T after S, then we must have that, for any x_i ∈(), [e_T/x_i] U e_T.









  The statement is trivial in the case that  has only one free variable, because property <ref> implies that we must have (x) S x. We may therefore assume that  has at least two free variables.

  In a composite theory, every term is equal to a separated term. So there is a t' and there are s'_x such that:
  
    [e_T/x_i] U t'[s'_x/x].

  Using the substitution f given by property <ref>:
  
    [e_T/x_i][f(y)/y ≠ x_i] U t'[s'_x[f(y)/y ≠ x_i]/x] 
    ⇒     axiom <ref>
        e_TU t'[s'_x[f(y)/y ≠ x_i]/x].

  We now have two separated terms equal to each other, so we can use essential uniqueness to conclude that there are variable substitutions g_1, g_2 such that:
  
    e_T[g_1] T t'[g_2].

  Since g_2 is a variable substitution, we can apply assumption <ref>, and conclude that t' T e_T. Going back to our original equation:
  
    [e_T/x_i] U t'[s'_x/x] 
    ⇒      t' T e_T
       [e_T/x_i] U e_T[s'_x/x] 
    ⇒      e_T has no variables
       [e_T/x_i] U e_T,

  which is what we needed to show.



If S satisfies property <ref>, that is, all terms in S with ≥ 1 variables satisfy <ref>, then the constant e_T in T annihilates any S-term it appears in. We say that e_T acts as a multiplicative zero.


If T has more than one constant, this could lead to inconsistencies. Our next no-go theorem makes this precise:

  Let S and T be algebraic theories with properties <ref> and <ref> respectively. Further assume that the term  satisfying <ref> has at least two free variables. Then there exists no composite theory of T after S if T has two or more constants.



  Suppose that U is a composite theory of T after S and let e_1 and e_2 be distinct constants in T. Suppose that {x,y}⊆(). Then by  <ref> we have:
  
    e_1 U s[e_1/x, e_2/y] U e_2.

  By essential uniqueness, we may conclude that e_1 T e_2. Contradiction. So U cannot be a composite of T after S.


[Iterated Distributive Laws]
Theorem <ref> is remarkably useful for determining whether iterated distributive laws are possible. Cheng shows in her paper Iterated distributive laws <cit.> that three or more monads can be composed if there are distributive laws for the pairwise compositions of the monads, and these distributive laws additionally satisfy the Yang-Baxter equation. Theorem <ref> approaches the question of iterated distributive laws from the other end, by severely limiting the possibilities. If in a proposed composition of monads C ∘ B ∘ A, the monads B and C each have a constant (and the other mild requirements of  <ref> are satisfied), then there is no distributive law A ∘ (C ∘ B) ⇒ (C ∘ B) ⇒ A, and hence any possible pairwise distributive laws will not satisfy Yang-Baxter.

We give a few concrete examples involving the list, multiset and powerset monads L, M, P, whose algebraic theories are monoids, commutative monoids, and join semilattices respectively. We know from Manes and Mulry <cit.> that we can form the monads M ∘ L, M ∘ M, and M ∘ P via distributive laws. All of these monads have two constants, which satisfy the condition for T in  <ref>. By picking the term x*y in each of the theories for L, M, and P, we see that these monads satisfy the condition for S. We can therefore exclude all of the following compositions via distributive laws:



[An Error in the Literature]
  
  We saw in the previous example that the term x*y from monoids (the list monad) satisfies the conditions for S in  <ref>. The exception monad satisfies <ref>, so when the exception monad has more than one exception,  <ref> states that there is no distributive law L∘ (-+E) ⇒ (-+E) ∘ L.

However, Manes and Mulry claim to have a distributive law of this type for the case where E = {a,b} <cit.>, given by:


    λ []    = []    λ L     = L  if no element of L is in  E 
    λ [e]     = e  for any exception  e ∈ E    λ L     = a  otherwise.

We check more concretely that this cannot be a distributive law by showing that it fails the first multiplication axiom from  <ref>:


  [column sep=small]
  [[b],[]] [d, "μ^L_EX"] [rr, "L(λ_X)"]         [b, []] [rr, "λ_LX"]         a [d, "E(μ^L_X)"] 

  [b] [rrr, "λ_X"]            b [r, phantom, "≠"]     a
  


The given distributive law follows directly from Manes and Mulry's Theorem 4.6 <cit.>. We suspect that the problem originates in Lemma 4.5 of this paper. Louis Parlant found that the proof of this lemma might use the isomorphism (A ⊗ I) ≅ A implicitly if the signature of the theory has constants, while the lemma explicitly does not assume any monoidal properties of its functors. So the lemma, and hence also Theorem 4.6, may not be valid in the case that the theory has constants. In addition, the induction in the proof of Lemma 4.5 starts at n = 1, where n is the number of variables appearing in a term. This induction therefore excludes constants, which should be considered separately but are absent from the proof.



It is important to notice that  <ref> does not contradict the well-known result that the exception monad distributes over every set monad T; that result is for the other direction (-+E) ∘ T ⇒ T ∘ (-+E).

[Exception Monad]
It is well known that the exception monad distributes over itself. Even though the corresponding theory satisfies properties <ref> and <ref>, there are no terms with more than one free variable, and hence  <ref> does not apply.




 §.§ The One Distributive Law, If It Exists

Needing just the properties <ref>, <ref>, and <ref>,  <ref> already greatly restricts the possibilities for a distributive law between monads S and T. We will now see that if both S and T have binary terms with units, then in a composite theory, the binary of S distributes over the binary of T like times over plus in  (<ref>). For the monads corresponding to these theories, this means that there is only one candidate distributive law to consider.




Let S and T be two algebraic theories, satisfying <ref>, <ref>, <ref> and <ref>, <ref>, <ref> respectively. Assume furthermore that there are terms:
 
    2 ⊢_𝕊     and      2 ⊢_𝕋,

 satisfying <ref> and <ref> respectively. Finally, let U be a composite theory of T after S. Then  distributes over :

    ((y_1,y_2), x_0)    U((y_1,x_0),(y_2,x_0))
    (x_0, (y_1,y_2))    U((x_0,y_1),(x_0,y_2)).





We derive the distributional behaviour in three stages, relying as always on separation and essential uniqueness in a composite theory. 
Suppose that t'[s'_x/x] is a separated term such that ((y_1,y_2), x_0) U t'[s'_x/x], then we derive the following about t'[s'_x/x]:

  
  * First we prove which variables appear in the terms s'_x of the separated term: (s'_x) = { y_1, x_0} or (s'_x) = {y_2,x_0}.
  
  * Then, we prove that each of the s'_x is either equal to (y_1,x_0) or to (y_2,x_0).
  
  * Finally, we derive that the separated term t'[s'_x/x] has to be equal to ((y_1,x_0),(y_2,x_0)).

The proofs of these three stages are quite long. They are separated into different lemmas to make it easier to keep track of the main line of reasoning.

  Let S and T be two algebraic theories satisfying <ref>, <ref>, <ref>, and <ref>, <ref> respectively. Assume furthermore that there are terms:
 
    2 ⊢_𝕊     and      2 ⊢_𝕋,

 satisfying <ref> and <ref> respectively. Finally, let U be a composite theory of T after S. Then there is a T-term X ⊢ t' and there is a family of S-terms s'_x, x ∈ X such that:
  
    ((y_1,y_2), x_0) U t'[s'_x/x],

  and for each x ∈(t'):
  
    (s'_x) = {y_1,x_0}    or    (s'_x) = {y_2,x_0}.

  Moreover, there is an x such that (s'_x) = {y_1,x_0} and an x such that (s'_x) = {y_2,x_0}.

  Similarly, there is a T-term X' ⊢ t” and there is a family of S-terms s”_x', x' ∈ X' such that:
  
    (x_0,(y_1,y_2)) U t”[s”_x'/x'],

  and for each x' ∈(t”):
  
    (s”_x') = {y_1,x_0}    or    (s”_x') = {y_2,x_0}.

  Moreover, there is an x' such that (s”_x') = {y_1,x_0} and an x' such that (s”_x') = {y_2,x_0}.



We only explicitly prove the statements for ((y_1,y_2), x_0). The proof for (x_0, (y_1,y_2)) is similar.

From the fact that U is a composite of the theories S and T, we know that every term in U is equal to a separated term. And so, there is a X ⊢ t' and there is a family s'_x, x ∈ X such that:

    ((y_1,y_2), x_0) U t'[s'_x/x].


We substitute x_0 ↦ e_ in  (<ref>). This yields:

    ((y_1,y_2), e_) U t'[s'_x[e_/x_0]/x] 
    ⇒     e_ is the unit of 
       (y_1,y_2) U t'[s'_x[e_/x_0]/x].

By the essential uniqueness property, we conclude that there are functions:

    : {y_1, y_2}→ Z,   : X → Z,

such that:

    (y_1, y_2)[] T t'[].

Furthermore, whenever (y_1) = (x) or (y_2) = (x), we have respectively:

    y_1    S s'_x[e_/x_0]
    
      y_2    S s'_x[e_/x_0].

Since we assume variables y_1 and y_2 to be distinct, essential uniqueness also gives us (y_1) ≠(y_2).

We analyse  (<ref>) more closely, comparing the variables appearing in both (y_1, y_2)[] and t'[]. First, we show that {(x)  x ∈(t')}⊆{(y_1), (y_2)}. This follows from the following equalities:

    e_
    T    e_ is the unit for 
       (e_, e_) 
    T    Substitution
       ((y_1), (y_2))[e_/(y_1), e_/(y_2)] 
    T    Equation (<ref>)
        t'[][e_/(y_1), e_/(y_2)].

So: e_T t'[][e_/(y_1), e_/(y_2)]. Then by assumption <ref>:

    (t'[][e_/(y_1), e_/(y_2)]) = ∅.

Therefore, t'[] can contain no other variables than (y_1) and (y_2). That is:

    {(x)  x ∈(t')}⊆{(y_1), (y_2)}.

Next, we show that both (y_1) and (y_2) need to appear in t'[]. Suppose that (y_1) does not appear in t'[]. Then from  (<ref>) we know that for all x ∈(t'), (x) = (y_2). Then:

    (y_1) 
    T    e_ is the unit for 
       ((y_1), e_) 
    T    Substitution
       ((y_1), (y_2))[e_/(y_2)] 
    T    Equation (<ref>)
        t'[][e_/(y_2)] 
    T    For all  x, (x) = (y_2)
        t'[e_/x].

So: (y_1) T t'[e_/x], but this contradicts assumption <ref>, because (t'[e_/x]) = ∅, since every free variable in t' has been substituted with the constant e_, and ((y_1)) = {(y_1)}≠∅.

So (y_1) has to appear in t'[]. A similar line of reasoning yields the same conclusion for (y_2). Therefore, there is an x such that (x) = (y_1) and there is an x such that (x) = (y_2).
In summary, if we define:

    X_1    = {x ∈(t') (x) = (y_1)}
    
    X_2    = {x ∈(t') (x) = (y_2)},

then we know that neither X_1 nor X_2 is empty and that X_1 ∪ X_2 = (t').

We finally consider  (<ref>) and (<ref>) to reach a conclusion about the variables appearing in the terms s'_x.
Since for all x ∈ X_1: (x) = (y_1), we have by  (<ref>) that s'_x[e_/x_0] S y_1. Similarly, for all x ∈ X_2, s'_x[e_/x_0] S y_2.
By assumption <ref>, we conclude that:

    ∀ x ∈ X_1:    {x_0, y_1}⊢ s'_x
    ∀ x ∈ X_2:    {x_0, y_2}⊢ s'_x.

In addition, since for any x ∈ X_1, y_1 S s'_x[e_/x_0], we would have y_1 equal to a constant if y_1 would not appear in s'_x, contradicting assumption <ref>. Similarly for y_2 and s'_x, x ∈ X_2. And so:

    ∀ x ∈ X_1:     y_1 ∈(s'_x)
    ∀ x ∈ X_2:     y_2 ∈(s'_x).


To prove that x_0 ∈(s'_x) for all x ∈(t'), we substitute x_0 ↦ e_ in  (<ref>):

    ((y_1,y_2), e_) U t'[s'_x[e_/x_0]/x].

By  <ref>, ((y_1,y_2), e_) U e_. Therefore we must have that also:

    t'[s'_x[e_/x_0]/x] U e_.

The left hand side of this equation might not be separated, since we substitute a T-term inside S-terms. We analyse the terms s'_x[e_/x_0] further to separate them into T-terms of S-terms. There are two cases: either x_0 ∈(s'_x) or not.
 


  * If x_0 ∈(s'_x), then by property <ref>: s'_x[e_/x_0] = e_, which is a separated term.

  * If x_0 ∉(s'_x), then s'_x[e_/x_0] = s'_x, which is also a separated term.

We conclude that t'[s'_x[e_/x_0]/x] is separated. It is our goal to show that we must have x_0 appearing in each s'_x. To this end, define:

    X_3 = {x ∈(t')  |  x_0 ∈ s'_x }.

We will show that we must have X_3 = (t'). We define:

    t” = t'[e_ / x ∈ X_3].

Then:

    t”[s'_x / x] 
    U     definition of  t”
        t'[e_ / x ∈ X_3, s'_x / x ∉ X_3] 
    U     for  x ∈ X_3: s'_x[e_/x_0] = e_. 
       .      and for  x ∉ X_3: s'_x[e_/x_0] = s'_x
        t'[s'_x[e_/x_0]/x] 
    U      (<ref>)
        e_.

So we can apply essential uniqueness to the equation t”[s'_x / x] U e_. We conclude that there must be a variable substitution g such that t”[g] T e_. By property <ref> we conclude that (t”[g]) = ∅ and hence also (t”) = ∅. Since t” = t'[e_ / x ∈ X_3], we conclude that t' has no variables that are not in X_3. In other words: X_3 = (t'), and hence for all x ∈(t'), x_0 ∈(s'_x).









This, together with  (<ref>), (<ref>), (<ref>) and (<ref>), proves that for all x ∈(t'):

    (s'_x) = {y_1,x_0}    or    (s'_x) = {y_2,x_0}.

The fact that neither X_1 nor X_2 are empty means that this proves the lemma.


With the first step done, we move on to the second step:


  Let S and T be two algebraic theories satisfying <ref>, <ref>, <ref> and <ref>, <ref>, <ref> respectively. Assume furthermore that there are terms: 
 
    2 ⊢_𝕊     and      2 ⊢_𝕋,

 satisfying <ref> and <ref> respectively. Finally, let U be a composite theory of T after S.  Then there is a T-term X ⊢ t' and there is a family of S-terms s'_x, x ∈ X such that:
  
    ((y_1,y_2), x_0) U t'[s'_x/x],

  and for each x ∈(t'):
  
    s'_x S(y_1,x_0)     or     s'_x S(y_2,x_0).

  Moreover, there is an x such that s'_x S(y_1,x_0) and an x such that s'_x S(y_2,x_0).

  Similarly, there is a T-term X' ⊢ t” and there is a family of S-terms s”_x', x' ∈ X' such that:
  
    (x_0,(y_1,y_2)) U t”[s”_x'/x'],

  and for each x' ∈(t”):
  
    s”_x'S(x_0,y_1)     or     s”_x'S(x_0,y_2).

  Moreover, there is an x' such that s”_x'S(y_1,x_0) and an x' such that s”_x'S(y_2,x_0).



Again, we only explicitly prove the statements for ((y_1,y_2), x_0). The second half of the claim follows similarly.

As U is a composite theory, we know from the separation axiom that there is a T-term X ⊢ t' and a family of S-terms s'_x,  x ∈ X such that:
  
    ((y_1,y_2), x_0) U t'[s'_x/x].

We substitute y_1 ↦ e_:

    ((e_,y_2), x_0) U t'[s'_x[e_/y_1]/x] 
    ⇒     e_ is the unit of 
       (y_2,x_0) U t'[s'_x[e_/y_1]/x] 
    ⇒     showing that (y_2,x_0) is a separated term
        z[(y_2,x_0)/z] U t'[s'_x[e_/y_1]/x].


To use essential uniqueness, we need two separated terms. However, t'[s'_x[e_/y_1]/x] is a T-term built out of S-terms with possibly a T-constant in them. So we need to separate this term. We use  <ref> in combination with our knowledge from  <ref> about the variables appearing in each s'_x to do this. Define:

    X_1     = {x ∈(t') (s'_x) = {y_1, x_0}}
    
    X_2     = {x ∈(t') (s'_x) = {y_2, x_0}}.

From  <ref> we know that neither X_1 nor X_2 is empty and their union contains all variables in t'. For each x ∈ X_1, we use property <ref> to apply  <ref>, which tells us s'_x[e_/y_1] U e_. For each x ∈ X_2, we know that since y_1 does not appear in s'_x, s'_x[e_/y_1] U s'_x. Therefore:

    t'[s'_x[e_/y_1]/x] T t'[e_/x ∈ X_1, s'_x/x ∈ X_2].

Next, define:

    t” = t'[e_/x ∈ X_1].

Then X_2 ⊢_T t”. We have:

    t”[s'_x/x] 
    U    Definition of  t”
        t'[e_/x ∈ X_1, s'_x/x ∈ X_2]  
    U    Equation (<ref>)
          t'[s'_x[e_/y_1]/x] 
    U    Equation (<ref>)
         z[(y_2,x_0)/z].

Now we can use the essential uniqueness property, and conclude that there are functions : {z}→ Z, : X_2 → Z such that:

    z[(z)/z] T t”[(x)/x].

Furthermore, we have:

    (x) = (z) ⇔ s'_x    S(y_2,x_0).


From  (<ref>) and assumption <ref> we conclude that {(z)}⊢ t”[(x)/x]. And hence for all x ∈ X_2, (x) = (z). So by  (<ref>), for each x ∈ X_2: s'_x S(y_2,x_0), which gives us half of the desired conclusion about each s'_x, x ∈(t').

 A similar argument using the substitution y_2 ↦ e_ instead of y_1 ↦ e_ leads to the conclusion that for each x ∈ X_1, s'_x S(y_1, x_0).


And finally, we prove the last step, in which we show that  distributes over . This yields a proof of  <ref>. We restate the theorem for convenience:


Let S and T be two algebraic theories, satisfying <ref>, <ref>, <ref> and <ref>, <ref>, <ref> respectively. Assume furthermore that there are terms:
 
    2 ⊢_𝕊     and      2 ⊢_𝕋,

 satisfying <ref> and <ref> respectively. Finally, let U be a composite theory of T after S. Then  distributes over :

    ((y_1,y_2), x_0)    U((y_1,x_0),(y_2,x_0)) 
    (x_0, (y_1,y_2))    U((x_0,y_1),(x_0,y_2)).




Again, we only explicitly prove the first statement, as the proof of the second statement is similar, using the appropriate parts of  <ref> and <ref>.

From the separation axiom of composite theories and  <ref> we know that there is a T-term X ⊢ t' and a family of S-terms s'_x,  x ∈ X such that either s'_x = (y_1,x_0) or s'_x = (y_2,x_0) and:
 
    ((y_1,y_2), x_0) U t'[s'_x/x].

Define:

    X_1     = {x ∈(t')  s'_x = (y_1,x_0)}
    
    X_2     = {x ∈(t')  s'_x = (y_2,x_0)}.

Then, using the substitution x_0 ↦ e_, we get:

    (y_1,y_2) 
    U    e_ is the unit of 
       ((y_1,y_2), e_) 
    U    Substitution
       ((y_1,y_2), x_0)[e_/x_0] 
    U     <ref>
        t'[s'_x[e_/x_0]/x] 
    U    s'_x = (y_1,x_0)  or  s'_x = (y_2,x_0).  
       .     and  e_ is the unit of 
        t' [y_1/x ∈ X_1, y_2/x ∈ X_2].

So:

    (y_1,y_2) U t' [y_1/x ∈ X_1, y_2/x ∈ X_2].

We also have:

    t'[s'_x/x]
    U     <ref>
        t'[(y_1,x_0)/x ∈ X_1, (y_2,x_0)/x ∈ X_2] 
    U    Substitution: term = variable[term/variable]
        t'[y_1[(y_1,x_0)/y_1]/x ∈ X_1, y_2[(y_2,x_0)/y_2]/x ∈ X_2].

So we conclude:

    t'[s'_x/x] 
    U    by the reasoning above
         t'[y_1[(y_1,x_0)/y_1]/x ∈ X_1, y_2[(y_2,x_0)/y_2]/x ∈ X_2] 
    U    Equation (<ref>)
       (y_1,y_2)[(y_1,x_0)/y_1, (y_2,x_0)/y_2] 
    U    ((y_1,x_0),(y_2,x_0)),

which proves the theorem.


In suitable cases,  <ref> reduces the search space for distributive laws to a single possibility. From  <ref> we know that the action of distributive laws is determined by the separated terms in the composite theory. And so:

   Let S and T be two monads presented by algebraic theories S and T, having signatures with at least one constant and one binary operation. If for both theories the constant acts as a unit for the binary operation and the theories further satisfy <ref>, <ref>, <ref>, and <ref> and <ref> respectively, then any distributive law S ∘ T ⇒ T ∘ S distributes the binary from S over the binary from T as in  (<ref>).

[Unique Distributive Laws]
 Let S be any of the monads tree[respresented by the theory of a single binary operation and a constant, satisfying only left and right unitality.], list, or multiset. Then the corresponding algebraic theory S contains only linear equations. Let T be either the multiset or powerset monad. Since the multiset and powerset monads are commutative monads, we know that there is a distributive law S ∘ T ⇒ T ∘ S <cit.>. Corollary <ref> states that this distributive law is unique. In particular, the distributive law for the multiset monad over itself mentioned in  <ref> is unique.




 §.§ Lacking the Abides Property: a No-Go Theorem


With  <ref> narrowing down the possible distributive laws for two monads, it is easier to find cases in which no distributive law can exist at all. We identify two properties that clash with  <ref>, one for T and one for S. In this section we show that not satisfying the abides equation,  <ref>, in combination with  <ref> prevents the existence of a distributive law. In the next section we do the same for idempotence,  <ref>. Both properties are sufficiently common to cover a broad class of monads.



   Let S and T be algebraic theories satisfying the conditions of  <ref>, and assume that the binary  in T promised by <ref> additionally satisfies <ref>, then there does not exist a composite theory of T after S.


Suppose there exists a composite theory U. Given  <ref>, we compute a separated term equal in U to ((y_1,y_2), (y_3,y_4)):


    ((y_1,y_2), (y_3,y_4)) 
    U    Substitution
       ((y_1,y_2),x_0)[(y_3,y_4)/x_0] 
    U    Equation (<ref>) from  <ref>
       ((y_1,x_0), (y_2,x_0))[(y_3,y_4)/x_0] 
    U    Substitution
       ((y_1,(y_3,y_4)), (y_2,(y_3,y_4))) 
    U    Equation (<ref>) from  <ref>
       (((y_1,y_3),(y_1,y_4)), ((y_2,y_3),(y_2,y_4))) .

Notice that we made a choice, taking out the right  term in

    ((y_1,y_2), (y_3,y_4)) U((y_1,y_2),x_0)[(y_3,y_4)/x_0],

rather than the left:

    ((y_1,y_2), (y_3,y_4)) U(x_0, (y_3,y_4))[(y_1,y_2)/x_0].

The latter option yields:

    ((y_1,y_2), (y_3,y_4)) 
    U    Substitution
       (x_0, (y_3,y_4))[(y_1,y_2)/x_0] 
    U    Equation (<ref>) from  <ref>
       ((x_0,y_3), (x_0,y_4))[(y_1,y_2)/x_0] 
    U    Substitution
       (((y_1,y_2),y_3), ((y_1,y_2), y_4)) 
    U    Equation (<ref>) from  <ref>
       (((y_1,y_3),(y_2,y_3)),((y_1,y_4),(y_2,y_4))) .

Of course, both computations are equally valid, so the terms in  (<ref>) and (<ref>) must be equal:

    (((y_1,y_3),(y_1,y_4)),((y_2,y_3),(y_2,y_4))) 
    U    (((y_1,y_3),(y_2,y_3)),((y_1,y_4),(y_2,y_4))).

Since these are two separated terms that are equal, we can apply the essential uniqueness property, stating that there exist functions:

    :    {x_1,x_2,x_3,x_4}→ Z
    :    {x_5,x_6,x_7,x_8}→ Z,

such that:

  
  * Equality in T:
         
    (((x_1),(x_2)), ((x_3),(x_4))) 
    T    (((x_5),(x_6)), ((x_7),(x_8))).

  
  * (x_i) = (x_j) iff the S-terms substituted for x_i and x_j in  (<ref>) and (<ref>) are equal in S.

From the second part of essential uniqueness we get that:

    (x_1)     = (x_5)    (x_3)     = (x_6)
    (x_2)     = (x_7)    (x_4)     = (x_8).

For readability of the next argument, set:

    z_1 = (x_1)     = (x_5)     z_3 = (x_3)     = (x_6)
    
    z_2 = (x_2)     = (x_7)     z_4 = (x_4)     = (x_8).

Putting this in the equality in T we found under the first bullet point yields:

    ((z_1,z_2), (z_3,z_4))    T((z_1,z_3), (z_2,z_4)).

And so by  <ref>:

    #(((z_1,z_2), (z_3,z_4))) ≤ 3.

So there must be i,j such that i ≠ j and z_i = z_j. Suppose without loss of generality that z_1 = z_2. Then by essential uniqueness we must have that (y_1,y_3) S(y_1,y_4). But then we can reason:

    y_1 
    S     e_ is a unit for 
       (y_1, e_) 
    S    Substitution
       (y_1, y_3)[e_/y_3] 
    S    (y_1, y_3) = (y_1, y_4)
       (y_1, y_4)[e_/y_3] 
    S    Substitution: no  y_3  in (y_1, y_4) 
       (y_1, y_4).


We conclude that, by  <ref>: {y_1}⊢(y_1, y_4), and so we must have y_4 = y_1. Since these variables are assumed to be distinct, we have a contradiction.
The same argument holds for any other i,j pair. Therefore, the existence of a composite theory leads to a contradiction. In other words, no such composite theory exists.


 If monads S and T are presented by algebraic theories S and T, satisfying the axioms of  <ref>, then there does not exist a distributive law S ∘ T ⇒ T ∘ S.

[Resolving an Open Question]
  This finally settles the question of whether the list monad distributes over itself, posed repeatedly by Manes and Mulry <cit.>. The theory of monoids satisfies all the conditions required of both theories in  <ref>, and hence there is no distributive law for the list monad over itself.

  Note that a distributive law for lists was claimed by King and Wadler <cit.>, although it was subsequently shown to be incorrect by Jones and Duponcheel <cit.>.


  Although there is no distributive law for the list monad over itself, the functor LL does still carry a monad structure. We are very grateful to Bartek Klin for pointing this out to us. The monad structure on LL can be described as follows:
  
    
  * There is a distributive law for the list monad over the non-empty list monad L ∘ L^+ ⇒ L^+ ∘ L <cit.>.
    
  * There is a distributive law for the resulting monad over the maybe monad (L^+L) ∘(-)_⇒(-)_∘ (L^+L), derived from general principles <cit.>.
    
  * The resulting functor (-)_∘ (L^+ ∘ L) is isomorphic to L ∘ L, and carries a monad structure. Hence L ∘ L carries a monad structure, but not one that can be derived from a distributive law L ∘ L ⇒ L ∘ L.
  

[Multiset Monad]
The multiset monad is closely related to the list monad, with an algebraic theory having just one extra equation compared to the list monad: commutativity. Because of this equation, the theory does not have  <ref>. As we have seen in  <ref>, there is a unique distributive law for the multiset monad over itself.





 §.§ Yet Another No-Go Theorem Caused by Idempotence

In  <ref> we saw a no-go theorem that required an idempotent term on one side, and a unital one on the other:  <ref>. We will now see a second theorem of this type. Adding idempotence of the binary to the assumptions for S yields yet another no-go theorem, which partly overlaps with  <ref>, but neither theorem is a consequence of the other.


 
  Let S and T be algebraic theories satisfying <ref>, <ref>, <ref> and <ref>, <ref>, <ref> respectively. Assume furthermore that there are terms

    2 ⊢_𝕊     and      2 ⊢_𝕋,

 satisfying <ref>, <ref> and <ref> respectively. Then there exists no composite theory of T after S.


  Suppose such a composite theory U exists. Then we have:
  
    (y_1,y_2) 
    U    <ref>:  is idempotent
       ((y_1,y_2), (y_1,y_2)) 
    U    Substitution
       ((y_1,y_2),x_0)[(y_1,y_2)/x_0] 
    U    Equation (<ref>) from  <ref>
       ((y_1,x_0), (y_2,x_0))[(y_1,y_2)/x_0] 
    U    Substitution
       ((y_1,(y_1,y_2)), (y_2,(y_1,y_2))) 
    U    Equation (<ref>) from  <ref>
       (((y_1,y_1),(y_1,y_2)), ((y_2,y_1),(y_2,y_2))) 
    U    <ref>:  is idempotent
       ((y_1,(y_1,y_2)), ((y_2,y_1),y_2)).


  From the essential uniqueness property, we may conclude that there are functions : {y_1,y_2}↦ Z, : {y'_1,y'_2,y'_3,y'_4}↦ Z such that:
  
    ((y_1), (y_2))    T(((y'_1),(y'_2)), ((y'_3), (y'_4))),

  and (y_i) = (y'_j) if and only if the S-terms substituted for y_i and y'_j in (y_1,y_2) and ((y_1,(y_1,y_2)), ((y_2,y_1),y_2)) are equal. From this we immediately get:
  
    (y_1)     = (y'_1) 
    (y_2)     = (y'_4).

   We know from essential uniqueness that (y_1) ≠(y_2).
   We show that {(y'_2), (y'_3)}⊆{(y_1),(y_2)}. Since we have:
   
    ((y_1), (y_2)) T(((y'_1), (y'_2)), ((y'_3),(y'_4))),

   we also have:
   
    ((y_1), (y_2))[e_/(y_1),e_/(y_2)] 
       T(((y'_1), (y'_2)), ((y'_3),(y'_4)))[e_/(y_1),e_/(y_2)] 
    ⇒    Substitution, and (y_1) = (y'_1), (y_2) = (y'_4)
       (e_, e_) T((e_, (y'_2)), ((y'_3),e_))[e_/(y_1),e_/(y_2)] 
    ⇒    <ref>: e_ is the unit of 
        e_T((y'_2),(y'_3))[e_/(y_1),e_/(y_2)].

   So by <ref>, (((y'_2), (y'_3))[e_/(y_1),e_/(y_2)]) = ∅. So we must have:
   
    {(y'_2), (y'_3)}⊆{(y_1),(y_2)}.

   But then, by the second part of the essential uniqueness property:
   
    (y_1,y_2) S y_1   or  (y_1,y_2) S y_2.

   Both contradict <ref>. Therefore, the composite theory U cannot exist.


  If monads S and T are presented by algebraic theories S and T, satisfying the axioms of  <ref>, then there does not exist a distributive law S ∘ T ⇒ T ∘ S.


[Powerset Monad Again]
The theory of join semilattices satisfies all the axioms required of both theories in Theorem <ref>. Therefore, there is no distributive law for the powerset monad over itself. This was already shown by Klin and Salamanca <cit.> using similar methods as in  <ref>. Theorem <ref> gives a second, independent proof of this fact.



Theorems <ref> and <ref> both require an idempotent term in theory S, and a unital term in theory T, to preclude a composite theory of T after S. However, these theorems are neither equivalent, nor does one imply the other. The most obvious difference is that Theorem <ref> is stated slightly more general, where instead of a unital term a generalisation of both unitality and idempotence is required. When restricting this requirement to just a unital term, there are still differences between the two theorems: Theorem <ref> applies only if the unital term in T is commutative, whereas  <ref> allows this term to be non-commutative. Conversely,  <ref> requires the idempotent term in S to be unital, where  <ref> does not have this restriction.


[Multiset Monad: The Sweet Spot]
 We come back to the multiset monad. In  <ref> we saw that the algebraic theory presenting the multiset monad had one extra equation compared to the theory for the list monad: commutativity. Because of this equation,  <ref> did not hold, and therefore  <ref> did not apply.

 There is a similar relation between the multiset monad and the powerset monad. Compared to the powerset monad, the theory presenting the multiset monad lacks just one equation: idempotence, which is exactly what  <ref> requires. The lack of this equation in the theory for the multiset monad therefore means that  <ref> does not apply to multiset either. So multiset holds a sort of `sweet spot' in between the two no-go theorems, where a distributive law M ∘ M ⇒ M ∘ M still can and does exist.






§ A CONJECTURE OF BECK YIELDING MORE NO-GO THEOREMS





 §.§ Motivation

The classical example of a distributive law constructs the ring monad from the list monad L, and the Abelian group monad A, via a distributive law L ∘ A ⇒ A ∘ L. We encountered this distributive law in  <ref>. It dates back to Beck's original paper <cit.>, and exploits the arithmetic distribution of multiplication over addition. A natural question, briefly considered by Beck, is
whether there can be a distributive law A ∘ L ⇒ L ∘ A with these monads reversed.
Beck gives the intuition that such a distributive law “would have the air of a universal solution to the problem of factoring polynomials into linear factors”. As such, he suggests L ∘ A “has little chance of being a triple”. Addressing the question of whether “plus distributes over times” is the motivating example for the work in this section.
Unsurprisingly, Beck's intuition is correct, and no such distributive law exists. It turns out that  <ref> is key to the proof.


There is no distributive law A ∘ L ⇒ L ∘ A for the Abelian group monad over the list monad.


The theory of Abelian groups A, yielding the Abelian group monad A, has presentation:


  * Signature: Σ^A = {0^(0), -(.)^(1), +^(2)}.

  * Equations: E^A contains the equations stating that 0 is the unit of +, + is associative and commutative, and -x is the additive inverse of x: x + (-x) = 0.

The theory of monoids M, yielding the list monad L, has presentation:


  * Signature: Σ^M= {1^(0), *^(2)}.

  * Equations: E^M contains the equations stating that 1 is unit of *, and * is associative.

The term x + y in A satisfies the conditions for S in  <ref>, and M satisfies the conditions for T.
We conclude that in any composite theory U of M after A, the following equation must hold:

    x + 1 U 1.

We prove that this implies that x U 0:

    x 
    U     unit
         x + 0 
    U     inverse
         x + (1 + (-1)) 
    U     associativity
         (x + 1) + (-1) 
    U     x + 1 U 1
         1 + (-1) 
    U     inverse
         0.

Hence for any two variables: x U 0 U y, which means any composite theory U is inconsistent. Since the component theories 𝕄 and 𝔸 are consistent,  <ref> tells us that there is no such composite theory.

As for the previous proof ideas, this specific negative result can be abstracted to yield general theorems. We shall address this in the following section.



 §.§ Generalization

The well-known positive result of Manes and Mulry <cit.> about distributive laws requires monads presented by theories with only linear equations. That is, with variables appearing exactly once on each side of the equation. These monads distribute over commutative monads: linear ∘ commutative ⇒ commutative ∘ linear. The careful management of variables has also been important to the proofs of the negative theorems in  <ref> and  <ref>. Generally these theorems do not apply to theories with inverses such as groups, as x - x = 0 means we can make variables appear and disappear almost at will, leading to behaviour too wild to analyze.
The concrete  <ref> did apply to an algebraic theory involving inverses. In fact, it made essential use of the ability to make variables appear and disappear, turning this behaviour from a liability into an asset.

We now abstract from  <ref>, deducing two general theorems that require `variables to go missing' in different ways. The first theorem requires an equation of form s' = e_S, where e_S is a constant and s' has at least one variable. The second theorem asks for an equation of form s' = s, where the term s has a variable that does not appear in s', and neither s nor s' are constants.

We begin with the case of a theory with an equation s' = e_S. Here, the example to keep in mind is an inverse axiom such as x - x = 0, typical of group-like structures, such as groups and rings. This is the most direct abstraction of the motivating counterexample.

Notice that the proof of  <ref> used associativity. We could have avoided this by using the following alternative, but less intuitive, reasoning that applies  <ref> twice:

    x 
    U     unit
         x + 0 
    U     inverse
         x + (1 + (-1)) 
    U     substitution
         x + (1 + y)[-1/y] 
    U      <ref>:  1 + y U 1
         x + 1 [-1/y] 
    U     no variable  y
         x + 1 
    U      <ref>:  x + 1 U 1
         1.

This argumentation uses fewer assumptions, so this is the proof we generalize below.


  Let S be an algebraic theory such that:
  
  
  * S has a constant e_S.
  
  *  S has a term s of arity ≥ 2 such that e_S is a unit of s, that is, for any variable x ∈(s):
  
    s[e_S/y≠ x] S x.

  
  *  S satisfies an equation of form
  
    X ⊢ s' S e_S,

  with (s') ≠∅, and s' can be written as s”[s_i/x_i], such that (s”) ∩(s') ≠∅, and there is a substitution f: (s”) →S such that for any x ∈(s”):
   
    Γ⊢ s”[f(y)/y ≠ x] S x.

  
  
  Let T be an algebraic theory such that:
  
  
  * T has a constant e_T.
  
  *  For all terms t' and any substitution f: X → Y:
  
    Y ⊢ t'[f] T e_T  ⇒   X ⊢ t' T e_T.

  
Then there does not exist a composite theory of T after S.

 <ref> is designed to generalize the proof technique illustrated above. We used the equation x + (-x) = 0, and the fact that x + (-x) could be written as x + y[(-x) / y]. We then used  <ref> on x + y. In order for this argument to work in general, we hence require:
  
  
  * A term s' which is equal to a constant, x + (-x) in the example above.
  
  * A term s” such that s' is equal to s” under a certain substitution, x + y in the example.
  
  * Since we want to apply  <ref>, s” needs to satisfy the conditions for this proposition.
  
  * And lastly we require that s' and s” share at least one variable, which is a technicality needed to make the proof go through.
  

  We need axiom <ref> to be able to apply propnary. As a reminder, it reads: “If a variable substitution of term t is provably equal to a constant, then t is already provably equal to that constant.”


Let U be any (candidate) composite theory of T after S.
Consider the equation s' = e_S.
We know that S has a term s such that e_S is a unit of s. Choose variable x such that x ∉(s'). Then we use both the unit equation for s and the fact that s' = e_S:

    x U s[e_S/y ≠ x] 
    ⇒      e_SS s' 
        x U s[s'/y ≠ x].

Next, we substitute e_T into all variables in s'. Since we chose x such that x ∉(s'), this substitution has no effect on the left hand side of our equation.

    x U s[s'/y ≠ x] 
    ⇒     Substitution
        x[e_T/z∈(s')] U s[s'[e_T/z∈(s')]/y ≠ x] 
    ⇒      x ∉(s')
        x U s[s'[e_T/z∈(s')]/y ≠ x].

We will now work on the term s[s'[e_T/z∈(s')]/y ≠ x]. Recall that s' can be written as s”[s_i/x_i] and s” satisfies the conditions for  <ref>. Also, since (s”)∩(s')≠∅, we know that the substitution s'[e_T/z∈(s')] U s”[s_i/x_i][e_T/z∈(s')] yields a term where at least one of the variables of s” gets substituted with e_T. Hence by  <ref>, this resulting term is equal to e_T. Therefore:

    x U s[s'[e_T/z∈(s')]/y ≠ x] 
    ⇒     writing  s'  as  s”[s_i/x_i] 
        x U s[s”[s_i/x_i][e_T/z∈(s')]/y ≠ x] 
    ⇒      <ref>:  s”[s_i/x_i][e_T/z∈(s')] U e_T
        x U s[e_T/y ≠ x] 
    ⇒      <ref> again
        x U e_T.

Notice that in the last step, we applied  <ref> to s instead of s”. We are allowed to do this because s is unital by assumption <ref>, and hence also satisfies  <ref>.

From the equation x U e_T, we get by simple variable substitution that y U e_T for any variable y, and so specifically: x U e_TU y. We conclude that U is inconsistent. As the original theories are assumed to be consistent, there is no such composite theory.


In case of Abelian groups and monoids, the equation s' = e_S required from Abelian groups is the inverse equation x + (-x) = 0. This equation can be written as (x + y)[(-x)/y]. Since the terms x + y and x + (-x) share the variable x, condition <ref> is satisfied.



There are countless monads satisfying the criteria for T. A few natural examples are the list, multiset, powerset, and the exception monads.

We have already seen that Abelian groups satisfy the criteria for S. In addition, any theory with a multiplicative zero x * 0 = 0 can be a good candidate, if the binary operation * is either idempotent or unital. Rings are an obvious example, but  <ref> gives us many more. The multiset monad satisfies all the criteria for S and T in  <ref>. We know that there is a distributive law for the multiset monad over itself, see  <ref>, so the unit of one of the binary operations in the composite theory corresponding to the monad M ∘ M must act as a multiplicative zero for the other.

We can hence make the following table of example compositions  <ref> proves impossible via a distributive law:












More examples illustrating the scope of  <ref> will be given in  <ref>.


The second theorem we find as a generalization of  <ref> focusses on the equation s = s', where s has a variable that does not appear in s'. Here
the motivating example axioms are absorption laws a ∧ (a ∨ b) = a, seen in lattices and similar structures.
This is a slightly less direct abstraction of  <ref>, exploiting the observation
that the key requirement is controlled introduction and elimination of variables.

  Let S be an algebraic theory such that:
  
  
  *  S satisfies an equation of form X ⊢ s S s', where (s)∖(s') ≠∅ (that is, s has a variable that does not appear in s').
   
  *  There is a substitution f: (s) →S such that for any x ∈(s):
   
    Γ⊢ s[f(y)/y ≠ x] S x.

  
  *  There is a substitution f': (s') →S such that for any x ∈(s'):
   
    Γ⊢ s'[f'(y)/y ≠ x] S x.

  
  Let T be an algebraic theory such that:
  
  
  * T has a constant e_T.
  
  *  For all terms t' and any substitution f: X → Y:
  
    Y ⊢ t'[f] T e_T  ⇒   X ⊢ t' T e_T.

  

Then there does not exist a composite theory of T after S.



Apart from <ref>, all the required properties are familiar from  <ref>. <ref> and <ref> are generalizations of idempotence/unitality equations, while <ref> states that “If a variable substitution of term t is provably equal to a constant, then t is already provably equal to that constant.”



Let U be any (candidate) composite theory of T after S. Consider the equation s = s' from the assumptions. Let f' be a substitution of the variables in s' such that s'[f'] S x, where x ∈(s'). Then:

    s S s' 
    ⇒     Substitution
        s[f'] S s'[f'] 
    ⇒      s'[f'] S x  by construction of  f' 
        s[f'] S x.


Now let g be the constant substitution g: (s)∖(s') →{e_T}, mapping all the variables that appear in s but not in s' to the constant e_T. Since (s)∖(s') ≠∅, at least one instance of e_T will be present in s[f'][g]. Then:

    s[f'] U x 
    ⇒     Substitution
        s[f'][g] U x[g] 
    ⇒      x ∈(s')  and therefore untouched by  g 
        s[f'][g] U x 
    ⇒      <ref>, since  s[f'][g]  contains at least one  e_T
        e_TU x.

Using substitution, we can hence show that x U e_TU y, from which it follows that U is inconsistent. As the original theories are assumed to be consistent, there is no such composite theory.


 <ref> solves a question Julian Salamanca posed in 2018 <cit.>, asking whether there is a distributive law bL ∘ P ⇒ P ∘ bL, distributing the bounded lattice monad bL over the powerset monad P. The answer is no.


There is no distributive law for the (bounded) lattice monad over the powerset monad.
The presentation for the bounded lattice monad is given by:


  * Signature: {⊤^(0), ^(0), ∨^(2), ∧^(2)}.

  * Equations: ⊤ is the unit of ∧,  is the unit of ∨, associativity of ∨ and ∧, commutativity of ∨ and ∧, idempotence of ∨ and ∧, absorption both ways: x ∨ (x ∧ y) = x and  x ∧ (x ∨ y) = x.

We see that the bounded lattice monad satisfies the criteria for S in  <ref>:

  
  * The equation s = s' is x ∨ (x ∧ y) = x.
  
  * The substitution f such that s[f] = x uses the unit of ∧ and idempotence of ∨:
  
    x ∨ (x ∧ y) [⊤ / y] = x ∨ (x ∧⊤) = x ∨ x = x.

  
  * The substitution f' such that s'[f'] = x is the identity, since the term s' is just the variable x.

The presentation of the powerset monad is given by:


  * Signature: {0^(0), +^(2)}.

  * Equations: 0 is unit of +, + is associative, commutative, and idempotent.

The powerset monad satisfies the criteria for T in  <ref>, and so we conclude that there is no distributive law bL ∘ P ⇒ P ∘ bL.






§ THE BOOM HIERARCHY: A CASE STUDY FOR DISTRIBUTIVE LAWS

We now pursue a detailed investigation of when distributive laws exist between some natural families of monads. To do so, we shall combine the techniques developed in earlier sections with results from the wider literature. Our objectives are to illustrate that the absence of distributive laws is not at all unusual, to document many useful examples, and to develop some intuitions via concrete applications.

We shall begin with the so-called Boom hierarchy, a small family of monads considered in the functional programming literature <cit.>. Later, to increase our available data points, we will expand the original Boom hierarchy to include more exotic, if slightly less natural, data structures. Similar expansions of the Boom hierarchy have been studied by Uustalu <cit.>.

The Boom hierarchy is a simple family of four monads, providing a pleasing connection between commonly used data structures and natural algebraic axioms.
The hierarchy consists of the tree, list, multiset, and powerset monads. Each of these monads has the same signature, consisting of a constant and a binary operation.
If the only axiom is the unitality axiom, the resulting monad is the binary tree monad. Adding associativity yields the list monad. Further adding commutativity yields the multiset monad, and finally adding idempotence results in the finite powerset monad, as shown in  <ref>.







  The Boom hierarchy is named after the Dutch Computer Scientist Hendrik Boom. The fact that `Boom' also means `tree' in Dutch is not entirely coincidental. Allegedly, the name was coined by Peter Grogono in a meeting with Stephen Spackman and Hendrik Boom. Spackman was a MSc student co-supervised by Grogono and Boom, working on this hierarchy of data structures. When Grogono suggested the name for the hierarchy, Boom's response was “What, because it is about trees?”. The name has stuck ever since <cit.>. Lambert Meertens is the first to mention this hierarchy in the literature <cit.>, citing an unpublished working paper by Boom <cit.>.







Studying the patterns of distributive laws in the Boom hierarchy provided some of the original inspiration for the abstract no-go theorems presented in earlier sections.
We now use the same hierarchy, and generalizations of it, to demonstrate both their scope and limitations, and their relationship to the existing positive results we are aware of in the literature.



 §.§ The Original Boom Hierarchy


For the original Boom hierarchy we have complete knowledge of possible compositions via distributive laws. An overview is presented in  <ref> below.

The negative result for P ∘ P ⇒ P ∘ P was already shown by Klin and Salamanca <cit.>, and can also be recovered from both  <ref> and <ref>. The other negative results follow from either  <ref> or  <ref>. Sometimes both theorems can be applied, for example to preclude a distributive law P ∘ L ⇒ L ∘ P.

The positive results are due to Manes and Mulry. They show that any monad with only linear equations in its presentation distributes over any commutative monad[A commutative monad is a strong monad for which the two possible double strengths coincide <cit.>. Algebraically, this means that all operations in the signature commute with one another. This is quite different from the algebraic property of commutativity that we consider in the Boom hierarchy.] via the times over plus distributivity <cit.>. The multiset and powerset monad are both commutative, and the theories of the tree, list and multiset monads all have solely linear equations.  This yields the six distributive laws indicated in the table.  <ref> proves that these distributive laws are in fact the only possible distributive laws for these monads.






In this small sample, Manes and Mulry's theorem is powerful enough to yield all the possible positive results. However,  <ref> is too small to draw general conclusions. To extract more information, we expand our hierarchy of monads in the next section.



 §.§ The Extended Boom Hierarchy


The original Boom hierarchy discussed in  <ref> consisted of a small number of well motivated data structures. Unfortunately, this small size means that it provides limited scope for identifying patterns in distributive law phenomena. To address this, we now consider an extended hierarchy in which all possible combinations of the original algebraic axioms appear, rather than the axioms being gradually added in a fixed order.
This yields a total of eight different monads: tree, idempotent tree, commutative tree (mobile), associative tree (list), idempotent and commutative tree, idempotent and associative tree (square-free list), associative and commutative tree (multiset), idempotent commutative and associative tree (powerset). If we additionally consider the non-empty versions of these monads, corresponding algebraically to removing the constant from the signature, the number of monads doubles to sixteen. Of course, some of these monads are less natural from a functional programming perspective, but they provide a convenient range of candidates for investigation.

An overview of these monads is given in  <ref> below. We have named the monads according to the axioms their theories satisfy: U(unitality), A(associativity), C(commutativity), I(idempotence). For example, multisets are associative and commutative trees with units, so they are denoted UAC in the table, whereas their non-empty version, which has no unit, is called AC. Note that this convention is unambiguous as we always impose the unitality axiom when the unit constant is present.






Within the extended Boom hierarchy, there are a total of 256 monad compositions to consider. Some distributive laws arise via Manes and Mulry's positive general theorems <cit.> and <cit.>. Other combinations are known to have a distributive law because an ad-hoc one has been found, for example for the non-empty list monad over itself <cit.>. A large number of the combinations are proven impossible by theorems from this paper. Our current knowledge about the existence of distributive laws for this extended Boom hierarchy is given in  <ref>.





Out of the 256 pairs of monads in  <ref>:


  * The 41 labelled with have a distributive law between them.

  * The 122 labelled with do not have a distributive law between them.

  * The remaining 93 pairs labelled with remain to be understood.

That is, almost half of the combinations of monads from the extended Boom hierarchy do not have a distributive law between them. The bottom right corner of  <ref> is especially striking. Every possible combination is understood, and 56 out of 64 combinations do not have a distributive law. This provides further evidence that we should not assume “most” monads will compose via suitable distributive laws.

An unsurprising pattern that emerges from  <ref> is that the axioms of idempotence and units are `bad' properties for monad compositions. Since all of our no-go theorems require at least one of these properties to hold, this observation does not lead to any new insights.

In the positive results, the most apparent patterns are the columns ∅, AC, ACI, UAC, and UACI. These are precisely the cases captured by Manes and Mulry.

For the remaining open cases, we cannot make any meaningful predictions. Our current techniques in no-go theorems require some way of bringing a term down to a variable, either via idempotence or via units. Whether this is the key property that prevents the existence of distributive laws remains an open question. On the other hand, all general positive results rely on one of the monads being commutative. The ad-hoc distributive law of the non-empty list monad over itself clearly indicates that commutativity is not a necessary condition for distributive laws to exist.

One thing is certain: to systematically fill in the gaps in  <ref> we will need additional ideas, supporting either further positive, or negative, theorems. As such, analyzing these hierarchies highlight directions which will deepen our understanding of distributive laws.



 §.§ Repeated Compositions

Another way to extend the original Boom hierarchy is to add the monads resulting from the six distributive laws appearing in  <ref>.
In order to study these additional monads, we first give concrete presentations for each of them:

 The presentations of the composite monads MT, ML, MM, PT, PL, PM are as follows:
  
  
  * The composite monad MT is presented by the following theory:
    
    
  * Signature: Σ^MT = {0^(0),1^(0),+^(2),*^(2)}.
    
  * Equations: 0 is the unit of +, + is associative and commutative, 1 is the unit of *, 0 is a multiplicative zero:
        
    0 * x     = 0
    
            x * 0     = 0,

        and * distributes over + from both left and right:
        
    x * (y + z)     = (x * y) + (x * z)
    
            (x + y) * z     = (x * z) + (y * z).

    
  
  * ML has the same signature and equations as MT, with the additional equation that * is associative.
  
  * MM also has the same signature and equations as MT, with * additionally being associative and commutative.
  
  * PT, PL, and PM have the same signatures and equations as MT, ML, and MM respectively, with one additional equation: + is idempotent.
  



We prove only that the given presentation for the monad MT is correct, the others follow similarly.
From  <ref>, we know that the composite monad MT has presentation:

    
    
  * Signature: Σ^MT = Σ^M ⊎Σ^T = {0^(0),1^(0),+^(2),*^(2)}.
    
  * Equations: E^MT = E^M ∪ E^T ∪ E^λ = { 0 is the unit of +, + is associative and commutative} ∪ { 1 is the unit of * } ∪ { s[t_x/x] MT t[s_y/y]  |  s, s_y terms in M, t, t_x terms in T}.
   
So all we need to show is that  (<ref>), (<ref>), (<ref>), and (<ref>) are enough to prove all equations in E^λ, that is, of form s[t_x/x] MT t[s_y/y].



To prove that all equations in E^λ are provable from the four given axioms, it is enough to show that each term of form s[t_x/x] is separable via the given axioms. Essential uniqueness then does the rest: Suppose that both s[t_x/x] MT t[s_y/y] and s[t_x/x] MT t'[s'_y'/y'] are in E^λ, and the first of these equations is provable using  (<ref>), (<ref>), (<ref>), and (<ref>). Then by transitivity of MT we know t'[s'_y'/y'] MT t[s_y/y]. Since this is an equality between two separated terms, essential uniqueness gives us that it is provable using just the axioms in E^M and E^T. So once we have derived one equation in E^λ involving a particular term s[t_x/x], we automatically gain all equations in E^λ involving this term.


To prove that every term of form s[t_x/x] is separable using just the axioms  (<ref>), (<ref>), (<ref>), and (<ref>), we use induction on the term complexity of s:

Base cases: s is a constant or a variable. In these cases s[t_x/x] is already separated.
Induction step: Suppose that s = s_1 * s_2, and assume that s_1[t_x/x] and s_2[t_x/x] are both separable using the four equations described above. Then we need to show that s[t_x/x] is separable. Let t'_1[s'_y'/y'] and t'_2[s'_y'/y'] be the terms resulting from separating s_1 and s_2 respectively. We need induction on both t'_1 and t'_2:

  
  * If t'_1 is a constant, t'_1 = 0, then by  (<ref>): s[t_x/x] = 0 * s_2 = 0, and hence s[t_x/x] is separable.
  
  
  * If t'_1 is a variable, t'_1 = x_1, we use induction t'_2:
   
   
  * If t'_2 is a constant, then by  (<ref>): s[t_x/x] = s_1 * 0 = 0, and hence s[t_x/x] is separable.
   
  * If t'_2 is a variable, t'_2 = x_2, then s[t_x/x] = x_1 * x_2, which is a separated term.
   
  * If t'_2 is term of form t'_3 + t'_4, and we assume (induction hypothesis) that x_1 * t'_3 is separable and x_1 * t'_4 is separable, then s[t_x/x] = x_1 * (t'_3 + t'_4). By  (<ref>), we can write:
       
    s[t_x/x] 
    
           =       x_1 * (t'_3 + t'_4) 
    
           =      (x_1 * t'_3) + (x_1 * t'_4).

       Since both (x_1 * t'_3) and (x_1 * t'_4) are separable, this shows that s[t_x/x] is separable.
    
    
  * If t'_1 is a term of form t'_5 + t'_6, we may assume (induction hypothesis) that t'_5 * t'_2 and t'_6 * t'_2 are separable. By  (<ref>), we know:
       
    s[t_x/x] 
    
           =       (t'_5 + t'_6) * t'_2 
    
           =      (t'_5 * t'_2) + (t'_6 * t'_2).

       Since both (t'_5 * t'_2) and (t'_6 * t'_2) are separable, this shows that s[t_x/x] is separable.

We conclude that the given presentation is indeed a presentation for the monad MT.

Checking these presentations against the various no-go theorems presented in this paper yields a new table of possible compositions, displayed in  <ref>.
Other than the six combinations we already discovered in the original Boom hierarchy, we find no new combinations of monads that compose via a distributive law.  The results shown in the columns of the composite monads MT, ML, MM, PT, PL, PM are covered by  <ref>, while the rows with any of these composite monads are covered by  <ref>.




§ CONCLUSION

We have shown there can be no distributive law between large classes of monads:


  * Section <ref> developed general theorems for demonstrating when distributive laws cannot exist, derived from a classical counterexample of Plotkin, making essential use of idempotence axioms.

  * Section <ref> introduced novel ideas, exploiting unitality axioms, yielding counterexamples beyond those possible in  <ref>.

  * Section <ref> developed a third family of no-go theorems, motivated by a question of Beck. Here the ability to “make variables disappear” in terms is central, such as in inverse and absorption axioms.

Our results cover many naturally occurring combinations of monads, including all previously known negative results. They also identify issues in the existing literature, resolve the open question of whether the list monad distributes over itself,
and confirm a negative conjecture of Beck.

We strongly advocated the use of algebraic methods. These techniques were used for all of our proofs. Taking this approach, rather than direct calculations involving Beck's axioms, enabled us to single out the essentials of each proof, so that the resulting theorems could be stated in full generality.

Lastly, we would like to emphasize that the methods described in this paper are of broader application, beyond our specific theorems. For example, Julian Salamanca found that there is no distributive law of the group monad over the powerset monad G ∘ P ⇒ P ∘ G <cit.>, before we formulated  <ref>. Although elements of his proof are very similar to those used in Section  <ref>, the proof itself uses further ideas outside the scope of our theorems.



 §.§ Summary of Axioms and Theorems

Our theorems use a range of different properties of algebraic theories. To aid navigation, we conclude with a summary of the properties that we exploit, and which theorems exploit them.

Our theorems typically require the existence of a special term with multiple properties, such as a binary term that is both idempotent and commutative. Below we list all these properties separately. Table <ref> then specifies which theorems require which properties to hold simultaneously for a single term. Note that some properties, such as <ref>, seem trivial on their own, but in conjunction with other properties we require of the special term in our theorems they are no longer trivial and must be stated as a requirement.


In addition, our theorems require certain properties to hold for the theories in question, such as the existence of a constant in the theory, or conditions that must hold for all terms in the theory, such as “if a term is equal to a constant, then it cannot have any variables”. In the list below, we split the properties into those that must hold for one special term, and those that must hold for the theory.



  * Properties of terms:


  * There is a binary term  such that:

  
  *   is idempotent:
        
    {x}⊢(x,x) = x

  
  *   has a unit:
  
    {x}⊢(x,e) = x = (e,x)

  
  *  There is a substitution f of terms for variables such that [f] is equal to a variable:
  
    ∃ f s.t. Γ⊢[f] = x

  
  *   is commutative:
  
    {x,y}⊢(x,y) = (y,x)

  
  *   does not satisfy the abides equation:
  
    (Γ⊢((x,y),(z,w)) = ((x,z),(y,w)))   ⇒  #{x,y,z,w}≤ 3

  
  *  Any term provably equal to  has at most two variables:
  
    ∀ : (Γ⊢(x,y) = )   ⇒  {x,y}⊢

  
  *  Any term provably equal to  has at least one variable:
  
    ∀ : (Γ⊢(x,y) = )   ⇒   (∅⊢)

  
  *  Any term provably equal to  has at least two variables:
  
    ∀ : (Γ⊢(x,y) = )   ⇒   ({x}⊢ ∨ {y}⊢)



  * There is an n-ary term  (n ≥ 2) such that:
 
  
  *   is idempotent:
         
    {x}⊢[x/x_i] = x

  
  *   has a unit:
  
    {x_i}⊢[e/x_j≠ i] = x_i

  
  *  There is a substitution f of terms for variables such that [f] is equal to a variable, and none of the terms in the range of f contain that variable:
  
    ∃ f s.t. Γ⊢[f] = x  ∧ ∀∈(f) :  (x ∈())

  
  *   is stable under a fixed-point free permutation σ of its variables:
  
    Γ⊢ = [σ]

  
  *  Any term provably equal to  has at most n variables:
  
    ∀ : (Γ⊢(x_1,…,x_n) = )   ⇒  {x_1,…,x_n}⊢

  
  *  Any term provably equal to  has at least two variables:
  
    ∀ : (Γ⊢ = )   ⇒   (⋁_x ∈Γ{x}⊢)



  * There is an n-ary term  (n ≥ 1) such that:
 
  
  *  There is a substitution f of terms for variables such that [f] is equal to a variable, and none of the terms in the range of f contain that variable:
  
    ∃ f s.t. Γ⊢[f] = x  ∧ ∀∈(f) :  (x ∈())

  
  *   can be written as [_i/x_i], such that  and  share at least one variable, and <ref> holds for .
  
  *   is provably equal to a constant, but contains at least one variable:
  
    ∃ e s.t. (∅⊢ e)  ∧  (e = )  ∧  (∅⊢)

  
  *  There is a term  that is provably equal to , and  contains a variable that  does not have. Moreover,  satisfies <ref>.
  
    ∃ s.t. (Γ⊢ = )  ∧ ()∖() ≠∅




  * Properties of theories:


  * The algebraic theory in question must satisfy:
 

  *  For all terms  of arity ≥ 1 there is a substitution f of terms for variables such that [f] is equal to a variable, and none of the terms in the range of f contain that variable:
    
    ∀ ∃ f s.t. Γ⊢[f] = x   ∧ ∀∈(f) :  (x ∈())


  *  There exists a constant term in the theory. That is, there is a term that has no variables.

    ∃ e s.t. ∅⊢ e


  *  There are at least two constants.

  *  If any variable substitution of a term is equal to a constant, then that term itself is equal to a constant:

    ∀, e : (∃ f s.t. [f] = e)   ⇒   = e


  *  If a term is provably equal to a constant, then it does not have any variables:

    ∀, e : (∅⊢ e ∧ e = )   ⇒  ∅⊢


  *  If a term is provably equal to a variable, then that variable is the only variable appearing in the term:

    ∀, x : (Γ⊢ = x)    ⇒  {x}⊢
































































































An overview of our theorems and which axioms they use is presented in  <ref>. 
We advise to use this table only as a quick reference, and to always check the precise statements of the theorems before drawing any conclusions about specific monads.




§ ACKNOWLEDGEMENTS


We are very grateful to Jeremy Gibbons, Bartek Klin, Hector Miller-Bakewell, Julian Salamanca and our reviewers for their insightful feedback on earlier versions of this paper. We also would like to thank Prakash Panangaden, Fredrik Dahlqvist, Louis Parlant, Sam Staton, Ohad Kammar, Jules Hedges, and Ralf Hinze for inspiring discussions, which all had a positive influence on this paper.

This work was partially supported by Institute for Information & communications Technology Promotion(IITP) grant funded by the Korea government(MSIT) (No.2015–0–00565, Development of Vulnerability Discovery Technologies for IoT Software Security).



alphaurl




