[解決済み] モナドが合成の下では閉じていないことを示す具体例(証明付き)?

質問

適用型ファンクタは合成のもとで閉じているが、モナドは閉じていないことはよく知られている。 しかし、私はモナドが常に合成されるわけではないことを示す具体的な反例を見つけるのに苦労しています。

この回答 は [String -> a] を非モナドの例として挙げています。 少し遊んでみて、私は直感的にそれを信じていますが、この回答は正当な理由を与えることなく、ただ"joinは実装できません"と言っています。 もっと正式なものが欲しいです。 もちろん、型 [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 を定義する場合、2つの選択肢があります。 B Nothing または B (Just (P x x)) . を返す望みを持つためには、明らかなことです。 x を返すためには、(1)と(2)から x を捨てられないので、2番目の選択肢を選ぶしかない。

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