Haskell 中 (M a >>= f) >>= g 和 M a >>= (f >>= g) 的等价性

Question

我有两个等效的 Haskell 函数。

triple :: Int -> Int
triple = do
  n <- id
  d <- (n+)
  (d+)

triple2 :: Int -> Int  
triple2 = (id >>= (\n -> (n+))) >>= (\d -> (d+))    

>>=的签名是M a -> (a -> M b) -> M b，所以括号用来强调((Ma >>= f) >>= f2)或M b >> f2的关系。

不过，这个triple3 也是和triple 或triple2 等价的函数。

triple3 :: Int -> Int  
triple3 = id >>= (\n -> (n+) >>= (\d -> (d+)))

这些等价背后的逻辑是什么？

Answer 1

这种等价是Monad Laws 的第三个，并且与关联性有关，因此triple2 和triple3 是等价的也就不足为奇了。毕竟(->) r monad 遵守单子法则。第三个单子定律指出

(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

在您的情况下，您有 m = id、f = \n -> (n+) 和 g = \d -> (d+)。为了证明这个定律为什么成立，我们需要看看definition of (>>=) for this monad。从这个链接，我们得到了

f >>= k = \ r -> k (f r) r

要使用 (>>=) 的定义验证第三个单子定律，我们将使用几个规则：

• (>>=) 的定义： f >>= k ≡ \ r -> k (f r) r
• Beta 转换： basically function application
• 函数柯里化： (f x) y ≡ f x y

现在证明：

(m >>= f) >>= g
  ≡ (\ r1 -> f (m r1) r1) >>= g                             (Definition of (>>=))
  ≡ \ r2 -> g ((\ r1 -> f (m r1) r1) r2) r2                 (Definition of (>>=))
  ≡ \ r2 -> g (f (m r2) r2) r2                              (Beta transformation)
  ≡ \ r2 -> g ((f (m r2)) r2) r2                            (Function currying)
  ≡ \ r2 -> (\ r1 -> g ((f (m r2)) r1) r1) r2               (Beta transformation)
  ≡ \ r2 -> ((\ x -> (\ r1 -> g ((f x) r1) r1)) (m r2)) r2  (Beta transformation)
  ≡ \ r2 -> ((\ x -> f x >>= g) (m r2)) r2                  (Definition of (>>=)) 
  ≡ \ r2 -> (\ x -> f x >>= g) (m r2) r2                    (Function currying) 
  ≡ m >>= (\ x -> f x >>= g)                                (Definition of (>>=))