Actually this means once you prove the identity applicative law pure id <*> x = x then it entails that pure f <*> x = fmap f x On Fri, 25 Feb 2011, roconnor@theorem.ca wrote:
On Fri, 25 Feb 2011, Ross Paterson wrote:
On Fri, Feb 25, 2011 at 05:34:18PM -0500, roconnor@theorem.ca wrote:
In the applicative documentation, it says for an Applicative functor f:
The Functor instance should satisfy
fmap f x = pure f <*> x
I think the documentation should be clarified that this does not need to be checked because it is a consequence of the other applicative laws.
Do you have a proof that Functor instances are uniquely determined?
Suppose we have a functor f and another function
foo :: (a -> b) -> f a -> f b
Then as a consequence of the free theorem for foo, for any f :: a -> b and any g :: b -> c.
foo (g . f) = fmap g . foo f
In particular, if foo id = id, then
foo g = foo (g . id) = fmap g . foo id = fmap g . id = fmap g
-- Russell O'Connor http://r6.ca/ ``All talk about `theft,''' the general counsel of the American Graphophone Company wrote, ``is the merest claptrap, for there exists no property in ideas musical, literary or artistic, except as defined by statute.''