在类型运算符存在的情况下实现嵌套/递归数据类型

Question

我一直在使用Pierce的《类型和编程语言》中的Rust实现System F-omega，想要添加iso-recursive的fold/unfold运算符来实现递归类型，并寻求指导。已经添加了和、积、记录、存在和全局类型。

在System F（没有类型操作符）中，我发现这相对简单，只需在解析后通过AST进行访问器遍历，在情况分析或类型构建期间执行折叠/展开同构即可。

而对于System F omega，由于类型层面存在lambda抽象，情况则较为复杂。例如（使用标准lambda-calc/haskell-ish语法），假设我想定义一个参数化的List数据类型。

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

这可以被编码在我们的演算中（省略*种类）：

type List = μ ΛX::*=>*. ΛA. Cons A (X A) | Nil
substs to: ΛA. Cons A ((μ ΛX::*=>*. ΛA. Cons A (X A) | Nil) A) | Nil

但是，一旦我们试图展开值，就会遇到问题，因为引入了一个新的抽象来再次绑定A。这似乎可能有效，只要我们在某个地方存储了具体类型A。

或者我们可以将其“lambda降级”为：

type ListF = ΛX. ΛA. Cons (A, X) | Nil
type List  = ΛA. μ (ListF A)

lambda删除对于像这样简单的递归类型非常有效，并且也很容易实现，我可以设想一种自动生成ListF类型的方式。但是我有一种烦恼的感觉，似乎有什么不对劲。

我一直在尝试阅读围绕此主题的文献（Mendler-style迭代、Andreas Abel、Ralph Matthes、Tarmo Uustalu，“Iteration and coiteration schemes for higher-order and nested datatypes”等），但说实话有些内容让我有点力不从心，而且我不知道如何以具体的方式实现它。任何建议都将不胜感激。

- crunch

---

我不确定我是否理解mu展开成抽象的问题。在第一个例子中，List应该展开为Cons A ((μ ...) A) | Nil，而不是Cons A (μ ...) | Nil（即，μ应该应用于A）。这可能是混淆的源头吗？这确实使类型检查变得困难，但这似乎不是您关心的问题，是吗？ - Li-yao Xia

那只是我从代码中翻译时的笔误，谢谢你发现了它。 - crunch

Answer 1

List = μ ΛX. ΛA. Cons A (X A) | Nil
-- μF unfolds to F(μF)
= (ΛX. ΛA. Cons A (X A) | Nil) (μ ΛX. ΛA. Cons A (X A) | Nil)
-- substitute *correctly*
= ΛA. Cons A ((μ ΛX. ΛA. Cons A (X A) | Nil) A) | Nil
--                                           ^ you dropped this!
-- folding back
List = ΛA. Cons A (List A) | Nil

A不需要在任何地方存储，除了类型本身。您删除了包含它的应用程序，但不应该删除它。请注意，您的展开是不良类型化的。顶层Cons的第二个字段具有* => *类型，但这是不正确的。但原始的类型是良好类型化的，因此展开（应该保留类型）一定出了问题。

"Lambda dropping"很好，但并非总是可行。考虑

data Binary a = Leaf a | Branch (Binary (a, a))

该类型包含了精确的2^n个a，其中n是自然数。这种类型是不规则递归的，不能用μ :: (* => *) => *来表示，就像List一样。

type Binary = μ ΛX. ΛA. Leaf A | Branch (X (A, A))

- HTNW

---

啊，那是个笔误，谢谢你发现了它。我保证我知道替换的工作原理，并且已经在代码中实现了它 :)。 - crunch

即使在那里进行了正确的替换，它也不是格式良好的，因为您不能将递归类型应用于具体类型，只能应用于类型抽象。让我们将“Nat”应用于我们正确替换的“List”类型： List = Cons Nat ((μ ΛX. ΛA. Cons A (X A) | Nil) Nat) | Nil。Nat无法替换到A的内部出现，因此我们必须将“Nat”存储在某个地方，以便下次需要折叠时应用它。 - crunch

我相信即使您修改了打字规则，以便在类型检查期间执行展开同构（以便您可以评估 (μ ΛX. ΛA. Cons A (X A) | Nil) Nat），您最终也会陷入无限循环，因为您不断引入新的类型抽象 ΛA.。这不正确吗？ - crunch

为什么你需要替换 Nat 呢？只需让应用程序并让折叠算子的类型处理它。fold1_F_A :: F (μ F) A -> μ F A，特别是 fold1_(ΛX. ΛA. Cons A (X A) | Nil)_Nat :: (Cons Nat ((μ ΛX. ΛA. Cons A (X A) | Nil) Nat) | Nil) -> ((μ ΛX. ΛA. Cons A (X A) | Nil) Nat)。 - HTNW

谢谢。我曾经认为那是另一种方法。Andreas Abel的博士论文《带有大小高阶类型的多态λ演算》也在某种程度上涵盖了这个问题，第3.5节和第4节。我认为你描述的方法（以及论文中描述的方法）可能是我最终会使用的方法。 - crunch