Clarify relationship between Functor and Applicative

roconnor at theorem.ca roconnor at theorem.ca
Sat Feb 26 01:58:44 CET 2011


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 at 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 at theorem.ca wrote:
>
>> On Fri, 25 Feb 2011, Ross Paterson wrote:
>> 
>>> On Fri, Feb 25, 2011 at 05:34:18PM -0500, roconnor at 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.
>>>> 
>>>> See <http://hpaste.org/44315/applicative_implies_functor>.
>>> 
>>> 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.''



More information about the Libraries mailing list