math - percepcion - ¿Qué es un ejemplo de una Mónada que es una alternativa pero no un MonadPlus?
monadas leibniz (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 seaMaybe
oIO
.
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
- 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 <*>
- Absorción derecha (para
<*>
):empty <*> a = empty
Eso es fácil, porque
Nothing <*> a = Nothing -- left failure <*>
- 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 <$>
- 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)
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 deMonad
, terminarías necesitando la claseMonadPlus
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 esAlternative
.
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
, 1 pero no las leyes MonadPlus
. 2 No puedo dar con un ejemplo de esto solo; ¿Alguien sabe de uno?
1 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:
- Distributividad derecha (de
<*>
):(f <|> g) <*> a = (f <*> a) <|> (g <*> a)
- Absorción derecha (para
<*>
):empty <*> a = empty
- Distributividad izquierda (de
fmap
):f <$> (a <|> b) = (f <$> a) <|> (f <$> b)
- Absorción izquierda (para
fmap
):f <$> empty = empty
También felizmente acepto recibir un conjunto más útil de leyes Alternative
.
2 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.