A "commutative diagram" conjecture about applicative functors
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.
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
Twan van Laarhoven wrote:
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:
good! I was still confused whether 'second' was necessarily in the (,) arrow (it is, here). So I used GHCi (6.8.2), and seemed to discover a GHC bug afterwards? Prelude Control.Arrow Control.Applicative
:t \f x -> fmap second f <*> fmap ((,) (0::Int)) x \f x -> fmap second f <*> fmap ((,) (0::Int)) x :: (Applicative f) => f (b -> c) -> f b -> f (Int, c)
:t \f x -> fmap ((,) (0::Int)) (f <*> x) \f x -> fmap ((,) (0::Int)) (f <*> x) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
Unfortunately, I get puzzling type errors if I annotate either one of them with their type (e.g. (Applicative f) => f (a -> b) -> f a -> f (Int, b) ) in an expression. The very answer doesn't seem to typecheck.
:t \f x -> fmap ((,) (0::Int)) (f <*> x) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
<interactive>:1:14: Couldn't match expected type `f a1 -> f (Int, a)' against inferred type `(Int, a11)' Probable cause: `(,)' is applied to too many arguments In the first argument of `fmap', namely `((,) (0 :: Int))' In the expression: fmap ((,) (0 :: Int)) (f <*> x) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
:t \f x -> fmap second f <*> fmap ((,) (0::Int)) x :: (Applicative f) => f (b -> c) -> f b -> f (Int, c)
<interactive>:1:13: Couldn't match expected type `f b -> f (Int, c)' against inferred type `(d, c1)' Probable cause: `second' is applied to too many arguments In the first argument of `fmap', namely `second' In the first argument of `(<*>)', namely `fmap second f' Of course if I leave out ":t" and leave out all type signatures then it complains that it needs monomorphism, which is fair, but...
\f x -> fmap second f <*> fmap ((,) (0::Int)) x
<interactive>:1:8: Ambiguous type variable `f' in the constraint: `Applicative f' arising from a use of `<*>' at <interactive>:1:8-46 Probable fix: add a type signature that fixes these type variable(s) Isaac
Isaac Dupree wrote:
Unfortunately, I get puzzling type errors if I annotate either one of them with their type (e.g. (Applicative f) => f (a -> b) -> f a -> f (Int, b) ) in an expression. The very answer doesn't seem to typecheck.
:t \f x -> fmap ((,) (0::Int)) (f <*> x) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
Here the type annotation applies to the *body* of the lambda abstraction, adding parentheses around the whole thing solve your problem.
:t (\f x -> fmap ((,) (0::Int)) (f <*> x)) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
Aside from the fact that ghci has some trouble formating the output. Twan
Twan van Laarhoven wrote:
Isaac Dupree wrote:
Unfortunately, I get puzzling type errors if I annotate either one of them with their type (e.g. (Applicative f) => f (a -> b) -> f a -> f (Int, b) ) in an expression. The very answer doesn't seem to typecheck.
:t \f x -> fmap ((,) (0::Int)) (f <*> x) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
Here the type annotation applies to the *body* of the lambda abstraction, adding parentheses around the whole thing solve your problem.
:t (\f x -> fmap ((,) (0::Int)) (f <*> x)) :: (Applicative f) => f (a1 -> a) -> f a1 -> f (Int, a)
Aside from the fact that ghci has some trouble formating the output.
thank you, oops, how annoying. I wonder if GHCi should output parentheses to make its :type result be a valid expression... Isaac
participants (3)
-
Isaac Dupree -
Robin Green -
Twan van Laarhoven