Idris `foldl` 默认实现

如何解决Idris `foldl` 默认实现

interface Foldable t where
  foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl f z t = foldr (flip (.) . flip f) id t z

这里的 foldr (flip (.) . flip f) id t z 是什么意思？
还有另一种使用 foldl 实现 foldr 的方法吗？
谢谢回答。

解决方法

上面定义的 foldl 中的第一个参数可以变成这样的 lambda：

\element -> (. (flip f element))
-- or
\element prevFun -> prevFun . flip f element
-- or
\element prevFun next -> prevFun $ f next element

让我们举一个例子，你想在列表 [a,b,c] 上折叠左边。您希望最终结果为 f (f (f z a) b) c)，其中 z 是累加器。

在第一次迭代中，第一个参数是 c，第二个参数是 id。因此，结果将是 id . flip f c，或者只是 flip f c（因为 id . f 只是 f，正如 @chepner 指出的那样）。

第二次迭代会产生 flip f c . flip f b，之后你会得到 flip f c . flip f b . flip f a（基本上，为每个下一个元素 . flip f x 添加一个 x。

这扩展为：

acc -> flip f c (flip f b (flip f a acc))
-- or
acc -> flip f c (flip f b (f acc a))
-- or
acc -> f (f (f acc a) b) c)

等等！我们有一个函数接受一个累加器 acc，并返回 foldl f acc t 的结果，所以我们只需将它应用到实际的累加器 z。