[Haskell-cafe] A "commutative diagram" conjecture about
applicative functors
Twan van Laarhoven
twanvl at gmail.com
Sun Dec 30 21:52:01 EST 2007
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
More information about the Haskell-Cafe
mailing list