我一直在深入研究foldTree
Haskell中的函数,它的定义如下:
foldTree :: (a -> [b] -> b) -> Tree a -> b
foldTree f = go where
go (Node x ts) = f x (map go ts)
最近我偶然发现了对这句话的如下解释:
当我们调用时
f x vs
,我们假设x
和vs
已经与已知值绑定。
go (Node x ts) = f x (map go ts)
- 的值
x
已经按照预期且熟悉的方式进行绑定。 - 然而,尚未绑定任何值
vs
;绑定vs
被推迟到整个子林的递归完成为止。
提到时间元素(使用“已经”和“尚未”等术语)让我感到困惑。为了更好地理解这一点,我开始尝试一些从自然演绎和归纳证明中借用的概念。具体来说,我试图将第二个论点概念化f
如下:
- 我假设已经定义了一种类型
[b]
。 - 然后,我考虑的实际定义是将这个假定类型与类型
f
相结合来定义整体表达式,其中类型为。[b]
a
foldTree f tree
tree
Tree a
我如何才能在假设方面完善这种思路,而不是使用实际函数求值,假设它是正确的?或者,我是否可以采用另一种正式或直观的视角来更好地理解这个函数及其机制?
这是惰性求值的结果 [Haskell-wiki]。
好吧,它与表达式绑定,与
map go ts
,就是这样。当f
需要它的值时,[b]
它将强制评估该表达式树。这意味着它将开始评估map go ts
。树可能没有子项,在这种情况下map
将返回一个空列表。如果树有子树,它将通过惰性求值来评估列表,因为需要节点,甚至不会对其中一个子树进行评估。
go ti
ti
Node
但由于 Haskell 函数是纯函数,因此顺序本质上并不重要。您可以假装这些项已被求值。