玫瑰树如何展开工作（来自 Origami Programming）

Question

我一直在阅读文章 Origami Programming by Jeremy Gibbons 并且无法弄清楚 unfoldR 和 unfoldF 函数如何为 Rose Trees 工作。

在论文中Rose Tree类型定义为：

data Rose α = Node α (Forest α)
type Forest α = List (Rose α)

unfoldR 和 unfoldF 函数是相互递归的，定义为：

unfoldR :: (β → α) → (β → List β) → β → Rose α
unfoldR f g x = Node (f x) (unfoldF f g x)

unfoldF :: (β → α) → (β → List β) → β → Forest α
unfoldF f g x = mapL (unfoldR f g) (g x)

看起来，除了一些小的边缘情况外，这些函数将无限递归。这两个相互递归的函数如何终止？

Answer 1

它们不一定会终止！

unfoldR 和 unfoldF 的定义分别在 Rose 和 Forest 类型上形成了 co-inductive 函数。共诱导是结构诱导的对偶。共归纳函数旨在创建无限的数据结构，稍后将通过递归函数使用这些数据结构。

由于 Haskell 的惰性求值，我们可以通过将函数 f :: (β → α) 和 g :: (β → List β) 以及初始“种子值”x :: β 应用到任一函数来定义和创建无限相互递归的 Rose 和 Forest 数据结构unfoldR 和 unfoldF。

然后我们将使用另一个递归函数 h :: Rose -> γ 来使用无限数据结构

把一个未定义的例子放在一起：

f :: (β → α)
f = undefined
g :: (β → List β) 
g = undefined
x :: β
x = undefined
h :: Rose -> γ
h = undefined

result :: γ
result = h $ unfoldR f g x

这里的result 将是对无限结构计算的评估。但如果是无限数据结构，h 怎么终止呢？ 如何 result 曾经被评估过？

虽然unfoldR f g x 会产生无限结构，但h 只会搜索搜索空间的有限子集，因此可以评估result。

注意： 我们也可以定义f, g & x 来创建一个有限结构，它不必是无限的