玫瑰树的初始代数

实际上,玫瑰树可以被视为类型和函数的内函子的不动点,我们最好称之为内函子 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))

[] is本身递归并不会阻止其通过以下方式形成递归数据类型: Fix . 为了明确说明递归,我们有嵌套的不动点,这里暗示地选择了绑定变量名:

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

现在,当我们到达第二个不动点时,我们有了一个类型公式

1 + (rose * list)

这在两个方面都是功能性的(实际上,严格地说是正的) rose list . 有人可能会说这是一个 Bifunctor ,但这是不必要的术语:它是来自 (Type, Type) 到 . 你可以做一个 Type -> Type

上述定义 Rose 失去了重要的财产。这不是真的

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

Rose x :: Type 如果 x :: Type

Functor Rose

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

你可以通过构建 因为它本身是 双Functor 三 a , 和 ,它们都有函数性。你需要一个 不同的 不动点类型构造函数和 不同的 建筑用套件 双Functor 实例:用于 玫瑰 ,生活变得更轻松,因为 参数不用于内不动点,但一般来说,将双Functor定义为不动点需要三函子,我们开始吧!

This answer 类型为 关闭 在函子构造的不动点下。也就是说,工作不在 类型 但是在 i -> Type i )您已经准备好进行相互递归、GADT等等。

这并不是你要问的问题的答案,但无论如何可能很有趣。请注意

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

或者在哈斯克尔,

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

Rose a List . 问题是 列表 本身是作为不动点获得的递归类型。 List (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)))
...

一种方法就是治疗 列表 罗斯a 只是

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

罗斯a

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

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

但是请注意,GRose仍然是递归的,因此上面实际上是在说明同构,而不是问题的解决方案。我们可以尝试通过在递归点上额外抽象来修复(wink-wink)

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在嵌套数据类型的上下文中开发了它(但定义显然在一般情况下适用)。它们还显示了以这种方式定义的数据类型上的折叠的系统构造,以及各种定律。

你似乎理解这是如何建模的

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))

对于任何 A.

G A = A * L A

这是一个通过合成得到的函子 L * 因此,同样的方法也适用。