applicative functor は構成下で閉じているが、モナドは閉じていないことはよく知られています。しかし、モナドが常に構成するとは限らないことを示す具体的な反例を見つけるのに苦労しています。
この回答は[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を満たすことを定義する方法は 1 つしかありません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 つの選択肢があります。(1) と (2) から戻る希望を持つためには、 を捨てることができないことは明らかなので、2 番目のオプションを選択する必要があります。B NothingB (Just (P x x))xx
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)))))) = ???
出力には typeがあるため、Bad aオプションはB Nothingor B (Just (P y1 y2))whereのみです。from を選択する必要があります。y1y2x1 ... x4
(A) と (B) の場合、 type の値がない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から選択する必要があることを意味します。x1x3y2x2x4
-- 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から選択する必要があることを示しています。2 つを組み合わせて、(E) の右辺が でなければならないことを決定します。x1x2y2x3x4B (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 の writer モナドも用意しましょう (たとえば、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)
...
パラメトリック性は、???が に有用な方法で依存できないことを示してxいるため、定数でなければなりません。その結果、join . returnも必然的に定数関数になるため、法則
join . return = id
私たちが選んだjoinandの定義が何であれ失敗しなければなりません。return
(->) rは every のモナドであり、 everyrのEither eモナドですe。それらの構成を定義しましょう（(->) r内側、Either e外側）：
import Control.Monad
newtype Comp r e a = Comp { uncomp :: Either e (r -> a) }
私は、every のモナドであれば、除外された middle の法則を実現できるComp r ereと主張します。これは、関数型言語の型システムの根底にある直観主義のロジックでは不可能です (排除された中間の法則を持つことは、 call/cc演算子を持つことと同じです)。
Compがモナドであるとしましょう。次に、
join :: Comp r e (Comp r e a) -> Comp r e a
したがって、定義できます
swap :: (r -> Either e a) -> Either e (r -> a)
swap = uncomp . join . Comp . return . liftM (Comp . liftM return)
(これは、Brent が言及しているswap紙のComposing monads セクション4.3 の関数であり、newtype の (デ) コンストラクターが追加されているだけです。どのようなプロパティを持っているかは気にしないことに注意してください。唯一の重要なことは、それが定義可能で完全であることです。 .)
設定してみましょう
data False -- an empty datatype corresponding to logical false
type Neg a = (a -> False) -- corresponds to logical negation
r = b、e = b、 のスワップを特殊化しa = Falseます。
excludedMiddle :: Either b (Neg b)
excludedMiddle = swap Left
結論:(->) rとはモナドですEither rが、それらの構成はモナドにはComp r rなりません。
注: これは、ReaderTおよびEitherTの定義方法にも反映されています。とはどちらも !に同形です。dual に対してモナドを定義する方法はありません。ReaderT r (Either e)EitherT e (Reader r)r -> Either e aEither e (r -> a)
IOアクション同じように、何らかの形IOで脱出につながる例がたくさんあります。IO例えば：
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)
さあ、いただきましょう
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)
このプログラムを実行するとどうなりますか? 次の 2 つの可能性があります。
inputfoofまたはswap(したがってjoin)IOアクションを破棄し、"First" も "Second" も出力されません。しかし、これはjoin法律に違反することを意味します
join . return = id
アクションを破棄するjoin場合、IO
foo ≠ (join . return) foo
他の同様のIO+ モナドの組み合わせは構築につながります
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)
...
それらの実装は、法律に違反して、それから逃れることをjoin許可するか、それを捨てて別のものに置き換える必要があります。eIO
リンクはこのデータ型を参照しているので、特定の実装を選択してみましょう。data A3 a = A3 (A1 (A2 a))
勝手に選びA1 = IO, A2 = []ます。またnewtype、楽しみのために、それを作成し、特に尖った名前を付けます。
newtype ListT IO a = ListT (IO [a])
そのタイプの任意のアクションを考え出し、2つの異なるが等しい方法で実行してみましょう。
λ> 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]
ご覧のとおり、これは結合法則に違反します∀x y z. (x >=> y) >=> z == x >=> (y >=> z)。
可換ListT mモナドの場合mは、モナドにすぎません。これにより、大きなカテゴリのモナドがで構成されなくなり、「2つの任意のモナドを構成するとモナドが生成される」という普遍的なルールが破られます。[]