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.

duplode duplode · Accepted Answer · 2020-04-26T20:42:05

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:

join (return v), which is v and therefore doesn't tell us anything new;
join (fmap return v), which is v as well; and
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

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

1 Answers