haskell - son - ¿Ejemplo concreto que muestra que las mónadas no se cierran bajo la composición(con la prueba)?
que son las monadas (4)
Es bien sabido que los funtores aplicativos se cierran bajo composición pero las mónadas no. Sin embargo, he tenido problemas para encontrar un contraejemplo concreto que demuestre que las mónadas no siempre componen.
Esta respuesta da [String -> a] como un ejemplo de una no mónada. Después de jugar con esto un poco, lo creo intuitivamente, pero esa respuesta solo dice "join no se puede implementar" sin dar ninguna justificación. Me gustaría algo más formal. Por supuesto, hay muchas funciones con el tipo [String -> [String -> a]] -> [String -> a] ; uno debe demostrar que cualquier función de este tipo necesariamente no satisface las leyes de la mónada.
Cualquier ejemplo (con la prueba adjunta) servirá; No necesariamente estoy buscando una prueba del ejemplo anterior en particular.
Construyendo medio excluido
(->) r es una mónada para cada r y Either e es una mónada para cada e . Vamos a definir su composición ( (->) r dentro, Either e fuera):
import Control.Monad
newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }
Yo afirmo que si Comp re fuera una mónada para cada r y e entonces podríamos realizar la ley del centro excluido . Esto no es posible en la lógica intuicionista que subyace en los sistemas de idiomas funcionales (tener la ley del medio excluido es equivalente a tener el operador call/cc ).
Supongamos que Comp es una mónada. Entonces nosotros tenemos
join :: Comp r e (Comp r e a) -> Comp r e a
y entonces podemos definir
swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
(Esta es solo la función de swap de las mónadas de composición de papel que Brent menciona, Sección 4.3, solo con los constructores de tipo nuevo agregados. Tenga en cuenta que no nos importa qué propiedades tenga, lo único importante es que es definible y total.)
Ahora vamos a establecer
data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation
y especializar intercambio para r = b , e = b , a = False :
excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left
Conclusión: Aunque (->) r Either r son mónadas, su composición Comp rr no puede ser.
Nota: Esto también se refleja en cómo se definen ReaderT y EitherT . Tanto ReaderT r (Either e) como EitherT e (Reader r) son isomorfos para r -> Either ea ! No hay forma de cómo definir la mónada para el dual Either e (r -> a) .
Escapar acciones IO
Hay muchos ejemplos en la misma línea que implican IO y que conducen a escapar IO alguna manera. Por ejemplo:
newtype Comp r a = Comp { uncomp :: IO (r -> a) }
swap :: (r -> IO a) -> IO (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
Ahora vamos a tener
main :: IO ()
main = do
let foo True = print "First" >> return 1
foo False = print "Second" >> return 2
f <- swap foo
input <- readLn
print (f input)
¿Qué pasará cuando este programa se ejecute? Hay dos posibilidades:
- "Primero" o "Segundo" se imprime después de leer la
inputde la consola, lo que significa que la secuencia de acciones se invirtió y que las acciones defooescaparon enfpura. O
swap(de ahíjoin) descarta la acciónIOy nunca se imprime ni "Primero" ni "Segundo". Pero esto significa quejoinviola la leyjoin . return = idporque si
joinarroja la acciónIO, entoncesfoo ≠ (join . return) foo
Otras combinaciones similares de IO + mónadas conducen a la construcción
swapEither :: IO (Either e a) -> Either e (IO a)
swapWriter :: (Monoid e) => IO (Writer e a) -> Writer e (IO a)
swapState :: IO (State e a) -> State e (IO a)
...
O bien sus implementaciones de join deben permitir que e escape de IO o deben descartarlo y reemplazarlo por otra cosa, violando la ley.
Considera esta mónada que es isomorfa a la mónada (Bool ->) :
data Pair a = P a a
instance Functor Pair where
fmap f (P x y) = P (f x) (f y)
instance Monad Pair where
return x = P x x
P a b >>= f = P x y
where P x _ = f a
P _ y = f b
y compáralo con la mónada Maybe :
newtype Bad a = B (Maybe (Pair a))
Reclamo que Bad no puede ser una mónada.
Prueba parcial:
Solo hay una forma de definir fmap que satisfaga fmap id = id :
instance Functor Bad where
fmap f (B x) = B $ fmap (fmap f) x
Recuerda las leyes de la mónada:
(1) join (return x) = x
(2) join (fmap return x) = x
(3) join (join x) = join (fmap join x)
Para la definición de return x , tenemos dos opciones: B Nothing o B (Just (P xx)) . Está claro que para tener alguna esperanza de devolver x de (1) y (2), no podemos tirar x , así que tenemos que elegir la segunda opción.
return'' :: a -> Bad a
return'' x = B (Just (P x x))
Eso deja join . Como solo hay algunas entradas posibles, podemos hacer un caso para cada una:
join :: Bad (Bad a) -> Bad a
(A) join (B Nothing) = ???
(B) join (B (Just (P (B Nothing) (B Nothing)))) = ???
(C) join (B (Just (P (B (Just (P x1 x2))) (B Nothing)))) = ???
(D) join (B (Just (P (B Nothing) (B (Just (P x1 x2)))))) = ???
(E) join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = ???
Como la salida tiene el tipo Bad a , las únicas opciones son B Nothing o B (Just (P y1 y2)) donde y1 , y2 deben elegirse entre x1 ... x4 .
En los casos (A) y (B), no tenemos valores de tipo a , por lo que estamos obligados a devolver B Nothing en ambos casos.
El caso (E) está determinado por las leyes de mónada (1) y (2):
-- apply (1) to (B (Just (P y1 y2)))
join (return'' (B (Just (P y1 y2))))
= -- using our definition of return''
join (B (Just (P (B (Just (P y1 y2))) (B (Just (P y1 y2))))))
= -- from (1) this should equal
B (Just (P y1 y2))
Para devolver B (Just (P y1 y2)) en el caso (E), esto significa que debemos elegir y1 de x1 o x3 , y y2 de x2 o x4 .
-- apply (2) to (B (Just (P y1 y2)))
join (fmap return'' (B (Just (P y1 y2))))
= -- def of fmap
join (B (Just (P (return y1) (return y2))))
= -- def of return
join (B (Just (P (B (Just (P y1 y1))) (B (Just (P y2 y2))))))
= -- from (2) this should equal
B (Just (P y1 y2))
Del mismo modo, esto dice que debemos elegir y1 de x1 o x2 , y y2 de x3 o x4 . Combinando los dos, determinamos que el lado derecho de (E) debe ser B (Just (P x1 x4)) .
Hasta ahora todo está bien, pero el problema surge cuando tratas de rellenar los lados derechos para (C) y (D).
Hay 5 posibles lados derechos para cada uno, y ninguna de las combinaciones funciona. Todavía no tengo un buen argumento para esto, pero sí tengo un programa que prueba exhaustivamente todas las combinaciones:
{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-}
import Control.Monad (guard)
data Pair a = P a a
deriving (Eq, Show)
instance Functor Pair where
fmap f (P x y) = P (f x) (f y)
instance Monad Pair where
return x = P x x
P a b >>= f = P x y
where P x _ = f a
P _ y = f b
newtype Bad a = B (Maybe (Pair a))
deriving (Eq, Show)
instance Functor Bad where
fmap f (B x) = B $ fmap (fmap f) x
-- The only definition that could possibly work.
unit :: a -> Bad a
unit x = B (Just (P x x))
-- Number of possible definitions of join for this type. If this equals zero, no monad for you!
joins :: Integer
joins = sum $ do
-- Try all possible ways of handling cases 3 and 4 in the definition of join below.
let ways = [ /_ _ -> B Nothing
, /a b -> B (Just (P a a))
, /a b -> B (Just (P a b))
, /a b -> B (Just (P b a))
, /a b -> B (Just (P b b)) ] :: [forall a. a -> a -> Bad a]
c3 :: forall a. a -> a -> Bad a <- ways
c4 :: forall a. a -> a -> Bad a <- ways
let join :: forall a. Bad (Bad a) -> Bad a
join (B Nothing) = B Nothing -- no choice
join (B (Just (P (B Nothing) (B Nothing)))) = B Nothing -- again, no choice
join (B (Just (P (B (Just (P x1 x2))) (B Nothing)))) = c3 x1 x2
join (B (Just (P (B Nothing) (B (Just (P x3 x4)))))) = c4 x3 x4
join (B (Just (P (B (Just (P x1 x2))) (B (Just (P x3 x4)))))) = B (Just (P x1 x4)) -- derived from monad laws
-- We''ve already learnt all we can from these two, but I decided to leave them in anyway.
guard $ all (/x -> join (unit x) == x) bad1
guard $ all (/x -> join (fmap unit x) == x) bad1
-- This is the one that matters
guard $ all (/x -> join (join x) == join (fmap join x)) bad3
return 1
main = putStrLn $ show joins ++ " combinations work."
-- Functions for making all the different forms of Bad values containing distinct Ints.
bad1 :: [Bad Int]
bad1 = map fst (bad1'' 1)
bad3 :: [Bad (Bad (Bad Int))]
bad3 = map fst (bad3'' 1)
bad1'' :: Int -> [(Bad Int, Int)]
bad1'' n = [(B Nothing, n), (B (Just (P n (n+1))), n+2)]
bad2'' :: Int -> [(Bad (Bad Int), Int)]
bad2'' n = (B Nothing, n) : do
(x, n'') <- bad1'' n
(y, n'''') <- bad1'' n''
return (B (Just (P x y)), n'''')
bad3'' :: Int -> [(Bad (Bad (Bad Int)), Int)]
bad3'' n = (B Nothing, n) : do
(x, n'') <- bad2'' n
(y, n'''') <- bad2'' n''
return (B (Just (P x y)), n'''')
Para un pequeño contraejemplo concreto, considere la mónada terminal.
data Thud x = Thud
El return y >>= simplemente van a Thud , y las leyes son triviales.
Ahora vamos a tener también la mónada del escritor para Bool (con, digamos, la estructura xor-monoide).
data Flip x = Flip Bool x
instance Monad Flip where
return x = Flip False x
Flip False x >>= f = f x
Flip True x >>= f = Flip (not b) y where Flip b y = f x
Er, um, necesitaremos composición
newtype (:.:) f g x = C (f (g x))
Ahora intenta definir ...
instance Monad (Flip :.: Thud) where -- that''s effectively the constant `Bool` functor
return x = C (Flip ??? Thud)
...
La parametricidad nos dice que ??? no puede depender de ninguna manera útil en x , por lo que debe ser una constante. Como resultado, join . return join . return es necesariamente una función constante también, de ahí la ley
join . return = id
debe fallar para cualquier definición de join y return que elijamos.
Su enlace hace referencia a este tipo de datos, así que intentemos elegir alguna implementación específica: data A3 a = A3 (A1 (A2 a))
Seleccionaré arbitrariamente A1 = IO, A2 = [] . También lo convertiremos en un newtype y le daremos un nombre particularmente newtype , por diversión:
newtype ListT IO a = ListT (IO [a])
Propongamos alguna acción arbitraria en ese tipo, y ejecútelo de dos formas diferentes pero iguales:
λ> let v n = ListT $ do {putStr (show n); return [0, 1]}
λ> runListT $ ((v >=> v) >=> v) 0
0010101[0,1,0,1,0,1,0,1]
λ> runListT $ (v >=> (v >=> v)) 0
0001101[0,1,0,1,0,1,0,1]
Como puede ver, esto rompe la ley de asociatividad: ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) ∀xy z. (x >=> y) >=> z == x >=> (y >=> z) .
Resulta que ListT m es solo una mónada si m es una mónada conmutativa . Esto evita que una gran categoría de mónadas componga con [] , lo que rompe la regla universal de "componer dos mónadas arbitrarias produce una mónada".
Ver también: https://.com/a/12617918/1769569