On Fri, Feb 25, 2011 at 5:42 PM, Ross Paterson <ross@soi.city.ac.uk> 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.
>
> See <http://hpaste.org/44315/applicative_implies_functor>.

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