¿Ejemplo concreto que muestra que las mónadas no están cerradas bajo composición (con prueba)?

Es bien sabido que los functores aplicativos están cerrados bajo composición, pero las mónadas no. Sin embargo, he tenido problemas para encontrar un contraejemplo concreto que muestre que las mónadas no siempre componen.

Esta respuesta da [String -> a]como ejemplo de una no mónada. Después de jugar un poco con él, lo creo intuitivamente, pero esa respuesta simplemente dice "la unión no se puede implementar" sin realmente dar ninguna justificación. Quisiera algo más formal. Por supuesto, hay muchas funciones con tipo [String -> [String -> a]] -> [String -> a]; hay que demostrar que tal función no satisface necesariamente las leyes de la mónada.

Cualquier ejemplo (con prueba adjunta) servirá; No estoy buscando necesariamente una prueba del ejemplo anterior en particular.

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

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ónelo con la Maybemónada:

newtype Bad a = B (Maybe (Pair a))

Afirmo que Badno puede ser una mónada.

Prueba parcial:

Solo hay una forma de definir fmapque satisface fmap id = id:

instance Functor Bad where
    fmap f (B x) = B $ fmap (fmap f) x

Recuerde las leyes de las mónadas:

(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 Nothingo B (Just (P x x)). Está claro que para tener alguna esperanza de regresar xde (1) y (2), no podemos tirar x, por lo que tenemos que elegir la segunda opción.

return' :: a -> Bad a
return' x = B (Just (P x x))

Eso se va join. Dado que solo hay unas pocas 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)))))) = ???

Dado que la salida tiene tipo Bad a, las únicas opciones son B Nothingo B (Just (P y1 y2))dónde y1, y2deben elegirse x1 ... x4.

En los casos (A) y (B), no tenemos valores de tipo a, por lo que estamos obligados a regresar B Nothingen ambos casos.

El caso (E) está determinado por las leyes de las mónadas (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 y1entre x1o x3, y y2entre x2o 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))

Asimismo, esto dice que debemos elegir y1entre x1o x2, y y2entre x3o 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 intentas completar los lados derechos para (C) y (D).

Hay 5 lados derechos posibles para cada uno y ninguna de las combinaciones funciona. Todavía no tengo un buen argumento para esto, pero 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 returny >>=simplemente vete Thud, y las leyes se cumplen trivialmente.

Ahora tengamos también la mónada de escritura 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 x, por lo que debe ser una constante. Como resultado, join . returnes necesariamente una función constante también, de ahí la ley

join . return = id

Debe fallar para cualquier definición de joiny returnque elijamos.

Construyendo el medio excluido

(->) res una mónada para todos ry Either ees una mónada para todos e. Definamos su composición ( (->) rinterior, Either eexterior):

import Control.Monad
newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }

Afirmo que si Comp r efuera una mónada para todos ry eentonces podríamos realizar la ley del medio excluido . Esto no es posible en la lógica intuicionista que subyace a los tipos de sistemas de lenguajes funcionales (tener la ley del medio excluido es equivalente a tener el operador call / cc ).

Supongamos que Compes una mónada. Entonces tenemos

join :: Comp r e (Comp r e a) -> Comp r e a

y así podemos definir

swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)

(Esta es solo la swapfunción del papel Componer mónadas que menciona Brent, Sección 4.3, solo con los constructores (de) de newtype agregados. Tenga en cuenta que no nos importa qué propiedades tiene, lo único importante es que es definible y total .)

Ahora vamos a configurar

data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation

y especializado de intercambio para r = b, e = b, a = False:

excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left

Conclusión: Aunque (->) ry Either rson mónadas, su composición Comp r rno puede serlo.

Nota: Que esto también se refleja en la forma ReaderTy EitherTse definen. ¡Ambos ReaderT r (Either e) y EitherT e (Reader r)son isomorfos a r -> Either e a! No hay forma de definir la mónada para el dual Either e (r -> a).

IOAcciones de escape

Hay muchos ejemplos en la misma línea que involucran IOy que conducen a escapar de IOalguna 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 tengamos

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 se ejecute este programa? Hay dos posibilidades:

1. "Primero" o "Segundo" se imprime después de que leemos inputdesde la consola, lo que significa que la secuencia de acciones se invirtió y que las acciones de fooescapó a puro f.

2. O swap(por lo tanto join) descarta la IOacción y nunca se imprime ni "Primero" ni "Segundo". Pero esto significa que joinviola la ley

   join . return = id
   

   porque si joindesecha la IOacción, entonces

   foo ≠ (join . return) foo
   

Otras IOcombinaciones similares de 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 sus joinimplementaciones deben permitir eescapar IOo deben tirarlo y reemplazarlo con otra cosa, violando la ley.

Su enlace hace referencia a este tipo de datos, así que intentemos elegir una implementación específica: data A3 a = A3 (A1 (A2 a))

Elegiré arbitrariamente A1 = IO, A2 = []. También lo haremos newtypey le daremos un nombre particularmente puntiagudo, por diversión:

newtype ListT IO a = ListT (IO [a])

Vamos a pensar en una acción arbitraria de ese tipo y ejecutarla 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 se puede ver, esto rompe la ley asociatividad: ∀x y z. (x >=> y) >=> z == x >=> (y >=> z).

Resulta que ListT mes solo una mónada si mes una mónada conmutativa . Esto evita que se componga una gran categoría de mónadas [], lo que rompe la regla universal de "componer dos mónadas arbitrarias produce una mónada".

Véase también: https://stackoverflow.com/a/12617918/1769569

Las mónadas no componen. No de forma genérica, no existe una forma general de componer mónadas. Ver https://www.slideshare.net/pjschwarz/monads-do-not-compose