玫瑰树的初始代数

Question

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

• 自然数data Nat = Zero | Succ Nat 对应于内函子F(-) = 1 + (-) 的初始代数。
• 列表data List a = Nil | Cons a (List a)，对应于内函子F(A, -) = 1 + A × (-)的初始代数。

但是，我不清楚玫瑰树对应的内函子应该是什么：

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

我不鼓励谈论“Hask 类别”，因为它会潜意识地限制您在 Haskell 编程中寻找其他类别结构。

确实，玫瑰树可以看作是类型和函数上的内函子的固定点，我们最好将其称为Type，因为Type 是类型的类型。如果我们给自己一些常用的函子套件...

newtype K a   x = K a deriving Functor           -- constant functor
newtype P f g x = P (f x, g x) deriving Functor  -- products

...和固定点...

newtype FixF f = InF (f (FixF f))

...那么我们可以采取

type Rose a = FixF (P (K a) [])
pattern Node :: a -> [Rose a] -> Rose a
pattern Node a ars = InF (P (K a, ars))

[] 本身是递归的这一事实并不妨碍它在通过Fix 形成递归数据类型中的使用。为了明确地说明递归，我们有嵌套的固定点，这里有提示性地选择绑定变量名称：

Rose a = μrose. a * (μlist. 1 + (rose * list))

现在，当我们到达第二个固定点时，我们有了一个类型公式

1 + (rose * list)

在rose 和list 中都是函数式的（实际上，严格来说是积极的）。有人可能会说它是Bifunctor，但这是不必要的术语：它是从(Type, Type) 到Type 的函子。您可以通过在该对的第二个组件中获取一个固定点来创建一个Type -> Type 函子，这就是上面发生的事情。

Rose 的上述定义丢失了一个重要的属性。这不是真的

Rose :: Type -> Type   -- GHC might say this, but it's lying

如果x :: Type，则只是Rose x :: Type。特别是，

Functor Rose

不是一个类型良好的约束，很遗憾，从直觉上讲，玫瑰树在它们存储的元素中应该是函数式的。

您可以通过构建Rose 来解决此问题，因为它本身就是Bifunctor 的固定点。因此，实际上，当我们到达列表时，我们在范围内有 三个 类型变量，a、rose 和 list，并且我们在所有这些变量中都具有功能性。您需要一个不同定点类型构造函数，以及一个不同工具包来构建Bifunctor 实例：对于Rose，生活变得更轻松，因为没有使用a 参数在内部固定点中，但一般来说，将双函子定义为固定点需要三函子，我们开始吧！

我的

This answer 通过展示 indexed 类型如何在 fixpoint-of-functor 构造下关闭 来展示如何对抗扩散。也就是说，不是在Type 中工作，而是在i -> Type 中工作（对于各种索引类型i），您就可以进行相互递归、GADT 等等了。

因此，缩小后，玫瑰树是由相互固定点给出的，它们具有完全合理的分类帐户，前提是您可以看到哪些类别实际上在起作用。

Answer 2

这不是您所问问题的真正答案，但无论如何可能很有趣。请注意，与

Rose a = a * List (Rose a)
List a = 1 + a * List a

事实上* 分布在+ 上，你有

  Rose a 
=   {- definition of `Rose` -}
  a * List (Rose a)
=   {- definition of `List` -}
  a * (1 + Rose a * List (Rose a))
=   {- `*` distributes over `+` -}
  a + a * Rose a * List (Rose a)
=   {- `*` is commutative -}
  a + Rose a * a * List (Rose a)
=   {- definition of `Rose` -}
  a + Rose a * Rose a

（等式实际上表示同构）。所以你不妨定义

Rose a = a + Rose a * Rose a

或者在 Haskell 中，

data Rose a = Leaf a | Bin (Rose a) (Rose a)

也就是说，玫瑰树与普通的（叶子标记的）二叉树同构，并且清楚地形成了正常的初始代数。

Answer 3

正如您所注意到的，Rose a 的函子的定义比较棘手，因为该类型的递归出现被馈送到List 中。问题是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

另一种更有趣的方法是遵循您发布的参考文献中的建议，并注意Rose a 的类型可以概括为抽象出递归事件被输入的函子

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

现在GRose 具有(* -> *) -> (* -> *) 类型，因此它是将一个内函子映射到另一个内函子的高阶函子。在我们的示例中，它将函子 List 映射到玫瑰树的类型。

但是请注意，GRose 仍然是递归的，所以上面的内容实际上是在说明同构而不是解决我们的问题。我们可以尝试通过对递归点进行额外抽象来解决（眨眼）这个问题

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

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

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

所以如果我们输入Rose ≡ μ(HRose) List，我们得到

Rose A ≃ A × List (Rose A)

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

Answer 4

你似乎明白这是如何建模的

data List a = Nil | Cons a (List a)

对于任何给定的A，采用内函子F(A, -) = 1 + A × (-) 的初始代数。我们称这个初始代数为L(A)。

如果我们忘记了L(A) 中的态射，我们可以认为L(A) 是我们范畴的一个对象。更好的是，L(-) 不仅是对象到对象的映射，还可以看作是一个内函子。

一旦L 是作为内函子的种子，递归类型

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

通过对任何Am 取函子的初始代数来解释

G A = A * L A

这是一个由L和*（和对角函子）组成的函子。 因此，同样的方法也有效。