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

Answer 2

Since the Functor-Applicative-Monad proposal, implemented in GHC 7.10, Applicative is a superclass of Monad. So even though your two functions can't be strictly equivalent, since sequenceA's domain includes sequenceA''s domain, we can look at what happens in this common domain (the Monad typeclass).

This paper shows an interesting demonstration of desugaring do notation to applicative and functor operations (<$>, pure and <*>). If the expressions on the right hand side of your left-pointing arrows (<-) don't depend on each other, as is the case in your question, you can always use applicative operations, and therefore show that your hypothesis is correct (for the Monad domain).

Also have a look at the ApplicativeDo language extension proposal, which contains an example that's just like yours:

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

which translates to:

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

Substituting f for (:), we get:

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

... which translates to...

(\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

Alternatively, you can make GHC's desugarer work for you by using the ApplicativeDo language extension and by following this answer to the SO question "haskell - Desugaring do-notation for Monads". I'll leave this exercise up to you (as it honestly goes beyond my capacities!).