可遍历的自然定律是什么意思？

Question

自然法规定：

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

现在对于法律的RHS，如果f具有type Applicative a => x -> a y，则(Applicative a, Applicative b) => a y -> b y由于函数组成，t必须是type 。

对于LHS，导线f的类型为(Applicative a, Traversable c) => c x -> a (c y)。但是由于遍历f由t组成。遍历f，t必须是（cx-> a（cy））-> b y类型。

现在，对于LHS，t的类型为a（cy）-> by，但是在RHS中，其类型为ay-> b y。从类型的角度看法律的声音如何？

编辑：修复了LHS中的类型t

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"

在右边，我们将它实例化为y得到t :: a y -> b y; 在左侧，我们实例化c y以获得a (c y) -> b (c y)。我的想法是，无论内部是什么，自然变换都会改变外层。自然法则总是谈论实例化事物的不同方式之间的关系。

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)