玫瑰树的初始代数

Question

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

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

但是我不清楚玫瑰树对应的endofunctor应该是什么：

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

如您所见，Rose a 的函子定义比较棘手，因为该类型的递归出现被送入 List。问题是 List 本身就是一个作为不动点得到的递归类型。 List (Rose a) 基本上对应于一个 "arbitrary number of elements of 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 2

我不鼓励谈论 "the Hask Category"，因为它会潜意识地限制您在 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

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

Functor Rose

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

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

我的

通过展示 indexed 类型如何在 fixpoint-of 下 closed 来展示如何对抗扩散-仿函数构造。也就是说，不是在 Type 中工作，而是在 i -> Type 中工作（对于各种索引类型 i），并且您已准备好相互递归、GADT 等。

因此，缩小范围，玫瑰树由相互固定点给出，它们有一个非常合理的分类帐户，前提是您看到哪些类别实际在起作用。

Answer 3

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

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和*（以及对角线函子）组合得到的函子。因此，同样的方法有效。

Answer 4

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

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)

也就是说，玫瑰树与普通的（叶子标记的）二叉树同构，显然形成了一个正常的初始代数。

玫瑰树的初始代数

Initial algebra for rose trees

recursion

haskell

algebra

algebraic-data-types

category-theory