问题描述
给定
> 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,我并没有真正掌握类型定义......