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

Question

我一直在遵循 Pierce 的类型和编程语言，在 Rust 中实现系统 F-omega，并且我正在寻找使用 iso-recursive 将递归类型添加到我的实现中的指导折叠/展开运算符。我已经添加了 sum、product、record、existential 和 universal 类型。

在系统 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

但是一旦我们尝试展开该值，就会出现问题，因为引入了尝试再次绑定(bind) A 的新抽象。只要我们将具体类型 A 存储在某个地方，这似乎就可以工作。

或者我们可以将其“lambda drop”到:

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

lambda 删除对于像这样的简单递归类型效果很好，而且实现起来也很简单，我可以设想一种自动生成 ListF 类型的方法。但我有一种挥之不去的感觉，这件事有些不对劲。

我一直在尝试阅读与此相关的文献(Mendler 式迭代、Andreas Abel、Ralph Matthes、Tarmo Uustalu、“高阶和嵌套数据类型的迭代和迭代方案”等)，但其中一些有点超出我的能力范围，我不知道如何以具体的方式实际实现这一点。任何建议将不胜感激

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 下降”很好，但并不总是可行。考虑一下

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

其中恰好包含一些自然 n 的 2^n a。这种类型是不规则递归的，不能像 List 那样用 μ::(* => *) => * 来表示。

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