Exemple concret montrant que les monades ne sont pas fermées en composition (avec preuve)?

considérez ce monad qui est isomorphe au (Bool ->) monad:

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

et la composer avec le Maybe monad:

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

j'affirme que Bad ne peut pas être une monade.

---

preuve partielle:

il n'y a qu'une seule façon de définir fmap qui satisfasse fmap id = id :

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

Rappel de la monade lois:

(1) join (return x) = x 
(2) join (fmap return x) = x
(3) join (join x) = join (fmap join x)

Pour la définition de return x , nous avons deux choix: B Nothing ou B (Just (P x x)) . Il est clair que pour avoir un quelconque espoir de retourner x de (1) et (2), nous ne pouvons pas jeter x , donc nous devons choisir la deuxième option.

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

qui laisse join . Puisqu'il n'y a que quelques entrées possibles, nous pouvons faire un cas pour chacune:

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)))))) = ???

puisque la sortie a le type Bad a , les seules options sont B Nothing ou B (Just (P y1 y2)) où y1 , y2 doivent être choisis de x1 ... x4 .

dans les cas (a) et (B), Nous n'avons pas de valeurs de type a , donc nous sommes forcés de retourner B Nothing dans les deux cas.

le cas E) est déterminé par les lois (1) et (2) monad:

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

pour retourner B (Just (P y1 y2)) dans le cas (E), cela signifie que nous devons choisir y1 de x1 ou x3 " , et y2 de x2 ou 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))

de même, ceci dit que nous devons choisir y1 de x1 ou x2 , et y2 de x3 ou x4 . En combinant les deux, nous déterminons que le côté droit de (E) doit être B (Just (P x1 x4)) .

jusqu'à présent tout va bien, mais le problème vient quand vous essayez de remplir les côtés de la main droite pour (C) et (d).

il y a 5 côtés droits possibles pour chacun, et aucune des combinaisons ne fonctionne. Je n'ai pas encore d'argument valable pour cela, mais j'ai un programme qui teste de manière exhaustive toutes les combinaisons:

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