[Haskell-cafe] A "commutative diagram" conjecture about applicative
functors
Robin Green
greenrd at greenrd.org
Sun Dec 30 19:00:46 EST 2007
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)"
McBride and Patterson give four laws for applicative functors in their
paper "Functional Pearl: Applicative programming with effects". Can
these laws be used to prove this conjecture for all applicative functors
satisfying those laws?
--
Robin
P.S. I realise this might not look like a "commutative diagram
conjecture", but as I said, I've made it more specific - my actual
conjecture is more general, but hopefully if I can understand how to
prove the specific one, I'll be able to prove my real one in short
order.
More information about the Haskell-Cafe
mailing list