时间戳

首页 > 解决方案 > 违反结合律的不正确单子的例子是什么？

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

问题描述

背景背景：

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

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

Wadler 的论文提到了错误实现的可能性：

Wadler 的论文关联性片段

Haskell Wiki提到以下内容：

第三定律是 的一种结合律>>=。遵守这三个法则可以确保使用 monad 的 do-notation 的语义是一致的。

任何具有满足三个单子法则的返回和绑定运算符的类型构造函数都是单子。在 Haskell 中，编译器不会检查 Monad 类的每个实例是否适用这些定律。程序员有责任确保他们创建的任何 Monad 实例都满足 monad 法则。

问题）：

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

标签： haskellfunctional-programming

解决方案

这是一个关联性失败的非单子示例：

{-# 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块将是等价的

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

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

推荐阅读