玫瑰树的初始代数

Question

据我明白,从Haskell的递归数据类型对应于endofunctors的初始代数从Hask类别[ 1,2 ].例如:

• 自然数,data Nat = Zero | Succ Nat对应于endofunctor的初始代数F(-) = 1 + (-).
• 列表,data List a = Nil | Cons a (List a)对应于endofunctor的初始代数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

我会劝阻谈论"Hask类别",因为它潜意识地阻止你在Haskell编程中寻找其他分类结构.

实际上,玫瑰树可以被视为类型和函数的endofunctor的固定点,我们可能更好地调用它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,并且我们在所有这些变量中都具有兼容性.你需要一个不同的 fixpoint类型构造函数,以及一个用于构建实例的不同工具包Bifunctor:for Rose,生活变得更容易,因为a参数没有在内部修复点中使用,但一般来说,将bifunctors定义为fixpoints需要trifunctors,然后关闭!

我的这个答案显示了如何通过展示索引类型在仿函数修复点构造下的关闭来对抗扩散.也就是说,工作不在,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)

也就是说，玫瑰树与普通（叶标）二叉树同构，并且显然形成了正规的初始代数。