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

我怎样才能正确地证明这一点

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 and Monad当然。

这是一个证明草图：

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符号并应用单子定律 https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Monad.html#t:Monad.

2. Use the 的定义ap https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#ap:

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

   将上面的代码变成

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

   and then

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

3. 现在你有

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

   假使，假设pure and <*>本质上是相同的return and `ap`分别，然后就完成了。

   后一个属性也在应用文档 https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Applicative.html#t:Applicative:

   If f也是一个Monad，应该满足

   • pure = return

   • (<*>) = ap