IOモナドの法則を満たさないという言及を見たことがありますが、それを示す簡単な例は見つかりませんでした。誰かが例を知っていますか？ありがとう。
編集： ertesとnmが指摘したように、使用するseqことは、モナドが法則に違反する可能性があるため、少し違法です（と組み合わせるundefined）。undefined終了しない計算と見なされる可能性があるため、これを使用することはまったく問題ありません。
したがって、改訂された質問は次のとおりです。使用せずにモナド法を満たさないことを示す例を誰もが知っていますか？IOseqIO（または、許可されていない場合は法律を満たしている証拠seqですか？）
seqHaskellのすべてのモナドは、奇妙なコンビネータを除外した場合にのみモナドになります。これはにも当てはまりますIO。は実際には通常の関数ではありませんが、魔法が関係しているためseq、除外する必要があるのと同じ理由で、モナドの法則のチェックから除外する必要がありますunsafePerformIO。次のように、あなたを使用seqすると、すべてのモナドが間違っていることを証明できます。
クライスリ圏では、モナドはreturnアイデンティティの射であり、(<=<)構成です。したがって、次returnのIDである必要があります(<=<)：
return <=< x = x
Identityを使用しseqても、モナドにはならないかもしれません。
seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined :: a -> Identity b) () = undefined
seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined :: a -> Maybe b) () = undefined
tl; dr upfront：seqが唯一の方法です。
の実装はIO規格で規定されていないため、特定の実装のみを見ることができます。ソースから入手できるGHCの実装を見ると（舞台裏での特別な扱いの一部がIOモナド法の違反を引き起こしている可能性がありますが、私はそのような出来事を認識していません）、
-- in GHC.Types (ghc-prim)
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
-- in GHC.Base (base)
instance Monad IO where
{-# INLINE return #-}
{-# INLINE (>>) #-}
{-# INLINE (>>=) #-}
m >> k = m >>= \ _ -> k
return = returnIO
(>>=) = bindIO
fail s = failIO s
returnIO :: a -> IO a
returnIO x = IO $ \ s -> (# s, x #)
bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO $ \ s -> case m s of (# new_s, a #) -> unIO (k a) new_s
thenIO :: IO a -> IO b -> IO b
thenIO (IO m) k = IO $ \ s -> case m s of (# new_s, _ #) -> unIO k new_s
unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a
（厳密な）状態モナドとして実装されます。したがって、モナド法の違反は、IOによっても行われControl.Monad.State[.Strict]ます。
モナドの法則を見て、何が起こるか見てみましょうIO：
return x >>= f ≡ f x:
return x >>= f = IO $ \s -> case (\t -> (# t, x #)) s of
(# new_s, a #) -> unIO (f a) new_s
= IO $ \s -> case (# s, x #) of
(# new_s, a #) -> unIO (f a) new_s
= IO $ \s -> unIO (f x) s
newtypeラッパーを無視すると、はreturn x >>= fになり\s -> (f x) sます。それを（おそらく）区別する唯一の方法f xはですseq。（そして、seqそれを区別できるのはf x ≡ undefined。）
m >>= return ≡ m:
(IO k) >>= return = IO $ \s -> case k s of
(# new_s, a #) -> unIO (return a) new_s
= IO $ \s -> case k s of
(# new_s, a #) -> (\t -> (# t, a #)) new_s
= IO $ \s -> case k s of
(# new_s, a #) -> (# new_s, a #)
= IO $ \s -> k s
newtypeラッパーを再び無視すると、kに置き換えられます。これも、。\s -> k sによってのみ区別seqできk ≡ undefinedます。
m >>= (\x -> g x >>= h) ≡ (m >>= g) >>= h:
(IO k) >>= (\x -> g x >>= h) = IO $ \s -> case k s of
(# new_s, a #) -> unIO ((\x -> g x >>= h) a) new_s
= IO $ \s -> case k s of
(# new_s, a #) -> unIO (g a >>= h) new_s
= IO $ \s -> case k s of
(# new_s, a #) -> (\t -> case unIO (g a) t of
(# new_t, b #) -> unIO (h b) new_t) new_s
= IO $ \s -> case k s of
(# new_s, a #) -> case unIO (g a) new_s of
(# new_t, b #) -> unIO (h b) new_t
((IO k) >>= g) >>= h = IO $ \s -> case (\t -> case k t of
(# new_s, a #) -> unIO (g a) new_s) s of
(# new_t, b #) -> unIO (h b) new_t
= IO $ \s -> case (case k s of
(# new_s, a #) -> unIO (g a) new_s) of
(# new_t, b #) -> unIO (h b) new_t
今、私たちは一般的に持っています
case (case e of case e of
pat1 -> ex1) of ≡ pat1 -> case ex1 of
pat2 -> ex2 pat2 -> ex2
言語レポートの式3.17.3。（a）に従って、この法則はモジュロだけではありませんseq。
要約すると、とを区別できるIOという事実を除いて、モナドの法則を満たします。同じことが、、、、および関数型をラップする他のモナドにも当てはまります。sequndefined\s -> undefined sState[T]Reader[T](->) a
モナド法の1つはそれです
m >>= return ≡ m
GHCiで試してみましょう：
Prelude> seq ( undefined >>= return :: IO () ) "hello, world"
"hello, world"
Prelude> seq ( undefined :: IO () ) "hello, world"
*** Exception: Prelude.undefined
したがって、はとundefined >>= return同じでundefinedはIOないため、モナドではありません。Maybe一方、モナドに対して同じことを試してみると、次のようになります。
Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
Prelude> seq ( undefined :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
2つの式は同一であるためMaybe、この例ではモナドであることが除外されていません。
誰かがの使用に依存しない例を持っているseqか、undefined私はそれを見たいと思います。
m >>= return ≡ m
は壊れてます：
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: IO ()
メモリが乱雑になり、計算時間が長くなりますが、
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: Maybe ()
ではない。
AFAIRには、この問題を解決するモナド変換子があります。私が正しく推測するならば、それは共密度モナド変換子です。