haskell - 我如何证明 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

请注意，这个证明实际上并不是必需的，因为所讨论的结果确实是一个自由定理。见 Reid Barton's answer .
我相信这会做到:

traverse f . fmap g -- LHS

由 fmap/traverse法律，

traverse f . runIdentity . traverse (Identity . g)

由于 fmap对于 Identity实际上是 id ,

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

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

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 的唯一性.