¿Qué significa la ley de Naturalidad para Traversables?

La ley de naturalidad establece que:

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

Ahora para el RHS de la ley, si f tiene el tipo Applicative a => x -> a y, entonces t tiene que ser del tipo (Applicative a, Applicative b) => a y -> b y, debido a la composición de la función.

Para el LHS, el recorrido f tiene el tipo (Applicative a, Traversable c) => c x -> a (c y). Pero dado que f transversal está compuesto por t. transversal f, t tiene que ser del tipo (cx -> a (cy)) -> b y.

Ahora, para el LHS, t tiene el tipo a (cy) -> by, pero desde el RHS tiene el tipo ay -> b y. ¿Cómo suena la ley desde una perspectiva tipo?

Editar: se corrigió el tipo t en LHS

Creo que lo que te has perdido es que tse supone que es una transformación natural (que probablemente también debe tener algunas propiedades de preservación de la estructura). Las transformaciones naturales se cuantifican así:

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

A la derecha lo instanciamos en y, para obtener t :: a y -> b y; a la izquierda lo instanciamos c ypara obtener a (c y) -> b (c y). La forma en que pienso es que una transformación natural cambia la capa externa, sin importar lo que haya adentro. Las leyes de naturalidad siempre hablan de las relaciones entre las diferentes formas en que se instancia algo.

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)