Applicative documentation: Identity law implies Homomorphism law
I recently made a post about "Ways of failing to be Applicative": https://www.reddit.com/r/haskell/comments/1c8nehp/ways_of_failing_to_be_applicative/
One of the conclusions from that, was that there is a logical dependency between the Identity and Homomorphism Applicative laws. Namely, that Identity implies Homomorphism.
This should be included in the Applicative documentation.
Using parametricity, you can derive
(f <$>) == (pure f <*>)
from the Identity law. I feel like you can use the same idea to derive the homomorphism law from the identity and fmap laws, so that would explain why you haven’t found a case with valid Identity but invalid Homomorphism laws.
You're right. The free theorem for
pure :: a -> f a
isfmap f . pure = pure . f
, getting us to:fmap f (pure x) = pure (f x)
. Now we just needamap f := (pure f <*>) = fmap f
and we'll have homomorphism.amap
has the free theorem:g . h = k . f ==> fmap g . amap h = amap k . fmap f
. Takingg, k = id
andh = f
we obtainamap f = amap id . fmap f
. Identity then gives usamap id = id
.QED: given parameticity and the Functor laws, identity implies homomorphism.