Is there a non-identity monad morphism M ~> M that is monadically natural in M?

Question

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.

Crumble

Answer 1

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.

Step 1: Use the theorem of Jaskelioff-O'Connor

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.

Step 2: A canonical form of ∀(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 + ...

Step 3: translating into terms of type ∀(M : Monad). M b → M b

For 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.

Step 4: Imposing the laws of monad morphisms

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.

Crumble

I'm also unsure about that "... ≅ 1" you are not certain with. What about λp. p (λ_. p id) ? – Jaal

Yes, and actually there are lots of other terms: λp. p x where x : r → r is defined by x = λy. p(λ_. y). We can also compose x with itself, apply x to the final result, etc. -- There is another potential problem with this method of proof: Suppose we find that ∀(r: Type). ((r → r) → r) → r is not Unit but some other type T. It will follow that ∀(b: Type). ∀(M: Monad). M b → M b = T. But we are asking about the type of monad morphisms, not just any natural transformations. So, we would not have proved that the result is T, only that it is smaller than T. – Crumble

I tried to prove the equivalence via parametricity but got stuck. cstheory.stackexchange.com/questions/53855/… – Crumble

@Jaal I was mistaken. The correct equivalence is most likely ∀(r: Type). ((r → r) → r) → r ≅ 1 + 2 + 3 + ... , see my answer to this question cstheory.stackexchange.com/questions/53855/… Various values of that type are described by pairs of integers (m, n) and most likely correspond directly to the kind of code shown in my question: do _ <- ma; ...; x <- ma ; ... _ <- ma; return x, where there are m total lines and the n-th line has "x <- ma". I'll have to revise my answer. – Crumble

@Jaal I revised my answer. I think it's close to being a proof now. – Crumble

@Imperception I have added a new answer with a hopefully more rigorous attempt at a proof. – Crumble

@Imperception The proof is now complete. Took me just 4 years. – Crumble

Answer 2

I think you have already exhausted all interesting possibilities. Any Monad m => m a -> m a function we might define will inescapably look like this:

e :: forall m a. Monad m => m a -> m a
e u = u >>= k
    where
    k :: a -> m a
    k = _

In particular, if k = return, e = id. For e not to be id, k must use u in a nontrivial way (for instance, k = const u and k = flip fmap u . const amount to your two attempts). In such a case, though, the u effects will be duplicated, leading e to fail to be a monad morphism for a number of choices of monad m. That being so, the only monad morphism fully polymorphic in the monad is id.

---

Let's make the argument more explicit.

For the sake of clarity, I will switch to the join/return/fmap presentation for a moment. We want to implement:

e :: forall m a. Monad m => m a -> m a
e u = _

What can we fill the right hand side with? The most obvious pick is u. By itself, that means e = id, which doesn't look interesting. However, since we also have join, return and fmap, there is the option of reasoning inductively, with u as the base case. Say we have some v :: m a, built using the means we have at hand. Besides v itself, we have the following possibilities:

1. join (return v), which is v and therefore doesn't tell us anything new;

2. join (fmap return v), which is v as well; and

3. join (fmap (\x -> fmap (f x) w) v), for some other w :: m a built according to our rules, and some f :: a -> a -> a. (Adding m layers to the type of f, as in a -> a -> m a, and extra joins to remove them wouldn't lead anywhere, as we would then have to show the provenance of those layers, and things would ultimately reduce to the other cases.)

The only interesting case is #3. At this point, I will take a shortcut:

join (fmap (\x -> fmap (f x) w) v)
    = v >>= \x -> fmap (f x) w
    = f <$> v <*> w

Any non-u right hand side, therefore, can be expressed in the form f <$> v <*> w, with v and w being either u or further iterations of this pattern, eventually reaching us at the leaves. Applicative expressions of this sort, however, have a canonical form, obtained by using the applicative laws to reassociate all uses of (<*>) to the left, which in this case must look like this...

c <$> u <*> ... <*> u

... with the ellipsis standing for zero or more further occurrences of u separated by <*>, and c being an a -> ... -> a -> a function of appropriate arity. Since ais fully polymorphic, c must, by parametricity, be some const-like function which picks one of its arguments. That being so, any such expression can be rewritten in terms of (<*) and (*>)...

u *> ... <* u

... with the ellipsis standing for zero or more further occurrences of u separated by either *> or <*, there being no *> to the right of a <*.

Going back to the start, all non-id candidate implementations must look like this:

e u = u *> ... <* u

We also want e to be a monad morphism. As a consequence, it must also be an applicative morphism. In particular:

-- (*>) = (>>) = \u v -> u >>= \_ -> v
e (u *> v) = e u *> e v

That is:

(u *> v) *> ... <* (u >* v) = (u *> ... <* u) *> (v *> ... <* v)

We now have a clear path towards a counterexample. If we use the applicative laws to convert both sides to the canonical form, we will (still) end up with interleaved us and vs on the left hand side, and with all vs after all us on the right hand side. That means the property won't hold for monads like IO, State or Writer, regardless of how many (*>) and (<*) there are in e, or exactly which values are picked by the const-like functions on either side. A quick demo:

GHCi> e u = u *> u <* u  -- Canonical form: const const <$> u <*> u <*> u
GHCi> e (print 1 *> print 2)
1
2
1
2
1
2
GHCi> e (print 1) *> e (print 2)
1
1
1
2
2
2

Imperception

I can't find a rigorous enough proof. How can we prove that the effects of u will be necessarily duplicated unless e = id? (We could also write e u = do _ <- u; _ <- u; _ <- u; u and combine further u-effects.) How can we describe mathematically that "a monadic value p :: m a has multiple effects copied from u :: m a? And then, how can we prove that duplicated (triplicated, etc.) u-effects necessarily lead to violations of monad morphism laws? – Crumble

@Crumble I have written down my argument more explicitly. The one thinko I had certainly committed in the original revision of the answer was mentioning idempotency, given that the failures I have observed have more to do with commutativity of effects. – Imperception

This is interesting. I will have to think some more about it. How can we prove that there is only one way of implementing a nontrivial e u, namely using some expression of the form u *> ... <* u as you described? Why can't we find some other clever and complicated combination of fmap, return, and join, so that we get something else? It is also a good move to consider applicative morphisms. It might be easier to prove the analogous property for applicative morphisms than for monad morphisms. (The only applicative morphisms that are applicatively natural are identity morphisms?) – Crumble

@Crumble (1) While it'd be nice to have a more crystalline presentation (I'm still thinking about it), I believe my three cases are exhaustive. Only join _ can lead to a non-id result, and #3 is the only way that won't lead to id or infinite regress. (2) On Applicative: informally, if your only Kleisli arrow is return, you aren't using the extra power Monad brings, so you might as well work with Applicative. (3) Yup, the analogous property holds for applicative morphisms. The part of my argument starting with the canonical form, which is self-contained, should suffice as proof. – Imperception

If we had a monad morphism that is monadically natural, we would have also an applicative morphism that is applicatively natural. I think it might be easier to prove that there is no such applicative morphism. – Crumble

I have added my answer below where I use a theorem by Jaskelioff and O'Connor. This looks like a more solid argument to me, except for some details that I haven't got time to work out. – Crumble