Proving equivalence of sequence definitions from Applicative and Monad

Question

How can I properly prove that

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

is essentially the same to monad inputs as

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

In spite of the constraint Applicative and Monad of course.

Answer 1

Here's a proof sketch:

1. Show that

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

   is equivalent to

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

   This involves desugaring (and resugaring) do notation and applying the Monad laws.

2. Use the definition of ap:

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

   to turn the above code into

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

   and then

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

3. Now you have

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

   Assume that pure and <*> are essentially the same as return and `ap`, respectively, and you're done.

   This latter property is also stated in the Applicative documentation:

   If f is also a Monad, it should satisfy

   • pure = return

   • (<*>) = ap