list - 从 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

这是一个证明草图:

显示

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 laws .

使用 definition of 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

现在你有

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

假设 pure和 <*>与 return 基本相同和 `ap` ，分别，你就完成了。

Applicative documentation 中也说明了后一个属性。 :

If f is also a Monad, it should satisfy

• pure = return

• (<*>) = ap