Relation between `<*>` and `<$>`

Question

According to the Haskell Wikibook, the following relation between <$> and <*> hold:

f <$> x = pure f <*> x

They claim that one can prove this theorem as a consequence of the functor and applicative laws.

I do not see how to prove this. Any help is appreciated.

Answer 1

The Functor and Applicative Laws

Let's start with what the functor and applicative laws are. Let's take a look at these laws presented in the Haskell Wikibook.

fmap id = id                   -- 1st functor law
fmap (g . f) = fmap g . fmap f -- 2nd functor law

Now we should look at the applicative laws.

pure id <*> v = v                            -- Identity
pure f <*> pure x = pure (f x)               -- Homomorphism
u <*> pure y = pure ($ y) <*> u              -- Interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- Composition

The identity law says that applying the pure id morphism does nothing, exactly like with the plain id function.

The homomorphism law says that applying a "pure" function to a "pure" value is the same as applying the function to the value in the normal way and then using pure on the result. In a sense, that means pure preserves function application.

The interchange law says that applying a morphism to a "pure" value pure y is the same as applying pure ($ y) to the morphism. No surprises there - as we have seen in the higher order functions chapter, ($ y) is the function that supplies y as argument to another function.

The composition law says that pure (.) composes morphisms similarly to how (.) composes functions: applying the composed morphism pure (.) <*> u <*> v to w gives the same result as applying u to the result of applying v to w.

What we need to prove in order to prove the relation

Per @benjamin-hodgson

it suffices to show that fmap f x = pure f <*> x obeys the fmap id = id law as a consequence of the Applicative laws.

The reason that we only need to show that fmap f x = pure f <*> x obeys the fmap id = id law is because the second functor law can be shown to follow from the first law. I've provided a brief walk through this proof, but Edward Kmett has a more verbose version here

Section 3.5 of Wadler's Theorems for Free provides some work on the function map. Based on the idea of free theorems anything that is shown for a function holds for any other function of the same type signature. Since we know that the list is a functor the type of map :: (a -> b) -> [a] -> [b] is analogous to the type of fmap :: Functor f => (a -> b) -> [a] -> [b] which means that all of Wadler's work with map applies to fmap as well.

Wadler's conclusion about map leads to this theorem about fmap:

Given functions f, g, k, and h such that g . h = k . f then $map g . fmap h = fmap k . $map' f with $map being the "natural" mapping function for a given functor. The full proof of this theorem is a bit verbose, but Bartosz Milewski provides a good overview of it.

We will need two lemmas to show that the second functor law is a consequence of the first.

Lemma 1

Given fmap id = id --the first functor law then fmap f = $map f

fmap f = $map id . fmap f   --Because $map id = id
= fmap id . $map f          --Because of the free theorem with g = k = id and h = f
= $map f                    --Because of the first functor law

So fmap f = $map f and by extension fmap = $map

Lemma 2

f . g = id . (f . g) which is obvious given that id . v = v

Putting it all together

Given fmap id = id then fmap f . fmap g = fmap (f . g)

fmap f . fmap g = $map f . fmap g  --Because of lemma 1
= fmap id . $map (f . g)           --Because of the free theorem for fmap and lemma 2
= $map (f . g)                     --Because of the first functor law
= fmap (f . g)                     --Because $map = fmap

Therefore, if we can show that the first functor law holds, then the second will also hold.

Proving the relation

To show that we'll need the Applicative Identity law. Looking at the law we have pure id <*> v = v and from the equivalence we are trying to prove f <$> x = pure f <*> x. If we let x = id then the Applicative Identity law tells us that the right hand side of that equivalence is id x and the first Functor law tells us that the left hand side is id x.

f <$> x = pure f <*> x
id <$> x = pure id <*> x  -- Substitute id into the general form
id <$> x = x              -- Apply the applicative identity law
id x = x                  -- Apply the first functor law
x = x                     -- simplify id x to x

There we have shown that fmap f x = pure f <*> x obeys the first functor law by applying the applicative laws.