如何顯示遍歷與fmap的合理交互？

Question

似乎直觀明顯，下面的法律應持有：

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

唯一Traversable法律，似乎申請是直接

fmap g = runIdentity . traverse (Identity . g) 

這改變了問題

traverse f . runIdentity . traverse (Identity . g) 

似乎有隱約適用於此的正確形狀的唯一法律是th自然法則。然而，這是關於應用性轉變，我沒有看到其中的任何轉變。

除非我遺漏了一些東西，剩下的唯一東西就是參數證明，而且我還沒有弄清楚如何編寫這些東西。

Answer 1

請注意，這個證明實際上並非必要，因爲問題的結果確實是一個自由定理。見裏德巴頓的答案。

我相信，這將做到：

traverse f . fmap g -- LHS 

由fmap/traverse法律，

traverse f . runIdentity . traverse (Identity . g) 

由於fmap爲Identity實際上是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) 

再次使用Identityfmap，

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