모나드가 컴포지션에서 닫히지 않음을 보여주는 구체적인 예 (증거 포함)?

모나드가 컴포지션에서 닫히지 않음을 보여주는 구체적인 예 (증거 포함)?

---

응용 펑 터는 컴포지션에서 닫히지 만 모나드는 그렇지 않다는 것은 잘 알려져 있습니다. 그러나 나는 모나드가 항상 구성하지 않는다는 것을 보여주는 구체적인 반례를 찾는 데 어려움을 겪었습니다.

이 답변 은 [String -> a]모나드가 아닌 예를 제공합니다 . 잠시 가지고 놀다가 직관적으로 믿고 있지만 그 대답은 실제로 정당화하지 않고 "조인을 구현할 수 없습니다"라고 말합니다. 좀 더 공식적인 것을 원합니다. 물론 type과 함께 많은 함수가 있습니다 [String -> [String -> a]] -> [String -> a]. 그러한 함수가 반드시 모나드 법칙을 만족하지 않는다는 것을 보여 주어야합니다.

모든 예 (증거 포함)가 가능합니다. 특별히 위의 예에 대한 증거를 찾는 것은 아닙니다.

---

모나드와 동형 인 다음 모나드를 고려하십시오 (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

Maybe모나드로 구성합니다 .

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

나는 그것이 Bad모나드가 될 수 없다고 주장합니다 .

---

부분 증명 :

다음 fmap을 충족시키는 정의 하는 방법은 하나뿐입니다 fmap id = id.

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

모나드 법칙을 상기하십시오.

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

의 정의 return x에는 두 가지 선택이 있습니다. B Nothing또는 B (Just (P x x)). x(1)과 (2)에서 돌아올 희망을 가지려면 버릴 수 없으므로 x두 번째 옵션을 선택해야합니다.

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

그것은 떠난다 join. 가능한 입력이 적기 때문에 각각에 대해 케이스를 만들 수 있습니다.

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

출력 형식을 갖기 때문에 Bad a, 유일한 옵션은 B Nothing또는 B (Just (P y1 y2))여기서 y1, y2로부터 선택되어야한다 x1 ... x4.

(A)와 (B)의 경우 유형 값이 없으므로 두 경우 모두 a반환해야합니다 B Nothing.

사례 (E)는 (1) 및 (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))

반환하기 위해 B (Just (P y1 y2))케이스 (E)에서,이 방법은 우리가 선택해야 y1하나에서 x1나 x3, 그리고 y2에서 하나 x2또는 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))

마찬가지로, 이것은 우리가 선택해야한다고 말한다 y1하나에서 x1나 x2, 그리고 y2에서 하나 x3또는 x4. 두 가지를 결합하여 (E)의 오른쪽이이어야 함을 결정합니다 B (Just (P x1 x4)).

지금까지는 모든 것이 좋지만 (C)와 (D)의 오른쪽을 채우려 고 할 때 문제가 발생합니다.

각각에 대해 5 개의 가능한 오른쪽이 있으며 조합이 작동하지 않습니다. 아직 이에 대한 좋은 주장은 없지만 모든 조합을 철저히 테스트하는 프로그램이 있습니다.

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

---

작은 구체적인 반례의 경우 터미널 모나드를 고려하십시오.

data Thud x = Thud

return및 >>=바로 가서 Thud하고, 법은 하찮게십시오.

이제 Bool에 대한 라이터 모나드 (예를 들어 xor-monoid 구조)도 만들어 보겠습니다.

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

어, 음, 작곡이 필요해

newtype (:.:) f g x = C (f (g x))

이제 정의 해보세요 ...

instance Monad (Flip :.: Thud) where  -- that's effectively the constant `Bool` functor
  return x = C (Flip ??? Thud)
  ...

Parametricity는 ???에 어떤 유용한 방식으로도 의존 할 수 없으므로 x상수 여야합니다. 결과적으로 join . return반드시 일정한 기능이므로 법칙은

join . return = id

정의가 무엇이든 실패해야 join하며 return우리는 선택합니다.

---

제외 된 중간 구성

(->) r is a monad for every r and Either e is a monad for every e. Let's define their composition ((->) r inside, Either e outside):

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

I claim that if Comp r e were a monad for every r and e then we could realize the law of exluded middle. This is not possible in intuitionistic logic which underlies typesystems of functional languages (having the law of excluded middle is equivalent to having the call/cc operator).

Let's assume Comp is a monad. Then we have

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

and so we can define

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

(This is just the swap function from paper Composing monads that Brent mentions, Sect. 4.3, only with newtype's (de)constructors added. Note that we don't care what properties it has, the only important thing is that it is definable and total.)

Now let's set

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

and specialize swap for r = b, e = b, a = False:

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

Conclusion: Even though (->) r and Either r are monads, their composition Comp r r cannot be.

Note: That this is also reflected in how ReaderT and EitherT are defined. Both ReaderT r (Either e) and EitherT e (Reader r) are isomorphic to r -> Either e a! There is no way how to define monad for the dual Either e (r -> a).

---

Escaping IO actions

There are many examples in the same vein that involve IO and which lead to escaping IO somehow. For example:

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)

Now let's have

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)

What will happen when this program is run? There are two possibilities:

1. "First" or "Second" is printed after we read input from the console, meaning that the sequence of actions was reversed and that the actions from foo escaped into pure f.

2. Or swap (hence join) throws away the IO action and neither "First" nor "Second" is ever printed. But this means that join violates the law

   join . return = id
   

   because if join throws the IO action away, then

   foo ≠ (join . return) foo
   

Other similar IO + monad combinations lead to constructing

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

Either their join implementations must allow e to escape from IO or they must throw it away and replace with something else, violating the law.

---

Your link references this data type, so let's try picking some specific implementation: data A3 a = A3 (A1 (A2 a))

I will arbitrarily pick A1 = IO, A2 = []. We'll also make it a newtype and give it a particularly pointed name, for fun:

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

Let's come up with some arbitrary action in that type, and run it in two different-but-equal ways:

λ> 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]

As you can see, this breaks the associativity law: ∀x y z. (x >=> y) >=> z == x >=> (y >=> z).

It turns out, ListT m is only a monad if m is a commutative monad. This prevents a large category of monads from composing with [], which breaks the universal rule of "composing two arbitrary monads yields a monad".

See also: https://stackoverflow.com/a/12617918/1769569

---

Monads do not compose. Not in a generic way - there is no general way of composing monads. See https://www.slideshare.net/pjschwarz/monads-do-not-compose

참고URL : https://stackoverflow.com/questions/13034229/concrete-example-showing-that-monads-are-not-closed-under-composition-with-proo