一个简单的例子表明IO不符合monad法则？

Question

我已经看到提到IO不满足monad定律,但我没有找到一个简单的例子来证明这一点.有人知道一个例子吗？谢谢.

编辑:正如ertes和nm指出的那样,使用seq有点非法,因为它可以使任何monad失败的法律(结合undefined).由于undefined可以将其视为非终止计算,因此使用它完全没问题.

所以修改后的问题是:任何人都知道一个例子表明IO未能满足monad法则,而不使用seq？(或者,IO如果seq不允许,可能会出现符合法律规定的证据？)

Answer 1

如果排除奇怪的seq组合子,Haskell中的所有monad都只是monad .这也是如此IO.由于seq实际上并不是常规函数,而是涉及魔法,因此必须将其排除在检查monad定律之外,原因与您必须排除相同unsafePerformIO.使用seq你可以证明所有monad错误,如下所示.

在Kleisli类别中monad引起的,return是身份态射和(<=<)构成.所以return必须是一个身份(<=<):

return <=< x = x

使用seq偶数身份和可能无法成为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

Answer 2

tl; dr beforefront:seq是唯一的方法.

由于IO标准没有规定实施,我们只能看具体实施.如果我们看一下GHC的实现,因为它可以从源头获得(可能是某些幕后特殊处理会IO引入违反monad法律的行为,但我不知道有任何此类事件发生),

-- 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

它被实现为(严格)状态monad.因此,任何违反monad法律的行为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满足monad法则,除了seq可以区分undefined和的事实\s -> undefined s.这同样适用于State[T],Reader[T],(->) a,和任何其它单子包裹的函数类型.

Answer 3

其中一个monad法则是

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    

这两个表达式是相同的 - 因此Maybe不排除在这个例子中成为monad.

如果有人有一个不依赖于使用的例子,seq或者undefined我有兴趣看到它.