玫瑰树的初始代数

Question

据我所知，来自Haskell的递归数据类型对应于Hask类别[1,2]中的内函数的初始代数。例如：

null

data Rose a = Node a (List (Rose a))

F(A, •, -) = A × (1 + (-) × (•))

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

Answer 1

正如您所注意到的，RoseA的函数的定义更加复杂，因为类型的递归出现被输入到列表中。问题在于list本身是作为固定点获得的递归类型。List（Rose a)基本上对应于“Rose a的任意数量的元素”，这些元素不能单独用乘积和和的签名来表示，因此需要对这些多个递归点进行额外的抽象。

函数f a-:*->*将不起作用，因为我们需要找到这样的内容

F A X ≃ A × (1 + X × List X)
F A X ≃ A × (1 + X × (1 + X × List X))
F A X ≃ A × (1 + X × (1 + X × (1 + X × List X)))
...

一种方法是将list视为基本元素。则Rose A只是

RoseF A : * -> * = λ X . A × List X

GRose F A ≃ A × F (GRose F A)

但是请注意，GRose仍然是递归的，所以上面所说的实际上是一个同构，而不是我们问题的解决方案。我们可以通过对递归点进行额外的抽象来解决（wink wink）这个问题

HRose G F A = A × F (G F A)

注意，现在hrose是((*->*)->(*->*))->(*->*)->(*->*)类型的常规高阶函数，因此它将高阶函数映射为高阶函数。计算hrose的最小不动点给我们

μ(HRose) F A ≃ A × F (μ(HRose) F A)

因此，如果我们将rose️μ(HRose)列表，我们将得到

Rose A ≃ A × List (Rose A)

这正是玫瑰树的定义方程。你可以找到许多关于使用高阶函子上的不动点的泛型程序设计的理论和实践的进一步例子。例如，这里，Bird和Paterson在嵌套数据类型的上下文中开发了它（但定义显然普遍适用）。它们还显示了以这种方式定义的数据类型上的折叠的系统构造，以及各种法律。