如何显示遍历与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的回答.

我相信这会做:

traverse f . fmap g -- LHS

根据fmap/traverse法律,

traverse f . runIdentity . traverse (Identity . g)

由于fmap为Identity是有效的id,

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

该Compose法提供了一条途径崩溃两次遍历到一个,但我们必须先介绍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.