从Applicative和Monad证明序列定义的等效性

Question

我该如何正确证明

sequenceA :: (Traversable t, Applicative f) => t (f a) -> f (t a)
sequenceA []     = pure []
sequenceA (x:xs) = pure (:) <*> x <*> sequenceA xs

与monad输入基本相同，

sequenceA' :: Monad m => [m a] -> m [a]
sequenceA' [] = return [] 
sequenceA' (x:xs) = do 
                    x'  <- x 
                    xs' <- sequenceA' xs 
                    return (x':xs')

尽管约束Applicative和Monad过程的。

Answer 1

这是一个证明草图：

1. 显示

   do
       x'  <- x
       xs' <- sequenceA' xs
       return (x' : xs')
   

   相当于

   do
       f1  <- do
           cons <- return (:)
           x'  <- x
           return (cons x')
       xs' <- sequenceA' xs
       return (f1 xs')
   

   这涉及到废止（和废止）do表示法并应用Monad法则。

2. 使用以下定义ap：

   ap m1 m2 = do { x1 <- m1; x2 <- m2; return (x1 x2) }
   

   把上面的代码变成

   do
       f1  <- return (:) `ap` x
       xs' <- sequenceA' xs
       return (f1 xs')
   

   然后

   return (:) `ap` x `ap` sequenceA' xs
   

3. 现在你有

   sequenceA' [] = return [] 
   sequenceA' (x:xs) = return (:) `ap` x `ap` sequenceA' xs
   

   假定pure和<*>本质上是一样的return，并`ap`分别就大功告成了。

   后一个属性在应用文档中也有说明：

   如果f也是Monad，则应满足

   • pure = return

   • (<*>) = ap

Answer 2

自GHC 7.10中实施Functor-Applicative-Monad建议以来，Applicative是Monad的超类。因此，即使您的两个函数不能严格等效，由于sequenceA的域包括sequenceA'的域，我们也可以看看在此公共域（Monad类型类）中发生了什么。

本文所示脱糖的一个有趣的示范do符号来应用性和仿函数操作（<$>，pure和<*>）。如果左箭头（<-）右侧的表达式不相互依赖（如您的问题一样），则您始终可以使用应用运算，从而表明您的假设是正确的（对于Monad域）。

还可以看看ApplicativeDo语言扩展提案，其中包含一个与您的示例类似的示例：

do
  x <- a
  y <- b
  return (f x y)

转换为：

(\x y -> f x y) <$> a <*> b

代f了(:)，我们得到：

do
  x <- a
  y <- b
  return (x : y)

...翻译成...

(\x y -> x : y) <$> a <*> b
--And by eta reduction
(:) <$> a <*> b
--Which is equivalent to the code in your question (albeit more general):
pure (:) <*> a <*> b

另外，您可以通过使用ApplicativeDo语言扩展并遵循对SO问题“ haskell-Monads的Desugaring do-notation”的回答，使GHC的desugarer工作。我将把这项练习留给您（老实说，这超出了我的能力！）。