我见过提到IO不满足单子定律，但我没有找到一个简单的例子来说明这一点。有人知道一个例子吗？谢谢。
编辑：正如ertes和 nm 所指出的， usingseq有点非法，因为它可以使任何 monad 违反法律（结合undefined）。由于undefined可能被视为非终止计算，因此使用它非常好。
所以修改后的问题是：任何人都知道一个IO不满足单子定律的例子，没有使用seq？（或者如果不允许，也许是一个IO确实满足法律的证明？）seq
问问题
5187 次
4 回答
43
seq如果你排除了奇怪的组合子，Haskell 中的所有单子都是单子。对于IO. 由于seq它实际上不是常规函数，而是涉及魔法，因此您必须将其排除在检查单子定律之外，原因与您必须排除unsafePerformIO. 使用seqyou 可以证明所有单子都是错误的，如下所示。
在 Kleisli 范畴中，monad 产生，return是恒等态射并且(<=<)是组合。所以return必须是一个身份(<=<)：
return <=< x = x
即使使用seqIdentity 和 Maybe 也不能成为 monad：
seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined :: a -> Identity b) () = undefined
seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined :: a -> Maybe b) () = undefined
于 2012-09-27T11:33:12.093 回答
26
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].
让我们看看 monad 法则，看看会发生什么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满足单子定律，除了seq可以区分undefined和\s -> undefined s. 这同样适用于State[T], Reader[T],(->) a和任何其他包装函数类型的 monad。
于 2012-09-27T14:14:08.647 回答
8
单子定律之一是
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另一方面，如果我们对 monad 尝试相同的操作：
Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
Prelude> seq ( undefined :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
这两个表达式是相同的 - 所以Maybe这个例子不排除是一个单子。
如果有人有一个不依赖于使用的例子，seq或者undefined我有兴趣看到它。
于 2012-09-27T09:14:25.947 回答
4
m >>= return ≡ m
被打破：
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: IO ()
使内存混乱并增加计算时间，而
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: Maybe ()
才不是。
AFAIR 有一个 Monad Transformer 可以解决这个问题；如果我猜对了，它就是 Codensity Monad Transformer。
于 2012-10-15T18:00:17.433 回答