<p>The equation <code>F Id ≅ ∀ (m: Monad). F m</code> seems to be correct (for most transformers <code>F</code>, see below). However, I would not say that &quot;a monad transformer is equivalent to its base monad&quot;. A monad transformer probably carries more information than its base monad, because there is no known way of mechanically converting a given base monad into its monad transformer.</p>
<p>By definition, a transformer's base monad can be obtained by applying the transformer to <code>Id</code>. This is denoted by <code>F Id</code>. You claim that <code>F Id ≅ ∀ (m: Monad). F m</code>. This seems to be correct.</p>
<p>Also you are correct that a proof will involve parametricity at the level of monads.</p>
<p>A possible proof could go like this. Consider the category of monads: objects are monads and arrows are monad morphisms. In that category, a monad transformer is an endofunctor. (This is true for almost all monad transformers, except <code>Continuation</code> and <code>Codensity</code> and some other variants of those monads. See <a href="https://stackoverflow.com/questions/63882053/whats-a-functor-on-the-category-of-monads?rq=3">https://stackoverflow.com/questions/63882053/whats-a-functor-on-the-category-of-monads?rq=3</a> and see also my answers in <a href="https://cstheory.stackexchange.com/questions/25783/explaining-monad-transformers-in-categorical-terms">Explaining monad transformers in categorical terms</a> and in <a href="https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io">https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io</a> .)</p>
<p>Then we want to prove the following property:</p>
<pre><code> F Id ≅ ∀ (m: Monad). F m
</code></pre>
<p>where <code>∀ (m: Monad)</code> goes over all monads.</p>
<p>The first step is to prove that the identity monad <code>Id</code> is an initial object in the category of monads. For any given monad <code>M</code>, there is only one monad morphism between <code>Id</code> and <code>M</code> (that morphism is given by the monad <code>M</code>'s <code>unit</code> method, <code>unit: ∀ a. Id a → M a</code>).  I omit the proof of this property.</p>
<p>The second step is to use the Yoneda lemma (still in the category of monads). The Yoneda lemma says: For any Set-valued functor <code>G</code> (that is, a functor from the category of monads to the category of sets), the Yoneda lemma says:</p>
<pre><code> G X ≅ Nat(Hom(X, _), G)  ,
</code></pre>
<p>where <code>Nat(K, L)</code> is the set of natural transformations between functors <code>K</code> and <code>L</code>; <code>Hom(X, _)</code> is the Set-valued functor that maps a given monad <code>M</code> into the set of morphisms (in the category of monads) between the monads <code>X</code> and <code>M</code>.</p>
<p>Now we want to apply the Yoneda lemma to our situation where <code>G = F</code> is our monad transformer endofunctor. But then there is a technical difficulty: we cannot use the Yoneda lemma because <code>G</code> is not a set-valued functor (it's a monad-valued functor). We need to map monads into sets in some way. This is not straightforward; for instance, it is not clear how to choose a set that would correspond to the <code>List</code> monad or to the <code>Maybe</code> monad. It is easier to introduce a type parameter <code>t</code> and talk about the type <code>List t</code> or <code>Maybe t</code>. For any given type <code>t</code> there is a well-defined set of all values of type <code>List t</code>. So, we can temporarily choose some arbitrary type <code>t</code> and define a set-valued functor <code>G</code> that maps a monad <code>m</code> into the set of all values of type <code>(F m) t</code>. For this functor <code>G</code>, the Yoneda lemma shown above will hold.</p>
<p>The third step is to choose <code>X = Id</code> in the Yoneda lemma and find:</p>
<pre><code> G Id ≅ Nat(Hom(Id, _), G)
</code></pre>
<p>The fourth step is to see why it makes sense to write the right-hand side as <code>∀ (m: Monad). G m</code> in the notation of a programming language. In fact, since we are working in a purely functional language where parametricity holds, any value of type <code>∀ (m: Monad). G m</code> must be implemented in a way that is fully parametric in the monad <code>m</code>: it may use only the monad <code>m</code>'s methods but no other knowledge about <code>m</code>.</p>
<p>The set <code>Hom(Id, M)</code> is a single-element set because <code>Id</code> is an initial object and there is only one monad morphism between <code>Id</code> and <code>M</code>. So, the functor <code>Hom(Id, _)</code> is a constant functor that maps any object into a single-element set.</p>
<p>What is the set of natural transformations between that constant functor and <code>G</code>? A component at <code>m</code> of such a transformation is a morphism of type <code>Hom(Id, m) =&gt; G m</code>. Here <code>=&gt;</code> means the arrow in the category <code>Set</code>.</p>
<p>But <code>Hom(Id, m)</code> is a single-element set. So, a morphism <code>Hom(Id, m) =&gt; G m</code> is the same as just choosing one element in the set <code>G m</code>.</p>
<p>We find that a natural transformation between <code>Hom(Id, _)</code> and <code>G</code> is the same as a choice, for each monad <code>m</code>, of an element in the set <code>G m</code> in a way that does not depend on the monad <code>m</code> other than through the monad <code>m</code>'s methods (in other words, in a fully parametric way). An element in the set <code>G m</code> is the same as a value of type <code>F m t</code>. In a programming language, we would write that as the type <code>∀ (m: Monad). F m t</code> assuming that values of that type must be fully parametric. The assumption of parametricity allows us to use the parametricity theorem and is necessary because otherwise the values of type <code>∀ (m: Monad). F m t</code> would <em>not</em> correspond to natural transformations.</p>
<p>In this way we find, in a programming language notation, that:</p>
<pre><code> (F Id) t ≅ ∀ (m: Monad). F m t
</code></pre>
<p>This holds for all types <code>t</code>. So, we can rewrite this identity more concisely as:</p>
<pre><code> F Id ≅ ∀ (m: Monad). F m
</code></pre>
<p>There are certainly some rough edges in this sketch of a proof, but I'm not sufficiently well-versed in category theory to polish it off.</p>
<p>The analogy with the Yoneda lemma for ordinary types and endofunctors gives the following equivalence between types:</p>
<pre><code>F 0 ≅ ∀ t. F t
</code></pre>
<p>because <code>0</code> is an initial object in the category of types.</p>

CC BY-SA 4.0
2023-09-06T13:41:31.073Z
How do I get around the rought edge `F X ≅ ∀ m. (X → m) => F m`? The left-hand side is a set. How do I read the right-hand side as a set? I expected `F X ≅ Nat(Hom(X, _), F)` which sort of looks like what you wrote, but I am not sure.
Andrej Bauer
CC BY-SA 4.0
2023-09-06T20:52:07.210Z
I haven't heard about the category of monads. And I can't find a reference on the internet. Could you provide one?
Russoul
CC BY-SA 4.0
2023-09-08T18:33:17.490Z
@AndrejBauer You may be right about `F X ≅ Nat(Hom(X, _), F)` but I wish I had a more immediate grasp of the Yoneda lemma in a general category. In principle we just need to write the Yoneda lemma in the category of monads and put `F` into the right place and then set `X = Id`. Isn't `Nat(Hom(X, _), F)` a set?
winitzki
CC BY-SA 4.0
2023-09-08T18:35:36.480Z
@Russoul There isn't a reference that I have in mind. We just consider a category whose objects are various monads in the usual sense (Maybe, List, State s, Identity  etc.) and whose morphisms are monad morphisms.
winitzki
CC BY-SA 4.0
2023-09-08T20:11:09.943Z
@winitzki: The basic question I have is, in what sense is `∀ m. (Id → m) => F m` a set? What does it mean to quantify with `∀` and get a set out?
Andrej Bauer
CC BY-SA 4.0
2023-09-08T21:51:14.767Z
@winitzki What is a monad morphism?
Russoul
CC BY-SA 4.0
2023-09-11T12:30:50.673Z
@AndrejBauer The notation `∀ m. (Id → m) => F m` is inspired by programming languages where we would write a type expression like that. The type `∀ a. K a → L a` is a type of natural transformations between endofunctors.  In category theory we will just say that there is a set of natural transformations between some functors and then, I guess, we should not write quantifiers any more. So, let's write the Yoneda lemma as `F X ≅ Nat(Hom(X, _), F)`. The right-hand side is a set of all natural transformations between set-valued functors `Hom(X, _)` and `F`. Let me try to edit my answer.
winitzki
CC BY-SA 4.0
2023-09-11T12:34:11.650Z
@Russoul A monad morphism `f: M → N` between two monads `M` and `N` is a natural transformation that satisfies suitable laws (in this case, the identity and the composition laws). https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html  The intuition is that `f` is a transformation that preserves the monad's methods.
winitzki
CC BY-SA 4.0
2023-09-11T15:21:43.083Z
I am not enough of a Haskell desciple to be able to take this amount of "fast & loose" reasoning, although it certainly points to how one would prove the claims rigorously.
Andrej Bauer
CC BY-SA 4.0
2023-09-11T16:59:33.070Z
@AndrejBauer  I have revised my answer and removed the quantifier in that place where you were objecting.
winitzki
CC BY-SA 4.0
2023-09-12T08:57:33.860Z
At this point I am confused abot something from the very beginning. If $F$ is an endofunctor, how can we use the Yoneda lemma on it? Or more preicsely, where does the `Nat(Hom(Id, _), F)` happen? The functor `F` is an endofunctor, whereas `Hom(Id, _)` maps to sets.
Andrej Bauer
CC BY-SA 4.0
2023-09-12T10:05:24.407Z
@AndrejBauer You are right. This is another helpful confusion coming from programming languages, where every type (including function types) is treated as a set. The endofunctor $F$ must be re-interpreted as a set-valued functor in order to apply Yoneda. Let me try to revise my answer again.
winitzki
CC BY-SA 4.0
2023-09-12T10:56:48.397Z
It might be better to go the other way an interpret `Hom(Id, _)` as an internal expoent, if such a thing exists.
Andrej Bauer
CC BY-SA 4.0
2023-09-12T18:08:26.193Z
@Russoul I have revised and expanded my answer, please let me know if you have questions.
winitzki
CC BY-SA 4.0
2023-09-12T19:29:29.140Z
@AndrejBauer If `Hom(X, Y)` were an internal exponent in the category of monads then we must be able to convert `Hom(X, Y)`, where `X` and `Y` are any given monads, into a new monad. I'm not sure it's possible because `Hom(X, Y)` is the set of all monad morphisms between monad `X` and `Y`. It's not clear in what way the set of all monad morphisms is equivalent to a new monad. For some `X` and `Y` there are no monad morphisms in `Hom(X, Y)`.
winitzki
CC BY-SA 4.0
2023-10-01T08:41:29.217Z
@winitzki I believe it's not enough to preserve just monad methods.
You have to preserve `map` as well. Otherwise I can't prove that monads form a category.
Russoul
CC BY-SA 4.0
2023-10-01T10:37:02.457Z
Otherwise, I've been able to follow your explanation through. And formally show it for StateT, though with some proofs missing (require parametricity). Thanks a lot!
Russoul
CC BY-SA 4.0
2023-10-02T10:19:17.200Z
@Russoul Of course you need to preserve `map` but a monad morphism is by definition a *natural transformation* that preserves the monad methods. Preserving `map` is exactly the same as "being a natural transformation".
winitzki
CC BY-SA 4.0
2023-10-03T10:28:04.243Z
@winitzki Indeed. Thanks again!
Russoul
CC BY-SA 4.0
2023-09-06T13:13:28.923Z
2023-09-18T08:23:18.470Z
2023-09-18T08:23:18.470Z
winitzki
<p>Question originally asked in proofassistants.stackexchange</p>
<p>Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-order version of parametricity/theorems-for-free is needed to show this.</p>
<p>A concrete instance of the problem:</p>
<pre><code>∀s. ∀a. (State s a ≅ (∀m. Monad m → StateT s m a))
</code></pre>
<p>In general the problem can be stated informally like so:</p>
<pre><code>∀a. (MonadT Id a ≅ (∀ m. Monad m → MonadT m a))
</code></pre>
<p>where <code>MonadT</code> is a &quot;schema&quot; standing for arbitrary monad transformer.</p>
<p>The background type theory can be assumed to be system F or some dependent type theory consistent with parametricity. Depending on the theory used, the statement can be either internal or external.</p>

CC BY-SA 4.0
2023-09-06T14:40:50.067Z
This is a long shot, but could the methods used in [On Monadic Parametricity of Second-Order Functionals](http://dx.doi.org/10.1007/978-3-642-37075-5_15) be adapted?
Andrej Bauer
CC BY-SA 4.0
2023-09-12T10:25:07.843Z
@AndrejBauer This is very interesting, thank you!
winitzki
<type-theory><monad><parametricity>
Is is true that every monad transformer is equivalent to its underlying/base monad?
Russoul
# Is is true that every monad transformer is equivalent to its underlying/base monad?

(Asked by: username_0 on 2023-09-06)

Question originally asked in proofassistants.stackexchange
Just like the title says, is it true (in some sensible model)? And if so, how to prove it? Something tells me it should be true and higher-order version of parametricity/theorems-for-free is needed to show this.
A concrete instance of the problem:
∀s. ∀a. (State s a ≅ (∀m. Monad m → StateT s m a))

In general the problem can be stated informally like so:
∀a. (MonadT Id a ≅ (∀ m. Monad m → MonadT m a))

where MonadT is a "schema" standing for arbitrary monad transformer.
The background type theory can be assumed to be system F or some dependent type theory consistent with parametricity. Depending on the theory used, the statement can be either internal or external.

**Tags:** type-theory, monad, parametricity

> **Comments:**
> **username_1**: This is a long shot, but could the methods used in [On Monadic Parametricity of Second-Order Functionals](http://dx.doi.org/10.1007/978-3-642-37075-5_15) be adapted?  
> **username_2**: @AndrejBauer This is very interesting, thank you!  

---

## 1 answers

### Answer by username_2 on 2023-09-06. Score: 3 | Accepted answer

The equation F Id ≅ ∀ (m: Monad). F m seems to be correct (for most transformers F, see below). However, I would not say that "a monad transformer is equivalent to its base monad". A monad transformer probably carries more information than its base monad, because there is no known way of mechanically converting a given base monad into its monad transformer.
By definition, a transformer's base monad can be obtained by applying the transformer to Id. This is denoted by F Id. You claim that F Id ≅ ∀ (m: Monad). F m. This seems to be correct.
Also you are correct that a proof will involve parametricity at the level of monads.
A possible proof could go like this. Consider the category of monads: objects are monads and arrows are monad morphisms. In that category, a monad transformer is an endofunctor. (This is true for almost all monad transformers, except Continuation and Codensity and some other variants of those monads. See https://stackoverflow.com/questions/63882053/whats-a-functor-on-the-category-of-monads?rq=3 and see also my answers in Explaining monad transformers in categorical terms and in https://stackoverflow.com/questions/24515876/is-there-a-monad-that-doesnt-have-a-corresponding-monad-transformer-except-io .)
Then we want to prove the following property:
 F Id ≅ ∀ (m: Monad). F m

where ∀ (m: Monad) goes over all monads.
The first step is to prove that the identity monad Id is an initial object in the category of monads. For any given monad M, there is only one monad morphism between Id and M (that morphism is given by the monad M's unit method, unit: ∀ a. Id a → M a).  I omit the proof of this property.
The second step is to use the Yoneda lemma (still in the category of monads). The Yoneda lemma says: For any Set-valued functor G (that is, a functor from the category of monads to the category of sets), the Yoneda lemma says:
 G X ≅ Nat(Hom(X, _), G)  ,

where Nat(K, L) is the set of natural transformations between functors K and L; Hom(X, _) is the Set-valued functor that maps a given monad M into the set of morphisms (in the category of monads) between the monads X and M.
Now we want to apply the Yoneda lemma to our situation where G = F is our monad transformer endofunctor. But then there is a technical difficulty: we cannot use the Yoneda lemma because G is not a set-valued functor (it's a monad-valued functor). We need to map monads into sets in some way. This is not straightforward; for instance, it is not clear how to choose a set that would correspond to the List monad or to the Maybe monad. It is easier to introduce a type parameter t and talk about the type List t or Maybe t. For any given type t there is a well-defined set of all values of type List t. So, we can temporarily choose some arbitrary type t and define a set-valued functor G that maps a monad m into the set of all values of type (F m) t. For this functor G, the Yoneda lemma shown above will hold.
The third step is to choose X = Id in the Yoneda lemma and find:
 G Id ≅ Nat(Hom(Id, _), G)

The fourth step is to see why it makes sense to write the right-hand side as ∀ (m: Monad). G m in the notation of a programming language. In fact, since we are working in a purely functional language where parametricity holds, any value of type ∀ (m: Monad). G m must be implemented in a way that is fully parametric in the monad m: it may use only the monad m's methods but no other knowledge about m.
The set Hom(Id, M) is a single-element set because Id is an initial object and there is only one monad morphism between Id and M. So, the functor Hom(Id, _) is a constant functor that maps any object into a single-element set.
What is the set of natural transformations between that constant functor and G? A component at m of such a transformation is a morphism of type Hom(Id, m) => G m. Here => means the arrow in the category Set.
But Hom(Id, m) is a single-element set. So, a morphism Hom(Id, m) => G m is the same as just choosing one element in the set G m.
We find that a natural transformation between Hom(Id, _) and G is the same as a choice, for each monad m, of an element in the set G m in a way that does not depend on the monad m other than through the monad m's methods (in other words, in a fully parametric way). An element in the set G m is the same as a value of type F m t. In a programming language, we would write that as the type ∀ (m: Monad). F m t assuming that values of that type must be fully parametric. The assumption of parametricity allows us to use the parametricity theorem and is necessary because otherwise the values of type ∀ (m: Monad). F m t would not correspond to natural transformations.
In this way we find, in a programming language notation, that:
 (F Id) t ≅ ∀ (m: Monad). F m t

This holds for all types t. So, we can rewrite this identity more concisely as:
 F Id ≅ ∀ (m: Monad). F m

There are certainly some rough edges in this sketch of a proof, but I'm not sufficiently well-versed in category theory to polish it off.
The analogy with the Yoneda lemma for ordinary types and endofunctors gives the following equivalence between types:
F 0 ≅ ∀ t. F t

because 0 is an initial object in the category of types.

> **Comments:**
> **username_1**: How do I get around the rought edge `F X ≅ ∀ m. (X → m) => F m`? The left-hand side is a set. How do I read the right-hand side as a set? I expected `F X ≅ Nat(Hom(X, _), F)` which sort of looks like what you wrote, but I am not sure.  
> **username_0**: I haven't heard about the category of monads. And I can't find a reference on the internet. Could you provide one?  
> **username_2**: @AndrejBauer You may be right about `F X ≅ Nat(Hom(X, _), F)` but I wish I had a more immediate grasp of the Yoneda lemma in a general category. In principle we just need to write the Yoneda lemma in the category of monads and put `F` into the right place and then set `X = Id`. Isn't `Nat(Hom(X, _), F)` a set?  
> **username_2**: @username_0 There isn't a reference that I have in mind. We just consider a category whose objects are various monads in the usual sense (Maybe, List, State s, Identity  etc.) and whose morphisms are monad morphisms.  
> **username_1**: @username_2: The basic question I have is, in what sense is `∀ m. (Id → m) => F m` a set? What does it mean to quantify with `∀` and get a set out?  
> **username_0**: @username_2 What is a monad morphism?  
> **username_2**: @AndrejBauer The notation `∀ m. (Id → m) => F m` is inspired by programming languages where we would write a type expression like that. The type `∀ a. K a → L a` is a type of natural transformations between endofunctors.  In category theory we will just say that there is a set of natural transformations between some functors and then, I guess, we should not write quantifiers any more. So, let's write the Yoneda lemma as `F X ≅ Nat(Hom(X, _), F)`. The right-hand side is a set of all natural transformations between set-valued functors `Hom(X, _)` and `F`. Let me try to edit my answer.  
> **username_2**: @username_0 A monad morphism `f: M → N` between two monads `M` and `N` is a natural transformation that satisfies suitable laws (in this case, the identity and the composition laws). https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html  The intuition is that `f` is a transformation that preserves the monad's methods.  
> **username_1**: I am not enough of a Haskell desciple to be able to take this amount of "fast & loose" reasoning, although it certainly points to how one would prove the claims rigorously.  
> **username_2**: @AndrejBauer  I have revised my answer and removed the quantifier in that place where you were objecting.  
> **username_1**: At this point I am confused abot something from the very beginning. If $F$ is an endofunctor, how can we use the Yoneda lemma on it? Or more preicsely, where does the `Nat(Hom(Id, _), F)` happen? The functor `F` is an endofunctor, whereas `Hom(Id, _)` maps to sets.  
> **username_2**: @AndrejBauer You are right. This is another helpful confusion coming from programming languages, where every type (including function types) is treated as a set. The endofunctor $F$ must be re-interpreted as a set-valued functor in order to apply Yoneda. Let me try to revise my answer again.  
> **username_1**: It might be better to go the other way an interpret `Hom(Id, _)` as an internal expoent, if such a thing exists.  
> **username_2**: @username_0 I have revised and expanded my answer, please let me know if you have questions.  
> **username_2**: @AndrejBauer If `Hom(X, Y)` were an internal exponent in the category of monads then we must be able to convert `Hom(X, Y)`, where `X` and `Y` are any given monads, into a new monad. I'm not sure it's possible because `Hom(X, Y)` is the set of all monad morphisms between monad `X` and `Y`. It's not clear in what way the set of all monad morphisms is equivalent to a new monad. For some `X` and `Y` there are no monad morphisms in `Hom(X, Y)`.  
> **username_0**: @username_2 I believe it's not enough to preserve just monad methods. You have to preserve `map` as well. Otherwise I can't prove that monads form a category.  
> **username_0**: Otherwise, I've been able to follow your explanation through. And formally show it for StateT, though with some proofs missing (require parametricity). Thanks a lot!  
> **username_2**: @username_0 Of course you need to preserve `map` but a monad morphism is by definition a *natural transformation* that preserves the monad methods. Preserving `map` is exactly the same as "being a natural transformation".  
> **username_0**: @username_2 Indeed. Thanks again!  

---

