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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
