Clarify relationship between Functor and Applicative
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. See http://hpaste.org/44315/applicative_implies_functor. -- 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.''
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?
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.''
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.''
And this means that pure id <*> x = x iff pure f <*> x = fmap f x ie. the fmap compatibility condition is equivalent to the identity applicative law. On Fri, 25 Feb 2011, roconnor@theorem.ca wrote:
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.''
On Fri, Feb 25, 2011 at 5:42 PM, Ross Paterson
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?
Given fmap id = id, the uniqueness of fmap for a given type follows trivially from the free theorem. -Edward Kmett
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.
Thanks, I've made this change.
participants (3)
-
Edward Kmett -
roconnor＠theorem.ca -
Ross Paterson