<p>Augmenting Andrej's answer:</p>

<p>There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's <a href="https://hackage.haskell.org/package/mtl" rel="noreferrer">MTL</a> is the de-facto interface, but Jaskelioff's <a href="https://hackage.haskell.org/package/Monatron" rel="noreferrer">Monatron</a> is an alternative.</p>

<p>One of the earlier technical reports by Moggi, <a href="http://www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf" rel="noreferrer">an abstract view of programming languages</a>, discusses what should be the right notion of transformer to some extent (section 4.1). In particular, he discusses the notion of an operation for a monad, which he (20 years later) revisits with Jaskelioff in <a href="http://www.disi.unige.it/person/MoggiE/ftp/tcs10.pdf" rel="noreferrer">monad transformers as monoid transformers</a>. </p>

<p>(This notion of operation is different from Plotkin and Power's notion of an <a href="http://homepages.inf.ed.ac.uk/gdp/publications/sem_alg_ops.pdf" rel="noreferrer">algebraic operation for a monad</a>, which amounts to a Kleisli arrow.)</p>

CC BY-SA 3.0
2014-09-18T09:46:53.013Z
2014-09-18T10:38:11.713Z
2014-09-18T10:38:11.713Z
Ohad Kammar
<p>How could monad transformers be described in the terms of category theory?</p>
<p>There are two definitions: the &quot;weak&quot; and the &quot;functorial&quot; one.</p>
<p>The &quot;functorial&quot; definition is that a monad transformer is &quot;just a pointed endofunctor in the category of monads, what's the problem?&quot;.</p>
<p>This definition, however, does not describe the known transformers for the continuation monad, the codensity monad, and some other rarely used monads, because those transformers are not functors. Full details are worked out in Chapter 14 of the book &quot;The Science of Functional Programming&quot;. <a href="https://github.com/winitzki/sofp" rel="nofollow noreferrer">https://github.com/winitzki/sofp</a></p>
<p>The &quot;weak&quot; definition is that a monad transformer should give a lawful monad <code>T(M)</code> for any monad <code>M</code>, and that there must exist a monad morphism <code>M -&gt; T(M)</code>. I will argue below that this definition is too weak to be adequate.</p>
<p>Let me expand on the &quot;functorial&quot; definition and answer the three questions posed initially.</p>
<p>What is a &quot;pointed endofunctor in the category of monads&quot;?</p>
<p>It is an endofunctor <code>T</code> that transforms an arbitrary monad <code>M</code> into another monad <code>T(M)</code> and an arbitrary monad morphism <code>f : M -&gt; N</code> into another monad morphism <code>T(f): T(M) -&gt; T(N)</code>. (This function is sometimes called <code>hoist</code>.) The laws of monad and monad morphisms must hold.</p>
<p>In addition, <code>T</code> is “pointed”, meaning that there is a natural transformation <code>lift: ID -&gt; T</code>, where <code>ID</code> is the identity endofunctor that maps each monad to itself: <code>ID(M) = M</code>.</p>
<p>The laws of functors and of natural transformations must hold for <code>T</code> and <code>lift</code> respectively.</p>
<p>Let us see how the natural transformation <code>ID -&gt; T</code> works. This natural transformation's component at monad <code>M</code> is a morphism <code>lift(M): ID(M) -&gt; T(M)</code> or equivalently <code>M -&gt; T(M)</code>, and this must be a lawful monad morphism since we are in the category of monads. The monad morphism <code>M -&gt; T(M)</code> embeds the effects of <code>M</code> into the bigger monad <code>T(M)</code>.</p>
<p>This expresses the intent of a monad transformer: to add some features to arbitrary monads M and obtain new “bigger” monads T(M) that have all the features of M and in addition some other features. Right now we have embedded M into T(M).</p>
<p>What is the &quot;base monad&quot; corresponding to <code>T</code>? Let us apply <code>T</code> to the identity monad (<code>Id</code>). The identity monad is defined by <code>Id a = a</code>. So, <code>T(Id)</code> is some other monad, which we may denote by <code>L</code> for brevity. This is what we call the &quot;base monad&quot; of <code>T</code>. Why? Because, as we will now see, there is a monad morphism <code>L -&gt; T(M)</code> for any monad <code>M</code>.</p>
<p>Indeed, for any monad <code>M</code> we have a monad morphism <code>Id -&gt; M</code>. (This is the “return” method.) Applying the functor <code>T</code> to this morphism, we get a monad morphism <code>T(Id) -&gt; T(M)</code>, or equivalently <code>L -&gt; T(M)</code>. In this way, we have embedded the base monad <code>L</code> into <code>T(M)</code>.</p>
<p>To summarize, we have an endofunctor <code>T</code> and two monads <code>L</code>, <code>M</code> such that we can embed <code>L -&gt; T(M)</code> and <code>M -&gt; T(M)</code> via monad morphisms. So, in this sense, the “bigger” monad <code>T(M)</code> supports all the effects of <code>L</code> and also all the effects of <code>M</code>. We have succeeded in combining the effects of a monad <code>L</code> and an arbitrary monad <code>M</code> in a “bigger” monad <code>T(M)</code>.</p>
<p>Now, the monad <code>L</code> is fixed for a given <code>T</code> but the monad <code>M</code> is arbitrary. So, if we want to be able to combine the effects of any two monads, we should have for any monad <code>L</code> the corresponding <code>T</code> such that <code>T(Id) = L</code>.</p>
<p>In practice, we have a certain limited set of known monads <code>L</code> for which we know how to construct the corresponding <code>T</code>. However, there is no general method for finding <code>T</code> given <code>L</code>.</p>
<p>Because transformers are pointed functors (in the category of monads), the functor composition of transformers is again a transformer. This explains why monad transformers compose even though monads do not.</p>
<p>What is a &quot;monad transformer stack&quot;? It is a composition of two or more monad transformers, acting on a monad <code>M</code> as <code>T1(T2(T3(M)))</code>. The result is a functor that transforms a foreign monad <code>M</code> into a complicated, big monad <code>T1(T2(T3(M)))</code>.</p>
<p>Suppose that each monad <code>L</code> has a single, fixed, designated transformer <code>LT</code> such that <code>LT(Id) = L</code>. Then we can pretend that we are able to mix any two monads <code>L</code> and <code>M</code>. Define the binary operation <code>**</code> on monads by <code>L ** M = LT(M)</code>. The operation <code>(L **)</code> is (for fixed <code>L</code>) the same as the endofunctor <code>T</code> in the category of monads, but it allows us to avoid writing <code>T</code> explicitly. Then we also find that the operation <code>**</code> is associative. The associativity of <code>**</code> means that we <em>define</em> the transformer of <code>L1 ** L2</code> as <code>L1T(L2T(M))</code>. Then we can write monad stacks simply as <code>K ** L ** M ** N</code> without parentheses.</p>
<p>There are some remaining questions:</p>
<ul>
<li>There are certain transformers <code>T</code> where the morphisms <code>M -&gt; T(M)</code> exist but <code>L -&gt; T(M)</code> does not exist. Those transformers <code>T</code> are not actually endofunctors in the category of monads because there is no functor map <code>T(f)</code> on monad morphisms <code>f: M -&gt; N</code>. Examples are the continuation monad and the codensity monad as well as some other rarely used monads.</li>
</ul>
<p>There are specific practical implications of the fact that some monads do not have functorial transformers. The implications are that those monads cannot be used at arbitrary places in monad stacks, because their effects cannot be lifted into the stack. To be able to use the monad stack, the continuation monad needs to be at the deep end of the stack (<code>K ** L ** M ** Cont</code>). The same applies to any monad that does not have a transformer.</p>
<p>This also implies that monad stacks may contain at most one monad that doesn't have a functorial transformer. Otherwise, programmers will be quite constrained in how effects are combined and lifted into the stack.</p>
<ul>
<li>The &quot;weak&quot; definition of the monad transformer specifies that there should be just a monad morphism <code>M -&gt; T(M)</code>; the morphism <code>L -&gt; T(M)</code> is not required. According to the &quot;weak&quot; definition, the continuation monad and the codensity monad do have transformers. In fact, all explicitly known monads have  transformers according to the &quot;weak&quot; definition.</li>
</ul>
<p>Why is the requirement of having just <code>M -&gt; T(M)</code> too weak? As a counterexample, let us define <code>T(M) = Unit</code> for all <code>M</code>. Then we will always have a monad morphism <code>M -&gt; T(M)</code>. So, the &quot;weak&quot; definition allows us to have nonsensical, useless transformers such as this &quot;Unit&quot; transformer. The &quot;Unit&quot; transformer discards all effects and all values and does not represent in any way the effects of any monads; so, it is quite useless in practice, but it satisfies the &quot;weak&quot; definition.</p>
<p>It is <em>not clear</em> how to relax the &quot;functorial&quot; definition of the monad transformer so that nonsensical transformers are excluded.</p>
<ul>
<li><p>Is it really true that each monad <code>L</code> (defined by explicit purely functional code) has at least one corresponding transformer even with the &quot;weak&quot; definition? This is an open research question but so far there are no known examples of monads without transformers, at least according to the &quot;weak&quot; definition.</p>
</li>
<li><p>How to construct a monad transformer for a given monad? The state-of-the-art answer is a collection of 6 or 7 different recipes that do not seem to have any common method behind them. There is no general type construction that works in all cases. Manzuk's paper (referenced above) defines monad transformers via adjunctions but this gives a working recipe only in a couple of cases.</p>
</li>
<li><p>There are several examples of monads with more than one transformer according to the &quot;weak&quot; definition. However, there are no examples of monads with more than one &quot;functorial&quot; transformer. Is this a general property?</p>
</li>
</ul>

CC BY-SA 4.0
2021-05-18T19:42:33.927Z
2024-02-25T16:03:57.163Z
2024-02-25T16:03:57.163Z
winitzki
<p>I would highly recommend the book book by Bartosz Milewski &quot;Category Theory for Programmers&quot; which goes into some detail about Monads from a Category Theoretic perpective. And it's also available freely online :</p>
<p><a href="https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/" rel="nofollow noreferrer">https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/</a></p>

CC BY-SA 4.0
2021-05-18T20:52:23.643Z
2021-05-18T20:52:23.643Z
Robert Long
<p>According to Oleksandr Manzuk, they are &quot;translation of a monad along an adjunction&quot;, see <a href="https://web.archive.org/web/20221231192524/https://oleksandrmanzyuk.files.wordpress.com/2012/02/calc-mts-with-cat-th1.pdf" rel="nofollow noreferrer">&quot;Calculating Monad Transformers with Category Theory&quot;</a>. By the way, that's the third hit on Google for &quot;monad transformer categorically&quot;. The first is a Stackoverflow question about this and the second is your question.</p>

CC BY-SA 4.0
2021-05-23T21:07:06.910Z
Alas, the problem with Manzuk's construction is that it only works for a handful of monad transformers where the correct adjunction can be guessed. All other monad transformers cannot be derived from that construction. Also, there are typically several adjunctions that give the same monad; but only one of them (if at all) will give the correct transformer.
winitzki
CC BY-SA 4.0
2014-09-17T21:39:28.273Z
2024-02-24T22:14:16.777Z
2024-02-24T22:14:16.777Z
Andrej Bauer
<p>Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers.</p>

<p><strong>How could <a href="https://en.wikibooks.org/wiki/Haskell/Monad_transformers">monad transformers</a> be described in the terms of category theory?</strong></p>

<p>In particular, I'd be interested in:</p>

<ul>
<li>the relationship between monad transformers and their corresponding base monads;</li>
<li>the relationship between them and the monads they're transforming into new monads;</li>
<li>monad transformer stacks.</li>
</ul>

<type-theory><functional-programming><ct.category-theory><haskell><monad>
Explaining monad transformers in categorical terms
Petr
# Explaining monad transformers in categorical terms

(Asked by: username_0 on 2014-09-17)

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers.

**How could [monad transformers](https://en.wikibooks.org/wiki/Haskell/Monad_transformers) be described in the terms of category theory?**

In particular, I'd be interested in:

* the relationship between monad transformers and their corresponding base monads;
* the relationship between them and the monads they're transforming into new monads;
* monad transformer stacks.

**Tags:** type-theory, functional-programming, ct.category-theory, haskell, monad


---

## 4 answers

### Answer by username_4 on 2014-09-17. Score: 11 | Accepted answer

According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see ["Calculating Monad Transformers with Category Theory"](https://web.archive.org/web/20221231192524/https://oleksandrmanzyuk.files.wordpress.com/2012/02/calc-mts-with-cat-th1.pdf). By the way, that's the third hit on Google for "monad transformer categorically". The first is a Stackoverflow question about this and the second is your question.

> **Comments:**
> **username_2**: Alas, the problem with Manzuk's construction is that it only works for a handful of monad transformers where the correct adjunction can be guessed. All other monad transformers cannot be derived from that construction. Also, there are typically several adjunctions that give the same monad; but only one of them (if at all) will give the correct transformer.  

---

### Answer by username_1 on 2014-09-18. Score: 9

Augmenting Andrej's answer:

There is still no widespread agreement on the appropriate interface monad transformers should support in the functional programming context. Haskell's [MTL](https://hackage.haskell.org/package/mtl) is the de-facto interface, but Jaskelioff's [Monatron](https://hackage.haskell.org/package/Monatron) is an alternative.

One of the earlier technical reports by Moggi, [an abstract view of programming languages](http://www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf), discusses what should be the right notion of transformer to some extent (section 4.1). In particular, he discusses the notion of an operation for a monad, which he (20 years later) revisits with Jaskelioff in [monad transformers as monoid transformers](http://www.disi.unige.it/person/MoggiE/ftp/tcs10.pdf).

(This notion of operation is different from Plotkin and Power's notion of an [algebraic operation for a monad](http://homepages.inf.ed.ac.uk/gdp/publications/sem_alg_ops.pdf), which amounts to a Kleisli arrow.)


---

### Answer by username_2 on 2021-05-18. Score: 2

How could monad transformers be described in the terms of category theory?

There are two definitions: the "weak" and the "functorial" one.

The "functorial" definition is that a monad transformer is "just a pointed endofunctor in the category of monads, what's the problem?".

This definition, however, does not describe the known transformers for the continuation monad, the codensity monad, and some other rarely used monads, because those transformers are not functors. Full details are worked out in Chapter 14 of the book "The Science of Functional Programming". <https://github.com/username_2/sofp>

The "weak" definition is that a monad transformer should give a lawful monad `T(M)` for any monad `M`, and that there must exist a monad morphism `M -> T(M)`. I will argue below that this definition is too weak to be adequate.

Let me expand on the "functorial" definition and answer the three questions posed initially.

What is a "pointed endofunctor in the category of monads"?

It is an endofunctor `T` that transforms an arbitrary monad `M` into another monad `T(M)` and an arbitrary monad morphism `f : M -> N` into another monad morphism `T(f): T(M) -> T(N)`. (This function is sometimes called `hoist`.) The laws of monad and monad morphisms must hold.

In addition, `T` is “pointed”, meaning that there is a natural transformation `lift: ID -> T`, where `ID` is the identity endofunctor that maps each monad to itself: `ID(M) = M`.

The laws of functors and of natural transformations must hold for `T` and `lift` respectively.

Let us see how the natural transformation `ID -> T` works. This natural transformation's component at monad `M` is a morphism `lift(M): ID(M) -> T(M)` or equivalently `M -> T(M)`, and this must be a lawful monad morphism since we are in the category of monads. The monad morphism `M -> T(M)` embeds the effects of `M` into the bigger monad `T(M)`.

This expresses the intent of a monad transformer: to add some features to arbitrary monads M and obtain new “bigger” monads T(M) that have all the features of M and in addition some other features. Right now we have embedded M into T(M).

What is the "base monad" corresponding to `T`? Let us apply `T` to the identity monad (`Id`). The identity monad is defined by `Id a = a`. So, `T(Id)` is some other monad, which we may denote by `L` for brevity. This is what we call the "base monad" of `T`. Why? Because, as we will now see, there is a monad morphism `L -> T(M)` for any monad `M`.

Indeed, for any monad `M` we have a monad morphism `Id -> M`. (This is the “return” method.) Applying the functor `T` to this morphism, we get a monad morphism `T(Id) -> T(M)`, or equivalently `L -> T(M)`. In this way, we have embedded the base monad `L` into `T(M)`.

To summarize, we have an endofunctor `T` and two monads `L`, `M` such that we can embed `L -> T(M)` and `M -> T(M)` via monad morphisms. So, in this sense, the “bigger” monad `T(M)` supports all the effects of `L` and also all the effects of `M`. We have succeeded in combining the effects of a monad `L` and an arbitrary monad `M` in a “bigger” monad `T(M)`.

Now, the monad `L` is fixed for a given `T` but the monad `M` is arbitrary. So, if we want to be able to combine the effects of any two monads, we should have for any monad `L` the corresponding `T` such that `T(Id) = L`.

In practice, we have a certain limited set of known monads `L` for which we know how to construct the corresponding `T`. However, there is no general method for finding `T` given `L`.

Because transformers are pointed functors (in the category of monads), the functor composition of transformers is again a transformer. This explains why monad transformers compose even though monads do not.

What is a "monad transformer stack"? It is a composition of two or more monad transformers, acting on a monad `M` as `T1(T2(T3(M)))`. The result is a functor that transforms a foreign monad `M` into a complicated, big monad `T1(T2(T3(M)))`.

Suppose that each monad `L` has a single, fixed, designated transformer `LT` such that `LT(Id) = L`. Then we can pretend that we are able to mix any two monads `L` and `M`. Define the binary operation `**` on monads by `L ** M = LT(M)`. The operation `(L **)` is (for fixed `L`) the same as the endofunctor `T` in the category of monads, but it allows us to avoid writing `T` explicitly. Then we also find that the operation `**` is associative. The associativity of `**` means that we *define* the transformer of `L1 ** L2` as `L1T(L2T(M))`. Then we can write monad stacks simply as `K ** L ** M ** N` without parentheses.

There are some remaining questions:

* There are certain transformers `T` where the morphisms `M -> T(M)` exist but `L -> T(M)` does not exist. Those transformers `T` are not actually endofunctors in the category of monads because there is no functor map `T(f)` on monad morphisms `f: M -> N`. Examples are the continuation monad and the codensity monad as well as some other rarely used monads.

There are specific practical implications of the fact that some monads do not have functorial transformers. The implications are that those monads cannot be used at arbitrary places in monad stacks, because their effects cannot be lifted into the stack. To be able to use the monad stack, the continuation monad needs to be at the deep end of the stack (`K ** L ** M ** Cont`). The same applies to any monad that does not have a transformer.

This also implies that monad stacks may contain at most one monad that doesn't have a functorial transformer. Otherwise, programmers will be quite constrained in how effects are combined and lifted into the stack.

* The "weak" definition of the monad transformer specifies that there should be just a monad morphism `M -> T(M)`; the morphism `L -> T(M)` is not required. According to the "weak" definition, the continuation monad and the codensity monad do have transformers. In fact, all explicitly known monads have transformers according to the "weak" definition.

Why is the requirement of having just `M -> T(M)` too weak? As a counterexample, let us define `T(M) = Unit` for all `M`. Then we will always have a monad morphism `M -> T(M)`. So, the "weak" definition allows us to have nonsensical, useless transformers such as this "Unit" transformer. The "Unit" transformer discards all effects and all values and does not represent in any way the effects of any monads; so, it is quite useless in practice, but it satisfies the "weak" definition.

It is *not clear* how to relax the "functorial" definition of the monad transformer so that nonsensical transformers are excluded.

* Is it really true that each monad `L` (defined by explicit purely functional code) has at least one corresponding transformer even with the "weak" definition? This is an open research question but so far there are no known examples of monads without transformers, at least according to the "weak" definition.
* How to construct a monad transformer for a given monad? The state-of-the-art answer is a collection of 6 or 7 different recipes that do not seem to have any common method behind them. There is no general type construction that works in all cases. Manzuk's paper (referenced above) defines monad transformers via adjunctions but this gives a working recipe only in a couple of cases.
* There are several examples of monads with more than one transformer according to the "weak" definition. However, there are no examples of monads with more than one "functorial" transformer. Is this a general property?


---

### Answer by username_3 on 2021-05-18. Score: 1

I would highly recommend the book book by Bartosz Milewski "Category Theory for Programmers" which goes into some detail about Monads from a Category Theoretic perpective. And it's also available freely online :

<https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/>


---

