¿Existe un morfismo de mónada sin identidad M ~> M que es monádicamente natural en M?

Se sabe que las transformaciones naturales con firma de tipo a -> adeben ser funciones de identidad. Esto se desprende del lema de Yoneda, pero también se puede derivar directamente. Esta pregunta pide la misma propiedad pero morfismos de mónada en lugar de transformaciones naturales.

Considere los morfismos de mónada M ~> Nentre mónadas. (Estas son transformaciones naturales M a -> N aque preservan las operaciones de mónada en ambos lados. Estas transformaciones son los morfismos en la categoría de mónadas). Podemos preguntarnos si existe un morfismo de mónada e :: (Monad m) => m a -> m aque funcione de la misma manera para cada mónada m. En otras palabras, un morfismo de mónada edebe ser monádicamente natural en el parámetro de tipo de mónada m.

La ley de naturalidad monádica dice que, para cualquier morfismo de mónada f: M a -> N a entre dos mónadas M y N, debemos tener f . e = e . fparámetros de tipo adecuados.

La pregunta es, ¿podemos demostrar que tal edebe ser una función de identidad, o hay un contraejemplo de un morfismo de mónada sin identidad edefinido como

  e :: (Monad m) => m a -> m a
  e ma = ...

Un intento fallido de definir tal ees:

 e ma = do
         _ <- ma
         x <- ma
         return x

Otro intento fallido es

 e ma = do
         x <- ma
         _ <- ma
         return x

Ambos intentos tienen la firma de tipo correcta pero fallan las leyes de morfismo de mónada.

Parece que el lema de Yoneda no se puede aplicar a este caso porque no hay morfismos de mónada Unit ~> Mdonde Unitestá la mónada de la unidad. Tampoco puedo encontrar ninguna prueba directamente.

Creo que ya has agotado todas las posibilidades interesantes. Cualquier Monad m => m a -> m afunción que podamos definir se verá inevitablemente así:

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

En particular, si k = return, e = id. Para eno serlo id, kdebe usarlo u de una manera no trivial (por ejemplo, k = const uy k = flip fmap u . constequivaldrá a sus dos intentos). Sin embargo, en tal caso, los uefectos se duplicarán, lo eque conducirá a no ser un morfismo de mónada para una serie de opciones de mónada m. Siendo así, el único morfismo de la mónada es totalmente polimórfico en la mónada id.

Hagamos el argumento más explícito.

En aras de la claridad, cambiaré a la join/ return/ fmappresentación por un momento. Queremos implementar:

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

¿Con qué podemos llenar el lado derecho? La elección más obvia es u. Por sí mismo, eso significa e = idque no parece interesante. Sin embargo, dado que también tenemos join, returny fmap, existe la opción de razonar inductivamente, con uel caso base. Digamos que tenemos algunos v :: m a, construidos utilizando los medios que tenemos a mano. Además de vsí mismo, tenemos las siguientes posibilidades:

1. join (return v), que es vy por lo tanto no nos dice nada nuevo;

2. join (fmap return v), que también lo es v; y

3. join (fmap (\x -> fmap (f x) w) v), para otro w :: m aconstruido de acuerdo con nuestras reglas, y algunos f :: a -> a -> a. (Agregar mcapas al tipo de f, como en a -> a -> m a, y joins extra para eliminarlas no llevaría a ninguna parte, ya que entonces tendríamos que mostrar la procedencia de esas capas, y las cosas finalmente se reducirían a los otros casos).

El único caso interesante es el # 3. En este punto, tomaré un atajo:

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

Cualquier ulado no derecho, por lo tanto, puede expresarse en la forma f <$> v <*> w, con vy wsiendo una uo más iteraciones de este patrón, llegando eventualmente a us en las hojas. Sin embargo, las expresiones de aplicación de este tipo tienen una forma canónica, obtenida mediante el uso de las leyes de aplicación para reasociar todos los usos de (<*>)la izquierda, que en este caso debe verse así ...

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

... con los puntos suspensivos representando cero o más ocurrencias adicionales de useparados por <*>, y cen a -> ... -> a -> afunción de la aridad apropiada. Como aes completamente polimórfico, cdebe, por paramétrica, ser una constfunción similar que elija uno de sus argumentos. Siendo así, cualquier expresión de este tipo puede reescribirse en términos de (<*)y (*>)...

u *> ... <* u

... con los puntos suspensivos representando cero o más ocurrencias adicionales de useparados por uno *>o por otro <*, no existiendo *>a la derecha de a <*.

Volviendo al inicio, todas las idimplementaciones no candidatas deben tener este aspecto:

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

También queremos eser un morfismo mónada. Como consecuencia, también debe ser un morfismo aplicativo. En particular:

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

Es decir:

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

Ahora tenemos un camino claro hacia un contraejemplo. Si usamos las leyes aplicables para convertir ambos lados a la forma canónica, (todavía) terminaremos con usy s intercaladas ven el lado izquierdo, y con todas las vs después de todas las us en el lado derecho. Eso significa que la propiedad no se mantendrá para mónadas como IO, Stateo Writer, independientemente de cuántos (*>)y (<*)hay e, o exactamente qué valores son elegidos por las constfunciones similares en ambos lados. Una demostración rápida:

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