一个简单的例子表明IO不能满足monad法则？
我已经提到IO不符合单子法，但是我没有find一个简单的例子来表明这一点。 有人知道一个例子吗？ 谢谢。
编辑：正如ertes和nm指出的，使用seq有点不合法，因为它可以使任何monad失败的法律（结合undefined ）。 由于undefined可能被视为非终止计算，所以使用它是完全正确的。
所以修改后的问题是： 有人知道一个例子，说明IO不能满足单子法则，不使用seq ？ （或者，如果seq不被允许，那么certificateIO确实符合法律？）
tl; dr先行： 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 ms of (# new_s, a #) -> unIO (ka) new_s thenIO :: IO a -> IO b -> IO b thenIO (IO m) k = IO $ \ s -> case ms of (# new_s, _ #) -> unIO k new_s unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #)) unIO (IO a) = a
它被实现为（严格）状态monad。 所以任何违反IO的monad法则，都是由Control.Monad.State[.Strict] 。
让我们看看单子法，看看IO发生了什么：
return x >>= f ≡ fx: return x >>= f = IO $ \s -> case (\t -> (# t, x #)) s of (# new_s, a #) -> unIO (fa) new_s = IO $ \s -> case (# s, x #) of (# new_s, a #) -> unIO (fa) new_s = IO $ \s -> unIO (fx) s
忽略newtype包装，这意味着return x >>= f变成\s -> (fx) s 。 （可能）与fx区分的唯一方法是seq 。 （如果fx ≡ undefined ， seq只能区分它。）
m >>= return ≡ m: (IO k) >>= return = IO $ \s -> case ks of (# new_s, a #) -> unIO (return a) new_s = IO $ \s -> case ks of (# new_s, a #) -> (\t -> (# t, a #)) new_s = IO $ \s -> case ks of (# new_s, a #) -> (# new_s, a #) = IO $ \s -> ks
再次忽略newtype包装， k被replace为\s -> ks ，它只能被seq区分，并且只有在k ≡ undefined 。
m >>= (\x -> gx >>= h) ≡ (m >>= g) >>= h: (IO k) >>= (\x -> gx >>= h) = IO $ \s -> case ks of (# new_s, a #) -> unIO ((\x -> gx >>= h) a) new_s = IO $ \s -> case ks of (# new_s, a #) -> unIO (ga >>= h) new_s = IO $ \s -> case ks of (# new_s, a #) -> (\t -> case unIO (ga) t of (# new_t, b #) -> unIO (hb) new_t) new_s = IO $ \s -> case ks of (# new_s, a #) -> case unIO (ga) new_s of (# new_t, b #) -> unIO (hb) new_t ((IO k) >>= g) >>= h = IO $ \s -> case (\t -> case kt of (# new_s, a #) -> unIO (ga) new_s) s of (# new_t, b #) -> unIO (hb) new_t = IO $ \s -> case (case ks of (# new_s, a #) -> unIO (ga) new_s) of (# new_t, b #) -> unIO (hb) new_t
现在，我们一般都有
case (case e of case e of pat1 -> ex1) of ≡ pat1 -> case ex1 of pat2 -> ex2 pat2 -> ex2
根据公式3.17.3（a）中的语言报告，所以这个法则不仅保持模数。
总结一下， IO满足monad定律，除了seq可以区分undefined和\s -> undefined s 。 这同样适用于State[T] ， Reader[T] ， (->) a和包装函数types的其他monad。
Haskell中的所有monad都是monad，如果你排除怪异的seq组合。 IO也是如此。 由于seq实际上并不是一个普通的函数，而是涉及到魔法，所以你必须排除它来检查单子法则，因为你必须排除unsafePerformIO 。 使用seq你可以certificate所有monad错误，如下所示。
在克莱斯里范畴中，单子产生， return是身份态射，而(<=<)是组合。 所以return必须是(<=<)的标识：
return <=< x = x
甚至使用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
单子法之一是这样的
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不是monad。 如果我们为Maybe monad尝试同样的事情，另一方面：
Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world" *** Exception: Prelude.undefined Prelude> seq ( undefined :: Maybe () ) "hello, world" *** Exception: Prelude.undefined
这两个expression式是相同的 – 所以这个例子Maybe并不排除是一个monad。
如果有人有一个不依赖于seq的使用或undefined的例子，我会有兴趣看到它。
m >>= return ≡ m
被打破：
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: IO ()
杂乱的记忆和增加计算时间
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: Maybe ()
才不是。
AFAIR有一个Monad Transformer解决了这个问题。 如果我猜对了，那就是Codensity Monad Transformer。
