haskell - razon - teoria de las monadas segun leibniz

¿Por qué usar un tipo de función tan peculiar en las mónadas?

Question

Nuevo en Haskell, y estoy tratando de resolver este asunto de la Mónada. El operador de enlace monádico - >>= - tiene una firma de tipo muy peculiar:

(>>=) :: Monad m => m a -> (a -> m b) -> m b

Para simplificar, sustituyamos Maybe por m :

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b

Sin embargo, tenga en cuenta que la definición podría haberse escrito de tres maneras diferentes:

(>>=) :: Maybe a -> (Maybe a -> Maybe b) -> Maybe b
(>>=) :: Maybe a -> ( a -> Maybe b) -> Maybe b
(>>=) :: Maybe a -> ( a -> b) -> Maybe b

De los tres, el del centro es el más asimétrico. Sin embargo, entiendo que el primero no tiene ningún significado si queremos evitarlo (lo que LYAH llama código repetitivo). Sin embargo, de los dos siguientes, preferiría el último. Para Maybe , esto se vería como:

Cuando esto se define como:

(>>=) :: Maybe a -> (a -> b) -> Maybe b
instance Monad Maybe where
Nothing >>= f = Nothing
(Just x) >>= f = return $ f x

Aquí, a -> b es una función ordinaria. Además, no veo nada inseguro de inmediato, porque Nothing detecta la excepción antes de la aplicación de la función, por lo que la función a -> b no se llamará a menos que se obtenga un Just a .

Así que tal vez haya algo que no me parece que haya causado la definición (>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b sea ​​la preferida sobre la mucho más simple (>>=) :: Maybe a -> (a -> b) -> Maybe b definición? ¿Hay algún problema inherente asociado con (lo que creo que es a) una definición más simple?

Answer 1

Consideremos uno de los usos comunes de la mónada Maybe : el manejo de errores. Digamos que quería dividir dos números de manera segura. Podría escribir esta función:

safeDiv :: Int -> Int -> Maybe Int
safeDiv _ 0 = Nothing
safeDiv n d = n `div` d

Luego, con la mónada estándar Maybe , podría hacer algo como esto:

foo :: Int -> Int -> Maybe Int
foo a b = do
c <- safeDiv 1000 b
d <- safeDiv a c -- These last two lines could be combined.
return d -- I am not doing so for clarity.

Tenga en cuenta que en cada paso, safeDiv puede fallar, pero en ambos pasos, safeDiv toma Int s, no Maybe Int s. Si >>= tenía esta firma:

(>>=) :: Maybe a -> (a -> b) -> Maybe b

Podrías componer funciones juntas, luego darle una Nothing o una Just , y desenvolvería la Just , recorrería toda la tubería y volvería a envolverla en la Just , o simplemente pasaría la Nothing esencialmente sin tocar. Eso podría ser útil, pero no es una mónada. Para que sea de alguna utilidad, tenemos que ser capaces de fallar en el medio, y eso es lo que esta firma nos da:

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b

Por cierto, existe algo con la firma que usted ideó:

flip fmap :: Maybe a -> (a -> b) -> Maybe b

Answer 2

El problema con la firma de tipo alternativa para (>>=) es que solo funciona accidentalmente para la mónada Maybe, si la prueba con otra mónada (es decir, la mónada de la Lista) verá que se descompone en el tipo de b para El caso general. La firma que proporcionó no describe un enlace monádico y las leyes de la mónada no se pueden mantener con esa definición.

import Prelude hiding (Monad, return)
-- assume monad was defined like this
class Monad m where
(>>=) :: m a -> (a -> b) -> m b
return :: a -> m a
instance Monad Maybe where
Nothing >>= f = Nothing
(Just x) >>= f = return $ f x
instance Monad [] where
m >>= f = concat (map f m)
return x = [x]

Falla con el error de tipo:

 Couldn''t match type `b'' with `[b]''
`b'' is a rigid type variable bound by
the type signature for >>= :: [a] -> (a -> b) -> [b]
at monadfail.hs:12:3
Expected type: a -> [b]
Actual type: a -> b
In the first argument of `map'', namely `f''
In the first argument of `concat'', namely `(map f m)''
In the expression: concat (map f m)

Answer 3

Es mucho más simétrico si piensa en términos de la siguiente función derivada (de Control.Monad ):

(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(f >=> g) x = f x >>= g

La razón por la que esta función es significativa es que obedece a tres ecuaciones útiles:

-- Associativity
(f >=> g) >=> h = f >=> (g >=> h)
-- Left identity
return >=> f = f
-- Right identity
f >=> return = f

Estas son leyes de categoría y si las traduce para usar (>>=) lugar de (>=>) , obtiene las tres leyes de la mónada:

(m >>= g) >>= h = m >>= /x -> (g x >>= h)
return x >>= f = f x
m >>= return = m

Entonces realmente no es (>>=) el operador elegante, sino que (>=>) es el operador simétrico que está buscando. Sin embargo, la razón por la que generalmente pensamos en términos de (>>=) es porque esa es la razón por la cual los usuarios de notación lo do .

Answer 4

La función más complicada con a -> Maybe b es la más genérica y útil y puede usarse para implementar la simple. Eso no funciona al revés.

Puede construir una función a -> Maybe b partir de una función f :: a -> b :

f'' :: a -> Maybe b
f'' x = Just (f x)

O, en términos de return (que es Just para Maybe ):

f'' = return . f

Lo contrario no es necesariamente posible. Si tiene una función g :: a -> Maybe b y quiere usarla con el enlace "simple", primero tendría que convertirla en una función a -> b . Pero esto no suele funcionar, porque g podría devolver Nothing donde la función a -> b necesita devolver un valor b .

Por lo general, el enlace "simple" se puede implementar en términos del "complicado", pero no al revés. Además, el enlace complicado es a menudo útil y no tenerlo haría muchas cosas imposibles. Entonces, al usar las mónadas de enlace más genéricas se aplican a más situaciones.

Answer 5

Lo que hace que una mónada sea una mónada es cómo funciona la "unión". Recordemos que la unión tiene el tipo:

join :: m (m a) -> m a

Lo que hace ''join'' es "interpretar" una acción de mónada que devuelve una acción de mónada en términos de una acción de mónada. Entonces, puedes pensar que se está desprendiendo una capa de la mónada (o mejor aún, tirando de las cosas de la capa interior hacia la capa exterior). Esto significa que las ''m'' forman una "pila", en el sentido de una "pila de llamadas". Cada ''m'' representa un contexto, y ''unirse'' nos permite unir contextos, en orden.

Entonces, ¿qué tiene esto que ver con el enlace? Recordar:

(>>=) :: m a -> (a -> m b) -> m b

Y ahora considera que para f :: a -> mb, y ma :: ma:

fmap f ma :: m (m b)

Es decir, el resultado de aplicar f directamente a la a en ma es an (m (mb)). Podemos aplicar unirse a esto, para obtener un m b. En breve,

ma >>= f = join (fmap f ma)