如何解决应用于 foldr 的 lambda 函数中的 Haskell 相关自变量
给定
> foldr (+) 5 [1,2,3,4]
15
第二个版本
foldr (\x n -> x + n) 5 [1,4]
也返回 15。关于第二个版本，我不明白的第一件事是 foldr 如何知道哪个变量与累加器种子 5 相关联，哪个与列表变量的元素 [1,4] 相关联。在 lambda 演算方式中，x 似乎是因变量而 n 是自变量。所以如果这个
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
是 foldr 和这些
:type foldr
foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
:t +d foldr
foldr :: (a -> b -> b) -> b -> [a] -> b
它的类型声明，我可以收集，从类型声明本身推断出“哪个是依赖的，哪个是独立的”的答案？似乎上面的 foldr 的两个例子都必须这样做
(+) 1 ((+) 2 ((+) 3 ((+) 4 ((+) 5 0))))
我只是猜到了上面的第二个 lambda 函数版本，但我真的不明白它是如何工作的，而带有 (+) 的第一个版本分解如上图所示。
另一个例子是这个
length' = foldr (const (1+)) 0
再次，const 似乎知道“抛出”传入的列表元素并简单地递增，从初始累加器值开始。这与
length' = foldr (\_ acc -> 1 + acc) 0
再一次，Haskell 知道 foldr 的第二个和第三个参数中的哪一个——累加器和列表——被视为因变量和自变量，看起来很神奇。但是不，我确信答案在于类型声明（我无法破译，因此，这篇文章），以及 lambda 演算的知识，我是初学者。
更新
我找到了这个
reverse = foldl (flip (:)) []
然后应用到一个列表
foldl (flip (:)) [] [1,3]
foldl (flip (:)) (1:[]) [2,3]
foldl (flip (:)) (2:1:[]) [3]
foldl (flip (:)) (3:2:1:[]) []
. . .
这里很明显，顺序是“累加器”，然后是列表，flip 正在翻转第一个和第二个变量，然后使它们服从 (:)。再说一遍
reverse = foldl (\acc x -> x : acc) []
foldl (\acc x -> x : acc) [] [1,3]
foldl (\acc x -> x : acc) (1:[]) [1,3]
. . .
似乎也依赖于顺序，但在上面的例子中
length' = foldr (\_ acc -> 1 + acc) 0
foldr (\_ acc -> 1 + acc) 0 [1,3]
它怎么知道 0 是累加器并且绑定到 acc 而不是第一个（幽灵）变量？因此，据我了解（前五页）lambda 演算，任何“lambda”的变量，例如，\x 是一个因变量，而所有其他非 lambda 的变量都是独立的。上面，\_ 与 [1,3] 相关联，acc 表面上是自变量，是 0；因此，顺序并不决定分配。就好像 acc 是某个关键字，在使用时总是绑定到累加器，而 x 总是在谈论传入的列表成员。
此外，t a 转换为 [a] 的类型定义中的“代数”是什么？这是来自范畴论的东西吗？看到了
Data.Foldable.toList :: t a -> [a]
在 Foldable 定义中。仅此而已吗？
解决方法
“依赖”很可能是指绑定变量。
“独立”很可能是指免费（即未绑定）变量。
(\x n -> x + n) 中没有自由变量。 x 和 n 都出现在箭头 -> 的左侧，因此它们是这个 lambda 函数的命名参数，绑定在它的主体内，到箭头的右侧。绑定意味着当此 lambda 函数确实应用于其参数时，函数主体中对 n 的每个引用都将替换为对相应参数的引用。
同样，_ 和 acc 都绑定在 (\_ acc -> 1 + acc) 的主体中。此处使用通配符这一事实并不重要。我们完全可以写_we_dont_care_。
lambda 函数定义中的参数获得“分配”（也称为“绑定”）应用程序中参数的值，纯位置。第一个参数将绑定/分配给第一个参数，第二个参数 - 第二个参数。然后根据规则进入 lambda 函数体并进一步约简。
这可以看成有点不同，即实际上在 lambda 演算中所有函数都只有一个参数，而多参数函数实际上是嵌套的单参数 lambda 函数；并且应用程序是左关联的，即嵌套在左侧。
这实际上意味着很简单
(\ x n -> x + n) 5 0
=
(\ x -> (\ n -> x + n)) 5 0
=
((\ x -> (\ n -> x + n)) 5) 0
=
(\ n -> 5 + n) 0
=
5 + 0
至于 Haskell 如何从类型签名中知道哪个是哪个，同样，函数类型中的类型变量也是位置变量，第一个类型变量对应第一个预期参数的类型，第二个类型变量对应第二个预期参数的类型等。
它所有纯粹是位置性的。
因此，作为一个纯粹机械和仔细的替换问题，因为根据 foldr 的定义它认为 foldr g 0 [1,2,3] = g 1 (foldr g 0 [2,3]) = ... = g 1 (g 2 (g 3 0))，我们有
foldr (\x n -> x + n) 0 [1,3]
=
(\x n -> x + n) 1 ( (\x n -> x + n) 2 ( (\x n -> x + n) 3 0 ))
=
(\x -> (\n -> x + n)) 1 ( (\x n -> x + n) 2 ( (\x n -> x + n) 3 0 ))
=
(\n -> 1 + n) ( (\x n -> x + n) 2 ( (\x n -> x + n) 3 0 ))
=
1 + ( (\x n -> x + n) 2 ( (\x n -> x + n) 3 0 ))
=
1 + ( (\x (\n -> x + n)) 2 ( (\x n -> x + n) 3 0 ))
=
1 + (\n -> 2 + n) ( (\x n -> x + n) 3 0 )
=
1 + (2 + (\x n -> x + n) 3 0 )
=
1 + (2 + (\x -> (\n -> x + n)) 3 0 )
=
1 + (2 + (\n -> 3 + n) 0 )
=
1 + (2 + ( 3 + 0))
换句话说，(\x n -> x + n) 和 (+) 之间绝对没有区别。
至于t中的那个foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b，意思是给定一个类型T a，如果instance Foldable T存在，那么类型变成foldr :: (a -> b -> b) -> b -> T a -> b ，当它与 T a 类型的值一起使用时。
一个例子是 Maybe a，因此是 foldr (g :: a -> b -> b) (z :: b) :: Maybe a -> b。
另一个例子是 [] a，因此是 foldr (g :: a -> b -> b) (z :: b) :: [a] -> b。
(edit:) 所以让我们关注列表。函数 foo 具有该类型意味着什么，
foo :: (a -> b -> b) -> b -> [a] -> b
？这意味着它需要一个 a -> b -> b 类型的参数，即一个函数，我们称它为 g，这样
foo :: (a -> b -> b) -> b -> [a] -> b
g :: a -> b -> b
-------------------------------------
foo g :: b -> [a] -> b
它本身是一个函数，需要一些 z 类型的参数 b，所以
foo :: (a -> b -> b) -> b -> [a] -> b
g :: a -> b -> b
z :: b
-------------------------------------
foo g z :: [a] -> b
它本身是一个函数，需要一些 xs 类型的参数 [a]，所以
foo :: (a -> b -> b) -> b -> [a] -> b
g :: a -> b -> b
z :: b
xs :: [a]
-------------------------------------
foo g z xs :: b
这样的函数 foo g z 可以做什么，给定一个列表，比如说，[x]（即 x :: a，[x] :: [a]）？
foo g z [x] = b where
我们需要生成一个 b 值，但是如何生成？好吧，g :: a -> b -> b 产生一个函数 b -> b，给定类型为 a 的值。等等，我们有！
f = g x -- f :: b -> b
它对我们有什么帮助？好吧，我们有z :: b，所以
b = f z
如果我们得到的是 [] 呢？我们根本没有任何 a，但是我们有一个 b 类型值，z - 所以我们只是定义
b = z
如果我们得到的是 [x,y] 呢？我们将执行相同的 f 构建技巧，两次：
f1 = g x -- f1 :: b -> b
f2 = g y -- f2 :: b -> b
为了产生 b，我们现在有很多选择：它是 z！或者，它是f1 z！？还是f2 z？但是我们可以做的最一般的事情是利用所有我们可以访问的数据
b = f1 (f2 z)
对于右折叠（......或，
b = f2 (f1 z)
对于左).
如果我们替换并简化，我们得到
foldr g z [] = z
foldr g z [x] = g x z -- = g x (foldr g z [])
foldr g z [x,y] = g x (g y z) -- = g x (foldr g z [y])
foldr g z [x,y,w] = g x (g y (g w z)) -- = g x (foldr g z [y,w])
出现了一种模式。
诸如此类，诸如此类
旁注：b 是一个糟糕的命名选择，这在 Haskell 中很常见。 r 会好得多——“递归结果”的助记符。
另一个助记符是 g 的参数顺序：a -> r -> r 建议，而不是规定，列表的元素 a 作为第一个参数出现； r 递归结果排在第二位（递归处理输入列表其余部分的结果——递归，因此以相同的方式）；然后由这个“步骤”函数 g 产生整体结果。
这就是递归的本质：递归处理输入结构的自相似子部分，并通过一个简单的单步完成处理：
a a
: `g`
[a] r
------------- -------------
[a] r
[a]
a [a]
--------
(x : xs) -> r
xs -> r
----------------------
( x,r ) -> r --- or,equivalently,x -> r -> r
好吧，foldr 本身根据定义知道这一点。它的定义方式是它的函数参数接受累加器作为第二个参数。
就像您编写 div x y = ... 函数时一样，您可以随意使用 y 作为股息。
也许您对 foldr 和 foldl 在累加器函数中交换了参数这一事实感到困惑？
正如 Steven Leiva 所说的 here，foldr (1) 接受一个列表并用给定的函数替换 cons 运算符 (:) 并且 (2) 替换最后一个空列表 {{ 1}} 与累加器种子，这就是 [] 的定义所说的
foldr因此脱糖的 [1,3] 是
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
并且递归实际上用 (:) 1 ((:) 2 ((:) 3 []))
替换了 (:)，正如我们在 f 中看到的那样，foldr f z (x:xs) = f x (foldr f z xs) 种子值会一直运行，直到替换 z 的基本情况，满足上面的 (1) 和 (2)。
我的第一个困惑是看到这个
[]并且不理解它会根据上面的定义扩展到
foldr (\x n -> x + n) 0 [1,3]
接下来，由于对实际 Beta 减少将如何进行的了解不足，我没有理解下面的第二到第三步
(\x n -> x + n) 1 ((\x n -> x + n) 2 ((\x n -> x + n) 3 0 ))
第二到第三步是 lambda 演算很奇怪，但这是为什么 (\x -> (\n -> x + n)) 1 ...
(\n -> 1 + n) ...
1 + ...
和 (+) 是同一件事的根源。我不认为它是纯粹的 lambda 演算加法，但它（详细地）模拟了递归中的加法。我可能需要跳回 lambda 演算才能真正理解为什么 (\x n -> x + n) 变成 (\n -> 1 + n)
我更糟糕的心理障碍是认为我首先在括号内查看某种热切的评估
1 + 其中 foldr ((\x n -> x + n) 0 [1,3,4])
的三个参数将首先交互，即 foldr 将绑定到 0，列表成员绑定到 x
n。 . .然后我不知道该怎么想。完全错误的想法，尽管正如 Will Ness 上面指出的那样，beta 减少是将参数绑定到变量的位置。但是，当然，我忽略了 Haskell 柯里化意味着我们首先遵循 (\x n -> x + n) 0 [1,4]
0 + 1
的扩展这一事实。
我还没有完全理解类型定义
foldr除了评论/猜测第一个 foldr :: (a -> b -> b) -> b -> [a] -> b
和 a 表示 [a] 是传入列表成员的类型，而 a 是(a -> b -> b) 会做什么的初步缩影，即，它将接受传入列表类型的参数（在我们的例子中是列表的元素？）然后是另一个 foldr 类型的对象并产生一个对象 b。所以种子参数是 b 类型，整个过程最终会产生 b 类型的东西，而且给定的函数参数将采用 b 并最终返回一个对象 {{1 }} 这实际上也可能是 a 类型，实际上在上面的例子中是整数...... IOW，我并没有真正掌握类型定义......
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
