mónada monadologia monadas leibniz las filosofía filosofia educatina doctrina haskell monads monad-transformers category-theory

haskell - monadologia - monadas filosofia



¿Por qué los transformadores de mónada son diferentes a apilar las mónadas? (2)

En muchos casos, no me queda claro qué se puede ganar al combinar dos mónadas con un transformador en lugar de usar dos mónadas separadas. Obviamente, usar dos mónadas separadas es una molestia y puede implicar hacer una notación interna, pero ¿hay casos en los que simplemente no sea lo suficientemente expresivo?

Un caso parece ser StateT en la lista: la combinación de mónadas no le da el tipo correcto, y si obtiene el tipo correcto a través de una pila de mónadas como Bar (donde Bar a = (Reader r (List (Writer w (Identity a))), no hace lo correcto.

Pero me gustaría una comprensión más general y técnica de qué es exactamente lo que los transformadores de la mónada traen a la mesa, cuándo son necesarios y por qué.

Para hacer esta pregunta un poco más enfocada:

  1. ¿Cuál es un ejemplo real de una mónada sin un transformador correspondiente (esto ayudaría a ilustrar lo que pueden hacer los transformadores que no puede apilar solo las mónadas)?
  2. Son StateT y ContT los únicos transformadores que dan un tipo que no es equivalente a la composición de ellos con m, para una mónada subyacente m (independientemente del orden en que se componen).

(No me interesan los detalles particulares de la implementación con respecto a las diferentes opciones de bibliotecas, sino la pregunta general (y probablemente independiente de Haskell) de qué mórada transformadores / morfismos están agregando como alternativa a la combinación de efectos al apilar un montón de constructores de tipo monádico .)

(Para dar un poco de contexto, soy un lingüista que está haciendo un proyecto para enriquecer la gramática de Montague, simplemente tecleé el cálculo lambda para componer los significados de las palabras en oraciones, con una pila de transformadores de mónada. Sería realmente útil saber si los transformadores funcionan realmente algo útil para mi)

Gracias,

Reuben


¿Cuál es un ejemplo real de una mónada sin un transformador correspondiente (esto ayudaría a ilustrar lo que pueden hacer los transformadores que no puede apilar solo las mónadas)?

IO y ST son los ejemplos canónicos aquí.

Son StateT y ContT los únicos transformadores que dan un tipo que no es equivalente a la composición de ellos con m, para una mónada subyacente m (independientemente del orden en que se componen).

No, ListT ma no es (isomorfo a) [ma] :

newtype ListT m a = ListT { unListT :: m (Maybe (a, ListT m a)) }


Para responder a su pregunta sobre la diferencia entre Writer w (Maybe a) vs MaybeT (Writer w) a , comencemos por echar un vistazo a las definiciones:

newtype WriterT w m a = WriterT { runWriterT :: m (a, w) } type Writer w = WriterT w Identity newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }

Usando ~~ para significar "estructuralmente similar a" tenemos:

Writer w (Maybe a) == WriterT w Identity (Maybe a) ~~ Identity (Maybe a, w) ~~ (Maybe a, w) MaybeT (Writer w) a ~~ (Writer w) (Maybe a) == Writer w (Maybe a) ... same derivation as above ... ~~ (Maybe a, w)

Así que, en cierto sentido, usted tiene razón: estructuralmente tanto el Writer w (Maybe a) como MaybeT (Writer w) a son los mismos, ambos son esencialmente un par de un valor Maybe y una w .

La diferencia es cómo los tratamos como valores monádicos. Las funciones return y >>= class hacen cosas muy diferentes según la mónada de la que forman parte.

Consideremos el par (Just 3, []::[String]) . Usando la asociación que hemos derivado anteriormente, aquí está cómo se expresaría ese par en ambas mónadas:

three_W :: Writer String (Maybe Int) three_W = return (Just 3) three_M :: MaybeT (Writer String) Int three_M = return 3

Y aquí es cómo construiríamos una pareja (Nothing, []) :

nutin_W :: Writer String (Maybe Int) nutin_W = return Nothing nutin_M :: MaybeT (Writer String) Int nutin_M = MaybeT (return Nothing) -- could also use mzero

Ahora considera esta función en pares:

add1 :: (Maybe Int, String) -> (Maybe Int, String) add1 (Nothing, w) = (Nothing w) add1 (Just x, w) = (Just (x+1), w)

y veamos cómo lo implementaríamos en las dos mónadas diferentes:

add1_W :: Writer String (Maybe Int) -> Writer String (Maybe Int) add1_W e = do x <- e case x of Nothing -> return Nothing Just y -> return (Just (y+1)) add1_M :: MaybeT (Writer String) Int -> MaybeT (Writer String) Int add1_M e = do x <- e; return (e+1) -- also could use: fmap (+1) e

En general, verá que el código en la mónada MaybeT es más conciso.

Además, semánticamente las dos mónadas son muy diferentes ...

MaybeT (Writer w) a es una acción de Writer que puede fallar, y la falla se maneja automáticamente por usted. Writer w (Maybe a) es solo una acción de Writer que devuelve un Maybe. No pasa nada especial si ese valor Tal vez resulta ser Nada. Esto se ejemplifica en la función add1_W donde tuvimos que realizar un análisis de caso en x .

Otra razón para preferir el enfoque MaybeT es que podemos escribir código que es genérico sobre cualquier pila de mónadas. Por ejemplo, la función:

square x = do tell ("computing the square of " ++ show x) return (x*x)

se puede usar sin cambios en cualquier pila de mónadas que tenga una cadena de escritura, por ejemplo:

WriterT String IO ReaderT (WriterT String Maybe) MaybeT (Writer String) StateT (WriterT String (ReaderT Char IO)) ...

Pero el valor de retorno de square no escribe check contra la Writer String (Maybe Int) porque square no devuelve un Maybe .

Cuando usted codifica en Writer String (Maybe Int) , el código revela explícitamente la estructura de la mónada haciéndola menos genérica. Esta definición de add1_W :

add1_W e = do x <- e return $ do y <- x return $ y + 1

solo funciona en una pila de mónadas de dos capas, mientras que una función como square funciona en una configuración mucho más general.