haskell - significa - ¿Es la composición de una mónada arbitraria con una mónada transitable siempre una mónada?

mónada significado

Question

Si tengo dos mónadas m y n , y n es transitable, ¿tengo necesariamente una m made compuesta?

Más formalmente, esto es lo que tengo en mente:

import Control.Monad
import Data.Functor.Compose

prebind :: (Monad m, Monad n) =>
         m (n a) -> (a -> m (n b)) -> m (n (m (n b)))
mnx `prebind` f = do nx <- mnx
                     return $ do x <- nx
                                 return $ f x

instance (Monad m, Monad n, Traversable n) => Monad (Compose m n) where
  return = Compose . return . return
  Compose mnmnx >>= f = Compose $ do nmnx <- mnmnx `prebind` (getCompose . f)
                                     nnx  <- sequence nmnx
                                     return $ join nnx

Naturalmente, este tipo verifica, y creo que funciona en algunos casos que verifiqué (Reader over List, State over List) - como en, la ''mónada compuesta'' satisface las leyes de la mónada - pero no estoy seguro si esto Es una receta general para colocar en capas cualquier mónada sobre una transitable.

Answer 1

Algunos comentarios adicionales, para hacer más explícita la conexión entre la respuesta general de Reid Barton y su pregunta concreta.

En este caso, realmente vale la pena trabajar su instancia de Monad en términos de join :

join'' ::  m (n (m (n b))) -> m (n b)
join'' = fmap join . join . fmap sequence

Al reintroducir compose / getCompose en los lugares apropiados y usar m >>= f = join (fmap fm) , puede verificar que esto sea realmente equivalente a su definición (tenga en cuenta que su prebind equivale al fmap f en esa ecuación).

Esta definición hace que sea cómodo verificar las leyes con los diagramas ¹ . Aquí hay uno para join . return = id join . return = id es decir (fmap join . join . fmap sequence) . (return . return) = id (fmap join . join . fmap sequence) . (return . return) = id :

3210 MT id MT id MT id MT ----> ----> ----> rT2 | | rT1 | | rT1 | | id rM3 V V rM3 V V V V ----> ----> ----> MTMT sM2 MMTT jM2 MTT jT0 MT

El rectángulo total es la ley de la mónada:

M id M ----> rM1 | | id V V ----> MM jM0 M

Al ignorar las partes que son necesariamente iguales en ambos sentidos a través de los cuadrados, vemos que los dos cuadrados de la derecha corresponden a la misma ley. (Por supuesto, es un poco tonto llamar a estos "cuadrados" y "rectángulos", dado todos los lados de id que tienen, pero se ajusta mejor a mis limitadas habilidades artísticas ASCII). Sin embargo, el primer cuadrado equivale a una sequence . return = fmap return sequence . return = fmap return , que es el diagrama inferior derecho de la página de Wikipedia que Reid Barton menciona ...

M id M ----> rT1 | | rT0 V V ----> TM sM1 MT

... y no es un hecho que eso se sostiene, como lo demuestra la respuesta de Reid Barton.

Si aplicamos la misma estrategia a la join . fmap return = id join . fmap return = id law, el diagrama superior derecho, sequence . fmap return = return sequence . fmap return = return , aparece: eso, sin embargo, no es un problema en sí mismo, ya que eso es solo (una consecuencia inmediata de) la ley de identidad de Traversable . Finalmente, haciendo lo mismo con la join . fmap join = join . join join . fmap join = join . join join . fmap join = join . join ley de join . fmap join = join . join hace los otros dos diagramas - sequence . fmap join = join . fmap sequence . sequence sequence . fmap join = join . fmap sequence . sequence sequence . fmap join = join . fmap sequence . sequence y sequence . join = fmap join . sequence . fmap sequence sequence . join = fmap join . sequence . fmap sequence sequence . join = fmap join . sequence . fmap sequence - saltar adelante.

Notas al pie:

1. Leyenda para la taquigrafía: r es return , s es sequence y j es join . Las letras mayúsculas y los números después de las abreviaturas de la función desambiguan la mónada involucrada y la posición de su capa introducida o modificada termina en - en el caso de s , que se refiere a lo que inicialmente es la capa interna, como en este caso sabemos que La capa exterior es siempre una T Las capas están numeradas de abajo hacia arriba, comenzando desde cero. La composición se indica escribiendo la abreviatura de la segunda función debajo de la primera.

Answer 2

No, no siempre es una mónada. Necesita condiciones de compatibilidad adicionales relacionadas con las operaciones de la mónada de las dos mónadas y la sequence :: n (ma) -> m (na) ley distributiva sequence :: n (ma) -> m (na) , como se describe, por ejemplo, en Wikipedia .

Su pregunta anterior da un ejemplo en el que no se cumplen las condiciones de compatibilidad, a saber:

S = m = [] , con la unidad X -> SX enviando x a [x];

T = n = (->) Bool , o equivalentemente TX = X × X, con la unidad X -> TX enviando x a (x, x).

El diagrama de abajo a la derecha en la página de Wikipedia no conmuta, ya que la composición S -> TS -> ST envía xs :: [a] a (xs,xs) y luego al producto cartesiano de todos los pares extraídos de xs ; mientras que el mapa de la derecha S -> ST envía xs a la "diagonal" que consiste en solo los pares (x,x) para x en xs . Es el mismo problema que hizo que su mónada propuesta no cumpliera con una de las leyes de la unidad.