一个简单的例子表明IO不能满足monad法则？ [英] A simple example showing that IO doesn't satisfy the monad laws?
问题描述
我已经看到 IO 不符合monad法则，但我没有找到一个简单的例子来说明这一点。有人知道一个例子吗？感谢。
编辑：由于 ertes a>和nm指出，使用 seq 有点违法，因为它可以使任何monad不遵守法律（与 undefined 结合）。由于 undefined 可能被视为非终止计算，因此使用它非常好。
IO 无法满足monad法则，而不使用 seq ？ （或者，如果 seq 不被允许，那么证明 tl; dr upfront： seq 是唯一的方法。 >
由于标准没有规定 IO 的实现，所以我们只能看具体的实现。如果我们看一下GHC的实现，就像它可以从源代码那里得到的那样（可能是因为 IO ）的一些幕后特殊处理引入了违反monad定律，但我不知道有这种情况发生），
- 在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
失败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 - > （＃new_s，a＃） - >的情况m s unIO（k a）new_s
thenIO :: IO a - > IO b - > IO b
thenIO（IO m）k = IO $ \\ s - > （＃new_s，_＃） - >的情况m s unio k new_s
unIO :: IO a - > （State＃RealWorld - >（＃State＃RealWorld，a＃））
unIO（IO a）= a
它被实现为（严格）状态monad。因此，任何违反monad法律的行为都是由 Control.Monad.State [.Strict] 产生的。
让我们看看单子定律，看看 IO 中会发生什么：
return x>> =f≡fx：
return x>> = f = 10 $ \ s - >
（＃new_s，a＃） - >的情况（\ t - >（＃t，x＃）） unIO（f a）new_s
= IO $ \s->
（＃new_s，a＃） - >的情况（＃s，x＃） unIO（f a）new_s
= IO $ \s-> unio（fx）s
忽略newtype包装，这意味着 return x> ;> = f 变成 \s - > （f x）s 。 （可能）区分 f x 的唯一方法是 seq 。 （ seq 只能在 fx≡undefined 中区分。）
m>> = return≡m：
（IO k）>> = return = 10 $ \ s - >
的情况k s（＃new_s，a＃） - > unIO（返回a）new_s
= IO $ \s - >
的情况k s（＃new_s，a＃） - > （\ t - >（＃t，a＃））new_s
= IO $ \s->
的情况k s（＃new_s，a＃） - > （＃new_s，a＃）
= IO $ \s - > ks
再次忽略newtype包装， k 由 \s - >替换ks ，它只能被 seq 区分，并且只有在 k≡undefined 时才可以区分。
m>> =（\ x - > gx> = h）≡（m> > = g）>> = h：
（IO k）>> =（\ x - > gx> = h）= 10 $ \\ s - >
的情况k s（＃new_s，a＃） - > （（\\ \\ x - > g x> = h）a）new_s
= 10 $ \\ s - >
的情况k s（＃new_s，a＃） - > unIO（g a>> = h）new_s
= IO $ \s->
的情况k s（＃new_s，a＃） - > （\\ new→new_t）new_s
= IO $ \ s - >的情况下的（$ a $ t $ b $）（＃new_t，b＃） - >
的情况k s（＃new_s，a＃） - >情况unIO（g a）new_s
（＃new_t，b＃） - > unIO（h b）new_t
（（IO k）>> = g）>> = h = 10 $ \\ s - > （＃new_t，b＃） - >
（＃new_s，a＃） - > unIO（g a）new_s）s的情况（\\ t→t→情况k t） unIO（h b）new_t
= IO $ \s - >
（＃new_s，a＃） - > unIO（g a）new_s）的情况（情况k s为
（＃new_t，b＃） - > unio（hb）new_t
现在，我们一般都有
≡pat1的情况（情况e为
pat1 - > ex1的情况e） - >案例ex1的
pat2 - > ex2 pat2 - > ex2
I've seen mentioned that IO doesn't satisfy the monad laws, but I didn't find a simple example showing that. Anybody knows an example? Thanks.
Edit: As ertes and n.m. pointed out, using seq is a bit illegal as it can make any monad fail the laws (combined with undefined). Since undefined may be viewed as a non-terminating computation, it's perfectly fine to use it.
So the revised question is: Anybody knows an example showing that IO fails to satisfy the monad laws, without using seq? (Or perhaps a proof that IO does satisfy the laws if seq is not allowed?)
tl;dr upfront: seq is the only way.
Since the implementation of IO is not prescribed by the standard, we can only look at specific implementations. If we look at GHC's implementation, as it is available from the source (it might be that some of the behind-the-scenes special treatment of IO introduces violations of the monad laws, but I'm not aware of any such occurrence),
-- 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
it's implemented as a (strict) state monad. So any violation of the monad laws IO makes, is also made by Control.Monad.State[.Strict].
Let's look at the monad laws and see what happens in 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
Ignoring the newtype wrapper, that means return x >>= f becomes \s -> (f x) s. The only way to (possibly) distinguish that from f x is seq. (And seq can only distinguish it if 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
ignoring the newtype wrapper again, k is replaced by \s -> k s, which again is only distinguishable by seq, and only if 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
Now, we generally have
case (case e of case e of
pat1 -> ex1) of ≡ pat1 -> case ex1 of
pat2 -> ex2 pat2 -> ex2
per equation 3.17.3.(a) of the language report, so this law holds not only modulo seq.
Summarising, IO satisfies the monad laws, except for the fact that seq can distinguish undefined and \s -> undefined s. The same holds for State[T], Reader[T], (->) a, and any other monads wrapping a function type.
这篇关于一个简单的例子表明IO不能满足monad法则？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
