玫瑰树的初始代数 [英] Initial algebra for rose trees

问题描述

据我了解，Haskell的递归数据类型对应于Hask类别[ 1 ， 2 ].例如:

As far as I understand, recursive data types from Haskell correspond to initial algebras of endofunctors from the Hask category [1, 2]. For example:

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

• Natural numbers, data Nat = Zero | Succ Nat, correspond to the initial algebra of the endofunctor F(-) = 1 + (-).
• Lists, data List a = Nil | Cons a (List a), correspond to the initial algebra of the endofunctor F(A, -) = 1 + A × (-).

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

However, it's not clear to me what the endofunctor corresponding to the rose trees should be:

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

让我感到困惑的是，有两个递归:一个递归给玫瑰树，另一个递归给列表.根据我的计算，我将获得以下函子，但这似乎不正确:

What confuses me is that there are two recursions: one for the rose tree and the other for the list. According to my calculations, I would get the following functor, but it doesn't seem right:

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

---

或者，玫瑰树可以定义为相互递归的数据类型:

---

Alternatively, rose trees can be defined as mutually recursive data types:

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

相互递归的数据类型在范畴论中有解释吗?

Do mutually recursive data types have an interpretation in category theory?

推荐答案

我不鼓励谈论"Hask类别"，因为它在潜意识中使您无法在Haskell编程中寻找其他分类结构.

I would discourage talk of "the Hask Category" because it subconsciously conditions you against looking for other categorical structure in Haskell programming.

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

Indeed, rose trees can be seen as the fixpoint of an endofunctor on types-and-functions, a category which we might be better to call Type, now that Type is the type of types. If we give ourselves some of the usual functor kit...

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

...和固定点...

...and fixpoints...

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

...那么我们可以接受

...then we may take

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

[]本身是递归的事实并不能阻止其在通过Fix形成递归数据类型中使用.为了明确说明递归，我们有嵌套的固定点，在这里我们建议性地选择绑定变量名称:

The fact that [] is itself recursive does not prevent its use in the formation of recursive datatypes via Fix. To spell out the recursion explicitly, we have nested fixpoints, here with bound variable names chosen suggestively:

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

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

Now, by the time we've arrived in the second fixpoint, we have a type formula

1 + (rose * list)

在rose和list中都是函数(实际上是严格肯定的).也许有人会说这是一个Bifunctor，但这是不必要的术语:它是一个从(Type, Type)到Type的函子.您可以通过在该对的第二个组件中使用一个固定点来制作Type -> Type仿函数，这就是上面发生的事情.

which is functorial (indeed, strictly positive) in both rose and list. One might say it is a Bifunctor, but that's unnecessary terminology: it's a functor from (Type, Type) to Type. You can make a Type -> Type functor by taking a fixpoint in the second component of the pair, and that's just what happened above.

Rose的上述定义失去了重要的属性.

The above definition of Rose loses an important property. It is not true that

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

仅仅是Rose x :: Type，如果是x :: Type.特别是

merely that Rose x :: Type if x :: Type. In particular,

Functor Rose

并不是一个很好类型的约束，这很遗憾，直觉上，玫瑰树应该在它们存储的元素中是功能性的.

is not a well typed constraint, which is a pity, as intuitively, rose trees ought to be functorial in the elements they store.

您可以通过将Rose构建为Bifunctor的固定点来解决此问题.因此，实际上，到列表时，我们在范围内有三个类型变量，分别为a，rose和list，并且所有这些函数都具有功能性.您需要一个 different 固定点类型构造函数和一个 different 套件来构建Bifunctor实例:对于Rose，由于不使用a参数，因此生活变得更加轻松在内部定点中，但是总的来说，要将bifunctors定义为定点，需要使用trifunctors，然后我们就开始了！

You can fix this by building Rose as itself being the fixpoint of a Bifunctor. So, in effect, by the time we get to lists, we have three type variables in scope, a, rose and list, and we have functoriality in all of them. You need a different fixpoint type constructor, and a different kit for building Bifunctor instances: for Rose, life gets easier because the a parameter is not used in the inner fixpoint, but in general, to define bifunctors as fixpoints requires trifunctors, and off we go!

我的答案通过显示索引类型如何显示了如何抵抗扩散 closed 在功能固定点的构造下.也就是说，不是在Type中工作，而是在i -> Type中工作(针对各种索引类型i)，并且您已经准备好进行相互递归，GADT等.

This answer of mine shows how to fight the proliferation by showing how indexed types are closed under a fixpoint-of-functor construction. That's to say, work not in Type but in i -> Type (for the full variety of index types i) and you're ready for mutual recursion, GADTs, and so on.

因此，如果缩小，则玫瑰树是由相互固定的点给出的，这些固定点具有完全合理的分类说明，只要您看到实际使用的分类即可.

So, zooming out, rose trees are given by mutual fixpoints, which have a perfectly sensible categorical account, provided you see which categories are actually at work.

这篇关于玫瑰树的初始代数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！