What does the Naturality law for Traversables mean?

Question

The Naturality law states that:

t . traverse f == traverse (t . f) -- for every applicative transformer t

Now for the RHS of the law, if f has the type Applicative a => x -> a y, then t has to be of the type (Applicative a, Applicative b) => a y -> b y, due to the function composition.

For the LHS, traverse f has the type (Applicative a, Traversable c) => c x -> a (c y). But since traverse f is composed with t . traverse f, t has to be of the type (c x -> a (c y)) -> b y.

Now, for the LHS, t has the type a (c y) -> b y, but from the RHS it has the type a y -> b y. How is the law sound from a type perspective?

Edit: Fixed the type t in LHS

Answer 1

I think what you have missed is that t is supposed to be a natural transformation (which also probably must have some structure-preserving properties). Natural transformations are quantified, like so:

t :: forall z. a z -> b z   -- "t is an N.T. from a ~> b"

On the right we instantiate it at y, to get t :: a y -> b y; on the left we instantiate it at c y to get a (c y) -> b (c y). The way I think of it is that a natural transformation changes the outer layer, no matter what is inside. Naturality laws always talk about relationships between the different ways something is instantiated.

t                :: forall z. a z -> b z

f                :: x -> a y
t                :: a y -> b y           -- instantiated at y
t . f            :: x -> b y
traverse (t . f) :: c x -> b (c y)

traverse f       :: c x -> a (c y)
t                :: a (c y) -> b (c y)   -- instantiated at (c y)
t . traverse f   :: c x -> b (c y)