haskell - 违反结合律的不正确 monad 的例子是什么？

Question

背景语境:

从数学上讲，我可以看到需要关联性以保持简单而不依赖顺序。我遇到的示例 monad 的所有实现(博客、书籍等)似乎总是有效。似乎只是简单地使用 map, flatMap (Scala) 或 fmap, >>= (Haskell) 就可以使事情成为一个有效的 monad。

据我所知，这并不完全正确，但无法通过失败案例提出一个反例来说明法律的“必要性”。

Wadler's paper提到了不正确实现的可能性:

Haskell Wiki提到以下内容:

The third law is a kind of associativity law for >>=. Obeying the three laws ensures that the semantics of the do-notation using the monad will be consistent.

Any type constructor with return and bind operators that satisfy the three monad laws is a monad. In Haskell, the compiler does not check that the laws hold for every instance of the Monad class. It is up to the programmer to ensure that any Monad instance they create satisfies the monad laws.

问题:

1. 看起来正确但破坏了关联性的不正确 monad 实现的示例是什么？
2. 这对 do 符号有何影响？
3. 如何验证 monad 实现的正确性？我们是否需要为每个新的 monad 编写测试用例，或者可以编写一个通用的测试用例来检查任何 monad 实现是否正确？

Answer 1

这是一个结合性失败的非 monad 示例:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad

newtype ListIO a = L { runListIO :: IO [a] }
  deriving Functor

instance Applicative ListIO where
   pure x = L $ return [x]
   (<*>) = ap

instance Monad ListIO where
   (L m) >>= f = L $ do
      xs <- m
      concat <$> mapM (runListIO . f) xs

如果满足结合性，这两个 do block 将是等价的

act1 :: ListIO Int
act1 = do
   L (pure [1,2,3])
   do L (putStr "a" >> return [10])
      L (putStr "b" >> return [7])

act2 :: ListIO Int
act2 = do
   do L (pure [1,2,3])
      L (putStr "a" >> return [10])
   L (putStr "b" >> return [7])

但是，运行操作会产生不同的输出:

main :: IO ()
main = do
   runListIO act1 -- ababab
   putStrLn ""
   runListIO act2 -- aaabbb
   return ()

总的来说，结合律的验证可能很困难。当然，可以编写测试，但确保关联性的理想方法是编写定律的数学证明。在某些情况下，等式推理足以证明结合性。有时候，我们也需要归纳。