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.

但是,这个三重3也与三重或三重相同.

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

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

Answer 1

这种等同性是Monad法则中的第三种,并且与关联性有关,因此毫不奇怪triple2并且triple3是等同的.在所有 (->) rmonad遵守monad法律之后.第三个monad法律规定

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

你的情况,你有m = id,f = \n -> (n+)和g = \d -> (d+).为了证明为什么这个法律成立,我们需要看看这个monad的定义(>>=).从这个链接,我们得到了

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

为了验证具有此定义的第三个monad法则(>>=),我们将使用一些规则:

• 定义(>>=): f >>= k ? \ r -> k (f r) r
• Beta转换: 基本上是功能应用
• 功能调整: (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 (>>=))