我如何证明 traverse 与 fmap 的交互是合理的？

Question

从直觉上看，以下定律应该成立：

traverse f . fmap g = traverse (f . g)

似乎直接适用的唯一Traversable法律是

fmap g = runIdentity . traverse (Identity . g)

这样问题就变成了

traverse f . runIdentity . traverse (Identity . g)

唯一似乎具有适用于此的模糊正确形式的法律是自然法。然而，那是关于应用转换的，我没有看到任何类似的转换。

除非我遗漏了什么，否则唯一剩下的就是参数证明，我还不知道如何编写这些证明。

Answer 1

请注意，这个证明实际上并不是必需的，因为所讨论的结果确实是一个自由定理。见 .

我相信这样做：

traverse f . fmap g -- LHS

根据fmap/traverse定律，

traverse f . runIdentity . traverse (Identity . g)

因为 Identity 的 fmap 实际上是 id,

runIdentity . fmap (traverse f) . traverse (Identity . g)

Compose定律提供了一种将两个遍历合并为一个的方法，但我们必须首先使用getCompose . Compose = id引入Compose。

runIdentity . getCompose . Compose . fmap (traverse f) . traverse (Identity . g)
-- Composition law:
runIdentity . getCompose . traverse (Compose . fmap f . Identity . g)

再次使用 Identity fmap,

runIdentity . getCompose . traverse (Compose . Identity . f . g)

Compose . Identity 是一个应用转换，所以很自然地，

runIdentity . getCompose . Compose . Identity . traverse (f . g)

倒塌的逆，

traverse (f . g) -- RHS

为了完整起见，引用了定律和推论：

-- Composition:
traverse (Compose . fmap g . f) = Compose . fmap (traverse g) . traverse f
-- Naturality:
t . traverse f = traverse (t . f) -- for every applicative transformation t
-- `fmap` as traversal:
fmap g = runIdentity . traverse (Identity . g)

后一个事实来自恒等律 traverse Identity = Identity，加上 fmap 的唯一性。

Answer 2

根据 lambdabot，这是一个自由定理（参数化）。

响应@free traverse :: (a -> F b) -> T a -> F (T b)，lamdabot 产生

$map_F g . h = k . f => $map_F ($map_T g) . traverse h = traverse k . $map_T f

设置g = id使得h = k . f。那么结论就变成了

traverse (k . f) = traverse k . fmap f

我如何证明 traverse 与 fmap 的交互是合理的？

How can I show that traverse interacts sensibly with fmap?

haskell

traversal