Traversable的自然法则是什么意思？

Question

自然法规定：

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

现在对于定律的RHS，如果f有类型Applicative a => x -> a y，那么由于函数组成，t必须是(Applicative a, Applicative b) => a y -> b y类型。

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

现在，对于LHS，t的类型是a (c，y) -> b y，但是从RHS的角度，它的类型是a，y，->，b，从类型的角度来看，这个定律听起来怎么样？

编辑:修正了LHS中的类型t

Answer 1

我认为您忽略的是，t应该是一种自然转换(它可能还必须具有一些结构保持属性)。自然转换是量化的，如下所示：

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)