¿Ejemplo concreto que muestra que las mónadas no se cierran bajo la composición (con la prueba)?

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.

Considera esta mónada que es isomorfa a la mónada (Bool ->) :

 data Pair a = P aa instance Functor Pair where fmap f (P xy) = P (fx) (fy) instance Monad Pair where return x = P xx P ab >>= f = P xy where P x _ = fa P _ y = fb 

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 xx)) 

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 progtwig que prueba exhaustivamente todas las combinaciones:

 {-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables #-} import Control.Monad (guard) data Pair a = P aa deriving (Eq, Show) instance Functor Pair where fmap f (P xy) = P (fx) (fy) instance Monad Pair where return x = P xx P ab >>= f = P xy where P x _ = fa P _ y = fb 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 xx)) -- 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 , \ab -> B (Just (P aa)) , \ab -> B (Just (P ab)) , \ab -> B (Just (P ba)) , \ab -> B (Just (P bb)) ] :: [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 xy)), 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 xy)), 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 = fx Flip True x >>= f = Flip (not b) y where Flip by = fx 

Er, um, necesitaremos composición

 newtype (:.:) fgx = C (f (gx)) 

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.

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 rea = 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 re (Comp rea) -> Comp rea 

y entonces podemos definir

 swap :: (r -> Either ea) -> 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 ra = 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 progtwig se ejecute? Hay dos posibilidades:

  1. "Primero" o "Segundo" se imprime después de leer la input de la consola, lo que significa que la secuencia de acciones se invirtió y que las acciones de foo escaparon en f pura.
  2. O swap (de ahí join ) descarta la acción IO y nunca se imprime ni "Primero" ni "Segundo". Pero esto significa que join viola la ley

     join . return = id 

    porque si join arroja la acción IO , entonces

     foo ≠ (join . return) foo 

Otras combinaciones similares de IO + mónadas conducen a la construcción

 swapEither :: IO (Either ea) -> Either e (IO a) swapWriter :: (Monoid e) => IO (Writer ea) -> Writer e (IO a) swapState :: IO (State ea) -> 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.

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 vn = 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://stackoverflow.com/a/12617918/1769569

    Intereting Posts