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

que son las monadas

Question

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.

Answer 1

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:

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 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.

Answer 2

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

Answer 3

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.

Answer 4

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