有趣的重复fmap [英] Fun with repeated fmap

问题描述

一般情况下， id 可以被实例化在类型（a - > b） - > a - > b 。

使用列表函子，我们有 fmap ::（a - > b） - > [a] - > [b] ，与 map 。

相同（（ - >）r）函子（来自 Control.Monad.Instances ）， fmap 是函数组合，因此我们可以实例化 fmap fmap fmap ::（a - > b） - > [[a]] - > [[b]] ，相当于（map。map）。

有趣的是， fmap 八次给了我们（map。map。map）！

因此，我们有

pre $ code> 0：id = id
1：fmap = map
3：fmap fmap fmap =（map。map）
8：fmap fmap fmap fmap fmap fmap fmap fmap =（map。map。map）


此模式是否继续？为什么/为什么不？是否有一个公式，我需要通过一个 n 时间嵌套列表映射一个函数多少个 fmap ？

我尝试编写一个测试脚本来搜索 n = 4 情况的解决方案，但GHC开始在40 fmap s。

解决方案

我无法解释为什么，循环的证明：

假设 k> = 2 和 fmap ^（ 4k）::（a - > b） - > F1 F2 F3 a - > F1 F2 F3 b ，其中 Fx 代表未知/任意 Functor 。 fmap ^ n 代表 fmap 应用于 n-1 fmap s，而不是 n - 折叠迭代。感应的开始可以通过手动查询或查询ghci。

  fmap ^（4k + 1）= fmap ^（4k）fmap 
 fmap ::（x  - > y） - > F4 x  - > F4 y 
  

与a - > b的统一产生 a = x - > y ， b = F4 x - > F4 y ，所以

  fmap ^（4k + 1）:: F1 F2 F3（x  - > y） - > F1 F2 F3（F4 x  - > F4 y）
  

现在，对于我们必须将 F1 F2 F3（x - > y）与（a - > b） - > F5 a - > F5 b 。

因此 F1 =（ - >）（a - > b）和 F2 F3（x - > y）必须与 F5 a - > F5 b 。

因此 F2 =（ - >）（F5 a）和 F3 （x→y）= F5b ，即 F5 = F3 并且 b = x - > ÿ。结果是：



  fmap ^（4k + 2）:: F1 F2 F3（F4 x  - > F4 y）
 =（a  - >（x  - > y）） - > F3a  - > F3（F4 x  - > F4 y）
  

对于 fmap ^（4k +3），我们必须统一 a - > （x - > y），其中（m - > n） - > F6 m - > F6 n），给出 a = m - > n ，

x = F6 m 和 y = F6 n ，所以

  fmap ^（4k + 3）:: F3 a  - > F3（F4 x→F4 y）
 = F3（m→n）→> F3（F4 F6 m  - > F4 F6 n）
  

最后，我们必须统一 F3（m - > n）与（a - > b） - > F7 a - > F7 b ，所以 F3 =（ - >）（a - > b）， m = F7 a 和 n = F7 b ，因此



  fmap ^（4k + 4）:: F3（F4 F6 m  - > F4 F6 n）
 =（a  - > b） - > （F4 F6 F7 a  - > F4 F6 F7 b）
  

并且周期结束。当然，结果来自查询ghci，但也许衍生揭示了它如何工作。

I was playing around with functors, and I noticed something interesting:

Trivially, id can be instantiated at the type (a -> b) -> a -> b.

With the list functor we have fmap :: (a -> b) -> [a] -> [b], which is the same as map.

In the case of the ((->) r) functor (from Control.Monad.Instances), fmap is function composition, so we can instantiate fmap fmap fmap :: (a -> b) -> [[a]] -> [[b]], which is equivalent to (map . map).

Interestingly, fmap eight times gives us (map . map . map)!

So we have

0: id = id
1: fmap = map
3: fmap fmap fmap = (map . map)
8: fmap fmap fmap fmap fmap fmap fmap fmap = (map . map . map)

Does this pattern continue? Why/why not? Is there a formula for how many fmaps I need to map a function over an n-times nested list?

I tried writing a test script to search for a solution to the n = 4 case, but GHC starts eating too much memory at around 40 fmaps.

解决方案

I can't explain why, but here's the proof of the cycle:

Assume k >= 2 and fmap^(4k) :: (a -> b) -> F1 F2 F3 a -> F1 F2 F3 b, where Fx stands for an unknown/arbitrary Functor. fmap^n stands for fmap applied to n-1 fmaps, not n-fold iteration. The induction's start can be verified by hand or querying ghci.

fmap^(4k+1) = fmap^(4k) fmap
fmap :: (x -> y) -> F4 x -> F4 y

unification with a -> b yields a = x -> y, b = F4 x -> F4 y, so

fmap^(4k+1) :: F1 F2 F3 (x -> y) -> F1 F2 F3 (F4 x -> F4 y)

Now, for fmap^(4k+2) we must unify F1 F2 F3 (x -> y) with (a -> b) -> F5 a -> F5 b.
Thus F1 = (->) (a -> b) and F2 F3 (x -> y) must be unified with F5 a -> F5 b.
Hence F2 = (->) (F5 a) and F3 (x -> y) = F5 b, i.e. F5 = F3 and b = x -> y. The result is

fmap^(4k+2) :: F1 F2 F3 (F4 x -> F4 y)
             = (a -> (x -> y)) -> F3 a -> F3 (F4 x -> F4 y)

For fmap^(4k+3), we must unify a -> (x -> y) with (m -> n) -> F6 m -> F6 n), giving a = m -> n,
x = F6 m and y = F6 n, so

fmap^(4k+3) :: F3 a -> F3 (F4 x -> F4 y)
             = F3 (m -> n) -> F3 (F4 F6 m -> F4 F6 n)

Finally, we must unify F3 (m -> n) with (a -> b) -> F7 a -> F7 b, so F3 = (->) (a -> b), m = F7 a and n = F7 b, therefore

fmap^(4k+4) :: F3 (F4 F6 m -> F4 F6 n)
             = (a -> b) -> (F4 F6 F7 a -> F4 F6 F7 b)

and the cycle is complete. Of course the result follows from querying ghci, but maybe the derivation sheds some light on how it works.

这篇关于有趣的重复fmap的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！