It is known that natural transformations with type signature a -> a must be identity functions. This follows from the Yoneda lemma but can be also derived directly. This question asks for the same property but for monad morphisms instead of natural transformations.
Consider monad morphisms M ~> N between monads. (These are natural transformations M a -> N a that preserve the monad operations on both sides. These transformations are the morphisms in the category of monads.) We can ask whether there exists a monad morphism e :: (Monad m) => m a -> m a that works in the same way for every monad m. In other words, a monad morphism e must be monadically natural in the monad type parameter m.
The monadic naturality law says that, for any monad morphism f: M a -> N a between any two monads M and N, we must have f . e = e . f with suitable type parameters.
The question is, can we prove that any such e must be an identity function, or is there a counter-example of a non-identity monad morphism e defined as
e :: (Monad m) => m a -> m a
e ma = ...
One failed attempt to define such e is:
e ma = do
_ <- ma
x <- ma
return x
Another failed attempt is
e ma = do
x <- ma
_ <- ma
return x
Both these attempts have the correct type signature but fail the monad morphism laws.
It seems that the Yoneda lemma cannot be applied to this case because there are no monad morphisms Unit ~> M where Unit is the unit monad. I also can't find any proof directly.
Here is a proof that uses a theorem by Jaskelioff and O'Connor in the paper https://arxiv.org/pdf/1402.1699.pdf where they prove the following identity:
(after Equation 6.1 in section 6)
∀(M: Monad). (a → M b) → M c ≅ µ r. c + a × (b → r)
However, note that the arrows here (such as a → M b) denote ordinary morphisms but not necessarily monad morphisms. We will still need to impose the monad morphisms laws at the end.
We use the identity above with a = 1, b = c and get:
∀(M: Monad). M b → M b ≅ µ r. b + (b → r)
We are interested in the following type:
∀(b: Type). ∀(M: Monad). M b → M b
So, we impose the quantifier ∀(b: Type) and get:
∀(b: Type). ∀(M: Monad). M b → M b ≅ ∀(b: Type). µ r. b + (b → r)
Now it remains to simplify the last type.
∀(b: Type). µ r. b + (b → r)Deriving this is a longer story, and it is written up in another question: https://cstheory.stackexchange.com/questions/53855 starting around "Step 3".
The result is the type equivalence:
∀(b: Type). µ r. b + (b → r) ≅ 1 + 2 + 3 + ...
Values of the type on the right-hand side are pairs of integers (n, k) where n >= k >= 1. Given a pair (n, k), we write a term t_n_k of type ∀(b : Type). µ r. b + (b → r) as:
t_n_k = λ(b : Type) → Right( λ(x_1 : b) → Right( λ(x_2 : b) → ... Right( λ(x_n : b) → Left x_k)...)
Here x_k is one of the bound variables x_1, ..., x_n introduced in the term.
So, we get:
∀(b: Type). ∀(M: Monad). M b → M b ≅ 1 + 2 + 3 + ...
∀(M : Monad). M b → M bFor each term t_n_k, it turns out that the corresponding term e_n_k of type M b → M b is written as:
e_n_k : Monad m => m b -> m b
e_n_k mb = do
_ <- mb -- line 1
... -- ...
_ <- mb -- line k - 1
x <- mb -- line k
_ <- mb -- line k + 1
... -- ...
_ <- mb -- line n
return x
There are n lines that run the effects of mb, and we are using the value x from the k-th line in the final result.
Each pair of integers (n, k) where n >= k >= 1 corresponds to a unique function of this form, so let us denote those functions by e_n_k.
To derive this explicit form of e_n_k, we need to follow the steps in the proof of the Jaskelioff-O'Connor theorem.
Select an arbitrary (n, k) and write the term t_n_k of type µ r. b + (b → r) as shown above:
t_n_k = λ(b : Type) → Right( λ(x_1 : b) → Right( λ(x_2 : b) → ... Right( λ(x_n : b) → Left x_k)...)
Our goal is to derive the corresponding function e_n_k of type m b → m b.
First, we need to express the type µ r. b + (b → r) via the free monad on an endofunctor G defined by G x = b → x.
The free monad on any covariant endofunctor C is defined (recursively) by:
FreeMonad C x = Either x (C (FreeMonad C x))
So, the free monad on G is:
FreeMonad G x = Either x (b → FreeMonad G x)
or equivalently:
FreeMonad G x = µ r. x + (b → r)
So, the type µ r. b + (b → r) is rewritten as FreeMonad G b. The term t_n_k is already of that type.
Next, we need to use the Yoneda lemma in the category of monads:
If K is any fixed monad, then the following types are equivalent:
K b ≅ ∀(M : Monad). ( ∀(x : Type). K x → M x ) → M b
Here the argument of type K x → M x is assumed to be a monad morphism.
We use this lemma with K x = FreeMonad G x and obtain:
FreeMonad G b ≅ ∀(m : Monad). (∀(x : Type). FreeMonad G x → m x) → m b
Here, functions of type FreeMonad G x → m x are required to be monad morphisms.
So, we rewrite our term t_n_k : FreeMonad G b into a function of the above type. Call that function t2:
t2 : ∀(m : Monad). (∀(x : Type). FreeMonad G x → m x) → m b
t2 = \h -> h t_n_k
(Here the polymorphic function h : ∀(x : Type). FreeMonad G x → m x has to be used with the type parameter x = b.)
The free monad on G has the property that for any monad M, the set of all natural transformations G -> M is the same as the set of all monad morphisms FreeMonad G -> M. Given a natural transformation m1 : G a → m a, the corresponding monad morphism m2 : FreeMonad G -> m is defined by:
m2 :: FreeMonad G a -> m a
m2 (Left x) = return x
m2 (Right gfrm) = bind (m1 gfrm) m2
Here, return and bind are m's monadic methods.
The equivalence transformation from m1 to m2 can be written as a function p:
p :: ∀(m : Monad). (∀(x : Type). G x → m x) → FreeMonad G y -> m y
p gxmx (Left x) = return x
p gxmx (Right gfrm) = bind (gxmx gfrm) (p gxmx)
The equivalence transformation p can be simplified even further by using the Yoneda lemma for types:
m b ≅ ∀(r : Type). (b → r) → m r
With this, we replace gxmx equivalently by a value m2 of type m b:
mb :: m b
mb = gxmx id
gxmx :: (b → x) → m x
gxmx s = fmap s mb
The transformation p is then replaced by an equivalent, simpler transformation q:
q :: ∀(m : Monad). m b → FreeMonad G y -> m y
q mb (Left x) = return x
q mb (Right gfrm) = bind (fmap gfrm mb) (q mb)
We can simplify further if we use the naturality law of bind:
bind (fmap f p) g = bind p (g . f)
Then we get the following code for q:
q :: ∀(m : Monad). m b → FreeMonad G y -> m y
q mb (Left x) = return x
q mb (Right gfrm) = bind mb (q mb . gfrm)
Using the function q (which is an isomorphism), we can transform the function t2 to take isomorphic arguments of a simpler type m b. The result is a function t3:
t3 :: Monad m => m b → m b
t3 = t2 . q
The function t3 is the required function of type m b → m b that we are looking for.
It remains to transform the code of t2 into a code for t3:
t3 mb = t2 (q mb) = q mb t_n_k
The function t_n_k is given by the expression shown above, which we will specialize for the fixed type b. (It is fixed only within this calculation; later we will impose a quantifier on b).
t_n_k = Right( λ(x_1 : b) → Right( λ(x_2 : b) → ... Right( λ(x_n : b) → Left x_k)...)
The recursive function q mb performs pattern-matching on t_n_k recursively, according to the code for q shown above. The evaluation will recursively peel off the layers of Right( λ(x_2 : b) → ... until at some point a Left() is found. At that point, the recursion will stop.
Let us trace some levels of that recursion. We will denote the sub-expressions of t_n_k by s_0, s_1, s_2, etc., like this:
s_0 = t_n_k = Right( λ(x_1 : b) → s1 )
s_1 = Right( λ(x_2 : b) → s2 )
...
s_{k-1} = Right( λ(x_k : b) → s_k )
...
s_{n-1} = Right( λ(x_n : b) → s_n )
s_n = Left x_k
Note that the term s_i is a function of the bound variables x_1, x_2, ..., x_i introduced earlier. In other words, the variables x_1, x_2, ..., x_i occur freely in the term s_i.
Then we evaluate t3 mb as:
t3 mb = q mb t_n_k = q mb s0
= q mb (Right( λ(x_1 : b) → s1)) -- Expand `q mb Right()`.
= bind mb ( q mb . (λ(x_1 : b) → s1) )
= bind mb (\x_1 -> q mb s1)
We can rewrite this code using the "do notation" instead of explicit bind:
t3 mb = do
x_1 <- mb
q mb s1
Expand q mb s1 further and get:
q mb s1 = do
x_2 <- mb
q mb s3
So:
t3 mb = do
x_1 <- mb
do
x_2 <- mb
q mb s3
By the associativity law of the monad m, we can flatten the layers of do and simplify the code:
t3 mb = do
x_1 <- mb
x_2 <- mb
q mb s3
Continuing in this way to expand q mb s_i and using induction in i, we obtain:
t3 mb = do
x_1 <- mb
x_2 <- mb
...
x_n <- mb
q mb s_n
Because s_n = Left x_k, we get q mb s_n = return x_k, and so:
t3 mb = do
x_1 <- mb
x_2 <- mb
...
x_n <- mb
return x_k
This is exactly equivalent to the code of e_n_k shown before.
We have found that all purely parametric functions of type ∀(b: Type). ∀(M: Monad). M b → M b are of the form e_n_k for some (n, k).
e_n_k : Monad m => m b -> m b
e_n_k mb = do
_ <- mb -- line 1
... -- ...
_ <- mb -- line k - 1
x <- mb -- line k
_ <- mb -- line k + 1
... -- ...
_ <- mb -- line n
return x
It remains to impose the monad morphism laws on e_n_k. Then we will find that only e_1_1 (which is an identity function) is a monad morphism while all other e_n_k are not monad morphisms.
To show that in detail, consider the standard State monad. We will use an integer internal state to keep track of how many mb lines we have in e_n_k. The Monad instance is defined by standard code that I omit here:
type StateInt a = Int -> (a, Int)
instance Monad StateInt where ...
Now we will show that the function e_n_k violates the monad morphism composition law unless n = k = 1.
The monad morphism composition law for e_n_k says that, for any value q : StateInt (StateInt a), the result of applying e_n_k separately to both layers of StateInt should be the same as the result of flattening q first and then applying StateInt.
e_n_k (join q) =?= join (e_n_k (fmap e_n_k q))
For the counterexample, we will use a carefully chosen value q : StateInt (StateInt a) with the type parameter a = Unit. The value q is defined by:
q :: StateInt (StateInt Unit)
q = \s -> (\t -> ((), s + 1), s)
Now we calculate both sides of the composition law for the given q step by step.
The left-hand side is calculated as:
join q = \s -> ((), s + 1)
e_n_k (join q) = \s -> ((), s + n)
Note that e_n_k repeats the state update n times.
The right-hand side is calculated as:
fmap e_n_k q = \s -> (\t -> ((), s + 1), s)
e_n_k (fmap e_n_k q) = \s -> (\t -> ((), s + 1), s)
join (e_n_k (fmap e_n_k q)) = \s -> ((), s + 1)
The two sides of the composition law are \s -> ((), s + n) and \s -> ((), s + 1). These functions are equal only if n = 1. Because 1 <= k <= n, we also must have k = 1.
So, the composition law holds only for e_1_1 (which is an identity function) but not for any other e_k_n.
This concludes the proof that there is only one natural monad morphism of type ∀(b: Type). ∀(M: Monad). M b → M b. Equivalently, there is only one natural transformation between identity functors in the category of monads.