math - percepcion - ¿Qué es un ejemplo de una Mónada que es una alternativa pero no un MonadPlus?

monadas leibniz

Question

En su respuesta a la pregunta "¿Distinción entre las clases de tipos MonadPlus , Alternative y Monoid ?" , Edward Kmett dice que

Además, incluso si Applicative fuera una superclase de Monad , terminarías necesitando la clase MonadPlus todos modos, porque obedecer

empty <*> m = empty

no es estrictamente suficiente para demostrar que

empty >>= f = empty

Entonces, afirmar que algo es un MonadPlus es más fuerte que afirmar que es Alternative .

Está claro que cualquier funcionador aplicativo que no sea una mónada es automáticamente un ejemplo de una Alternative que no es un MonadPlus , pero la respuesta de Edward Kmett implica que existe una mónada que es una Alternative pero no un MonadPlus : está empty y <|> haría satisfacer las leyes Alternative , ¹ pero no las leyes MonadPlus . ² No puedo dar con un ejemplo de esto solo; ¿Alguien sabe de uno?

¹ No pude encontrar una referencia canónica para un conjunto de leyes Alternative , pero planteo lo que creo que son más o menos a la mitad de mi respuesta a la pregunta "Confundido por el significado de la clase de tipo Alternative y su relación con otras clases de tipos " (busque la frase" distributividad correcta "). Las cuatro leyes que creo deberían tener son:

1. Distributividad derecha (de <*> ): (f <|> g) <*> a = (f <*> a) <|> (g <*> a)
2. Absorción derecha (para <*> ): empty <*> a = empty
3. Distributividad izquierda (de fmap ): f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
4. Absorción izquierda (para fmap ): f <$> empty = empty

También felizmente acepto recibir un conjunto más útil de leyes Alternative .

² Sé que hay cierta ambigüedad acerca de las leyes de MonadPlus ; Estoy contento con una respuesta que usa la distribución izquierda o la izquierda, aunque preferiría débilmente la anterior.

Answer 1

La clave de tu respuesta está en HaskellWiki sobre MonadPlus a la que vinculaste :

¿Qué reglas? Martin y Gibbons eligen Monoid, Left Zero y Left Distribution. Esto hace que [] un MonadPlus, pero no sea Maybe o IO .

Entonces, según su elección preferida, Maybe no es un MonadPlus (aunque hay una instancia, no satisface la distribución izquierda). Probemos que satisface la alternativa.

Maybe es una alternativa

1. Distributividad derecha (de <*> ): (f <|> g) <*> a = (f <*> a) <|> (g <*> a)

Caso 1: f=Nothing :

(Nothing <|> g) <*> a = (g) <*> a -- left identity <|>
= Nothing <|> (g <*> a) -- left identity <|>
= (Nothing <*> a) <|> (g <*> a) -- left failure <*>

Caso 2: a=Nothing :

(f <|> g) <*> Nothing = Nothing -- right failure <*>
= Nothing <|> Nothing -- left identity <|>
= (f <*> Nothing) <|> (g <*> Nothing) -- right failure <*>

Caso 3: f=Just h, a = Just x

(Just h <|> g) <*> Just x = Just h <*> Just x -- left bias <|>
= Just (h x) -- success <*>
= Just (h x) <|> (g <*> Just x) -- left bias <|>
= (Just h <*> Just x) <|> (g <*> Just x) -- success <*>

1. Absorción derecha (para <*> ): empty <*> a = empty

Eso es fácil, porque

Nothing <*> a = Nothing -- left failure <*>

1. Distributividad izquierda (de fmap ): f <$> (a <|> b) = (f <$> a) <|> (f <$> b)

Caso 1: a = Nothing

f <$> (Nothing <|> b) = f <$> b -- left identity <|>
= Nothing <|> (f <$> b) -- left identity <|>
= (f <$> Nothing) <|> (f <$> b) -- failure <$>

Caso 2: a = Just x

f <$> (Just x <|> b) = f <$> Just x -- left bias <|>
= Just (f x) -- success <$>
= Just (f x) <|> (f <$> b) -- left bias <|>
= (f <$> Just x) <|> (f <$> b) -- success <$>

1. Absorción izquierda (para fmap ): f <$> empty = empty

Otra fácil:

f <$> Nothing = Nothing -- failure <$>

Maybe no es un MonadPlus

Vamos a probar la afirmación de que Maybe no es un MonadPlus: Tenemos que mostrar que mplus ab >>= k = mplus (a >>= k) (b >>= k) no siempre se cumple. El truco es, como siempre, usar un enlace para escabullir valores muy diferentes:

a = Just False
b = Just True
k True = Just "Made it!"
k False = Nothing

Ahora

mplus (Just False) (Just True) >>= k = Just False >>= k
= k False
= Nothing

aquí he usado bind (>>=) para arrebatar el fracaso ( Nothing ) de las mandíbulas de la victoria porque Just False parecía éxito.

mplus (Just False >>= k) (Just True >>= k) = mplus (k False) (k True)
= mplus Nothing (Just "Made it!")
= Just "Made it!"

Aquí, la falla ( k False ) se calculó temprano, por lo que nos ignoraron y "Made it!" logramos "Made it!" .

Entonces, mplus ab >>= k = Nothing más que mplus (a >>= k) (b >>= k) = Just "Made it!" .

Puedes ver esto como yo usando >>= para romper el sesgo izquierdo de mplus para Maybe .

Validez de mis pruebas:

En caso de que sintieras que no había hecho suficientes derivaciones tediosas, probaré las identidades que utilicé:

en primer lugar

Nothing <|> c = c -- left identity <|>
Just d <|> c = Just d -- left bias <|>

que provienen de la declaración de instancia

instance Alternative Maybe where
empty = Nothing
Nothing <|> r = r
l <|> _ = l

En segundo lugar

f <$> Nothing = Nothing -- failure <$>
f <$> Just x = Just (f x) -- success <$>

que solo viene de (<$>) = fmap y

instance Functor Maybe where
fmap _ Nothing = Nothing
fmap f (Just a) = Just (f a)

En tercer lugar, los otros tres requieren un poco más de trabajo:

Nothing <*> c = Nothing -- left failure <*>
c <*> Nothing = Nothing -- right failure <*>
Just f <*> Just x = Just (f x) -- success <*>

Que viene de las definiciones

instance Applicative Maybe where
pure = return
(<*>) = ap
ap :: (Monad m) => m (a -> b) -> m a -> m b
ap = liftM2 id
liftM2 :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 f m1 m2 = do { x1 <- m1; x2 <- m2; return (f x1 x2) }
instance Monad Maybe where
(Just x) >>= k = k x
Nothing >>= _ = Nothing
return = Just

asi que

mf <*> mx = ap mf mx
= liftM2 id mf mx
= do { f <- mf; x <- mx; return (id f x) }
= do { f <- mf; x <- mx; return (f x) }
= do { f <- mf; x <- mx; Just (f x) }
= mf >>= /f ->
mx >>= /x ->
Just (f x)

entonces si mf o mx son Nada, el resultado es también Nothing , mientras que si mf = Just f y mx = Just x , el resultado es Just (fx)