haskell - Traversables 的自然法则是什么意思？

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) .但是由于 traverse f 是由 t 组成的。遍历 f，t 必须是 (c x -> a (c y)) -> b y 类型。

现在，对于 LHS，t 的类型为 a (c y) -> b y，但在 RHS 中，它的类型为 a y -> b y。从类型的角度来看，法律听起来如何？

编辑:修复了 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)