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