How can I show that traverse interacts sensibly with fmap?

Question

It seems intuitively obvious that the following law should hold:

traverse f . fmap g = traverse (f . g)

The only Traversable law that seems to apply directly is

fmap g = runIdentity . traverse (Identity . g)

That changes the problem to

traverse f . runIdentity . traverse (Identity . g)

The only law that seems to have vaguely the right shape to apply to this is the naturality law. That, however, is about applicative transformations, and I don't see any of those around.

Unless I'm missing something, the only thing left is a parametricity proof, and I've not yet gotten a clue about how to write those.

Answer 1

Note that this proof isn't actually necessary, as the result in question is indeed a free theorem. See Reid Barton's answer.

I believe this will do:

traverse f . fmap g -- LHS

By the fmap/traverse law,

traverse f . runIdentity . traverse (Identity . g)

Since fmap for Identity is effectively id,

runIdentity . fmap (traverse f) . traverse (Identity . g)

The Compose law offers a way to collapse two traversals into one, but we must first introduce Compose using getCompose . Compose = id.

runIdentity . getCompose . Compose . fmap (traverse f) . traverse (Identity . g)
-- Composition law:
runIdentity . getCompose . traverse (Compose . fmap f . Identity . g)

Again using the Identity fmap,

runIdentity . getCompose . traverse (Compose . Identity . f . g)

Compose . Identity is an applicative transformation, so by naturality,

runIdentity . getCompose . Compose . Identity . traverse (f . g)

Collapsing inverses,

traverse (f . g) -- RHS

Invoked laws and corollaries, for the sake of completeness:

-- Composition:
traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f
-- Naturality:
t . traverse f = traverse (t . f) -- for every applicative transformation t
-- `fmap` as traversal:
fmap g = runIdentity . traverse (Identity . g)

The latter fact follows from the identity law, traverse Identity = Identity, plus the uniqueness of fmap.

Answer 2

According to lambdabot it is a free theorem (parametricity).

In response to @free traverse :: (a -> F b) -> T a -> F (T b), lamdabot produces

$map_F g . h = k . f => $map_F ($map_T g) . traverse h = traverse k . $map_T f

Set g = id so that h = k . f. Then the conclusion becomes

traverse (k . f) = traverse k . fmap f