[Haskell-cafe] A "commutative diagram" conjecture about applicative functors

[Twan van Laarhoven]

Robin Green wrote:

> I am proving various statements relating to applicative functors, using
> the Coq proof assistant (I am considering only Coq terms, which always
> terminate so you don't have to worry about _|_). However, I'm not sure
> how to go about proving a certain conjecture, which, translated back
> into Haskell and made more specific to make it easier to think about,
> looks like this (assuming Control.Applicative and Control.Arrow are
> imported):
> 
> "For all applicative functors:
> 
> \f x -> fmap second f <*> fmap ((,) (0::Int)) x
> 
> is equivalent to
> 
> \f x -> fmap ((,) (0::Int)) (f <*> x)"

Using the laws from the Control.Applicative haddock page, and some puzzling:

First of all, to avoid getting lost in parenthesis hell, define:
   let g = (,) (0::Int)
   let c = (.)

      fmap second f <*> fmap g x
  law: fmap*2
<=>  (pure second <*> f) <*> (pure g <*> x)
  law: composition
<=>  (pure c <*> (pure second <*> f)) <*> pure g <*> x
  law: interchange
<=>  pure ($g) (pure c <*> (pure second <*> f)) <*> x
  law: composition
<=>  pure c <$> pure ($g) <*> pure c <*> (pure second <*> f) <*> x
  law: homomorphism*2
<=>  pure (c ($g) c) <*> (pure second <*> f) <*> x
  simplify
<=>  pure (. g) <*> (pure second <*> f) <*> x
  law: composition
<=>  pure c <*> pure (. g) <*> pure second <*> f <*> x
  law: homomorphism*2
<=>  pure (c (. g) second) <*> f <*> x
  rewrite (unpl)
<=>  pure (\ d u -> (0,d u)) <*> f <*> x
  rewrite some more
<=>  pure (c g) <*> f <*> x
  law: homomorphism
<=>  pure c <*> pure g <*> f <*> x
  law: composition
<=>  pure g <*> (f <*> x)
  law: fmap
<=>  fmap g (f <*> x)

Q.E.D.

Twan