haskell - monadologia - monadas filosofia

Explicación de las leyes de la mónada.

Question

De una suave introducción a Haskell , existen las siguientes leyes de mónadas. ¿Alguien puede explicar intuitivamente lo que significan?

return a >>= k             = k a
m >>= return               = m
xs >>= return . f          = fmap f xs
m >>= (/x -> k x >>= h)    = (m >>= k) >>= h

Aquí está mi intento de explicación:

1. Esperamos que la función de retorno se ajuste de modo que su naturaleza monádica sea trivial. Cuando lo vinculamos a una función, no hay efectos monádicos, solo se debe pasar a la función.

2. La salida desenvuelta de m se pasa para return y la return envolver. La naturaleza monádica sigue siendo la misma. Así que es lo mismo que la mónada original.

3. El valor sin envolver se pasa a f luego se vuelve a envolver. La naturaleza monádica sigue siendo la misma. Este es el comportamiento esperado cuando transformamos una función normal en una función monádica.

4. No tengo una explicación para esta ley. Esto sí dice que la mónada debe ser "casi asociativa".

Answer 1

En términos de notación do , la regla 4 significa que podemos agregar un bloque do adicional para agrupar una secuencia de operaciones monádicas.

    do                          do
                                  y <- do
      x <- m                             x <- m
      y <- k x          <=>              k x
      h y                         h y

Esto permite que las funciones que devuelven un valor monádico funcionen correctamente.

Answer 2

Las primeras tres leyes dicen que "devolver" solo envuelve un valor y no hace nada más. Así que puedes eliminar las llamadas "devueltas" sin cambiar la semántica.

La última ley es la asociatividad para vincular. Significa que tomas algo como:

do
   x <- foo
   bar x
   z <- baz

y convertirlo en

do
   do
      x <- foo
      bar x
   z <- baz

Sin cambiar el significado. Por supuesto, no harías exactamente esto, pero podrías poner la cláusula interna "do" en una declaración "if" y desear que signifique lo mismo cuando "if" sea verdadero.

A veces, las mónadas no siguen exactamente estas leyes, especialmente cuando se produce algún tipo de valor de fondo. Eso está bien siempre y cuando esté documentado y sea "moralmente correcto" (es decir, se siguen las leyes para los valores no inferiores, o los resultados se consideran equivalentes de alguna otra manera).

Answer 3

No hay desacuerdos con las otras respuestas, pero podría ayudar pensar que las leyes de la mónada realmente describen dos conjuntos de propiedades. Como dice John, la tercera ley que mencionas es ligeramente diferente, pero así es como los otros pueden dividirse:

Las funciones que enlaza con una mónada se componen igual que las funciones normales.

Como en la respuesta de John, lo que se llama una flecha de Kleisli para una mónada es una función con tipo a -> mb . Piense en el return como id y (<=<) como (.) , Y las leyes de la mónada son las traducciones de estos:

1. id . f id . f es equivalente a f
2. f . id f . id es equivalente a f
3. (f . g) . h (f . g) . h es equivalente a f . (g . h) f . (g . h)

Secuencias de efectos monádicos se anexan como listas.

En su mayor parte, puede pensar en la estructura monádica extra como una secuencia de comportamientos adicionales asociados con un valor monádico; por ejemplo, Maybe ser "renunciar" por Nothing y "seguir adelante" por Just . La combinación de dos acciones monádicas concatena esencialmente las secuencias de comportamientos que sostuvieron.

En este sentido, el return es nuevamente una identidad (la acción nula, similar a una lista vacía de comportamientos) y (>=>) es concatenación. Entonces, las leyes de la mónada son traducciones de estas:

1. [] ++ xs es equivalente a xs
2. xs ++ [] es equivalente a xs
3. (xs ++ ys) ++ zs es equivalente a xs ++ (ys ++ zs)

Estas tres leyes describen un patrón ridículamente común, que desafortunadamente Haskell no puede expresar con toda su generalidad. Si está interesado, Control.Category proporciona una generalización de "cosas que parecen una composición de función", mientras que Data.Monoid generaliza el último caso en el que no intervienen parámetros de tipo.

Answer 4

Tus descripciones parecen bastante buenas. En general, la gente habla de tres leyes de la mónada, que tienes como 1, 2 y 4. Tu tercera ley es ligeramente diferente, y lo veré más adelante.

Para las tres leyes de la mónada, me parece mucho más fácil obtener una comprensión intuitiva de lo que significan cuando se reescriben utilizando la composición de Kleisli:

-- defined in Control.Monad
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
mf >=> n = /x -> mf x >>= n

Ahora las leyes se pueden escribir como:

1) return >=> mf = mf                  -- left identity
2) mf >=> return = mf                  -- right identity
4) (f >=> g) >=> h = f >=> (g >=> h)   -- associativity

1) Ley de identidad de la izquierda: devolver un valor no cambia el valor y no hace nada en la mónada.

2) Ley de identidad correcta: devolver un valor no cambia el valor y no hace nada en la mónada.

4) Asociatividad: la composición monádica es asociativa (me gusta la respuesta de KennyTM para esto)

Las dos leyes de identidad básicamente dicen lo mismo, pero ambas son necesarias porque el return debe tener un comportamiento de identidad en ambos lados del operador de enlace.

Ahora para la tercera ley. Esta ley esencialmente dice que tanto la instancia de Functor como la de tu mónada se comportan de la misma manera al elevar una función a la mónada, y que ninguna de las dos cosas es monádica. Si no me equivoco, es el caso de que cuando una mónada obedece a las otras tres leyes y la instancia de Functor obedece a las leyes de functor, esta afirmación siempre será cierta.

Mucho de esto viene de la Wiki de Haskell . La Typeclassopedia es también una buena referencia.

Answer 5

Una mónada se usa esencialmente para permitir el acceso a un valor global y al mismo tiempo para ocultar el valor global de la lista de parámetros de la función.

La idea es, una llamada a la función, para simular un global, recibe sus argumentos reales y también el global y devuelve el valor y el nuevo global. La mónada se utiliza para hacer esto de una manera elegante al ocultar el valor global.

Para una mónada de tipo Mx , cada operación monádica es un cierre que encierra un valor de tipo x . La operación monádica dice "pass me the global value and I provide you the result consisting of the new value of the global and in the same time the value you need to compute" : esta declaración es la misma para cualquier mónada, incluida la continuación. monada.

Hay 2 operadores que son suficientes para realizar cualquier cálculo como una mónada y ambos siguen la lógica de esta declaración.

El operador de return simplemente empaca el valor que debe calcularse en el entorno de un cierre que no realiza ningún cálculo. Este cierre espera el valor global y proporciona la respuesta.

El operador de bind también está esperando un valor global, pero antes realiza algún cálculo para proporcionar la respuesta. Desempaqueta el valor encerrado en la mónada (desempaqueta el valor encerrado por el cierre que representa la mónada), realiza algunos cálculos en 2 continuaciones que se pasan una vez que el valor global y otra que pasa el valor calculado por la primera continuación y devuelve un nuevo cierre que encierra el valor calculado como un valor monádico.

Ahora, para responder a su pregunta, desde el punto de vista que se acaba de describir, la composición de la ley de unidades dice que al operador de return nunca se le permite cambiar el valor de la variable global que recibe, de lo contrario, incluso si el código es semánticamente correcto, es No más un patrón de mónada debido a la comprobación de tipos.

La associative law significa que el orden de las composiciones monádicas no es importante. Esto está de acuerdo con la evaluación perezosa y el modelo matemático de componer el mismo operador de forma asociativa.