类型理论中mu（μ）绑定的作用范围

Question

在 Haskell 中，列表可能看起来像这样：

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

一种类型理论解释是：

λα.μβ.1+αβ

使用函子的不动点来编码列表类型。在 Haskell 中可以表示为：

data Fix f = In (f (Fix f))
data ListF a b = Nil | Cons a b
type List  a   = Fix (ListF a)

我对早期的μ binder的作用范围很好奇。在外部作用域中绑定的名称能否在内部作用域中保持可用性？例如，以下表达式是否有效：

μγ.1+(μβ.1+γβ)γ

也许它与以下内容相同：

μβ.μγ.1+(1+γβ)γ

但是当名称被重复使用时，事情会发生什么变化：

μβ.μγ.1+(μβ.1+γβ)γ

以上所有类型都是常规类型吗？

- user2023370

---

我认为 type List = ... 应该改为 type List a = ...。 - Erik Post

谢谢@eriksensei - 我已经修复了。 - user2023370

Answer 1

μ的作用域与其他绑定符号没有区别，因此，是的，你提供的所有示例都是有效的。它们也是常规的，因为它们甚至不包含λ。(*)

至于相等性，这取决于你拥有哪种μ类型。基本上有两种不同的概念：

• 等价递归：在这种情况下，类型规则假定一个等式

  μα.T = T[μα.T / α]

  即，递归类型被认为等于其一级“展开”，其中μ被移除，μ绑定变量被替换为类型本身(因为这个规则可以反复应用，所以可以展开任意多次)。

• 等值递归：在这里，没有这样的等价性存在。相反，μ类型是一种独立的类型形式，具有自己的表达式形式来引入和消除它——它们通常被称为roll和unroll(或fold和unfold)，并且如下所示进行了类型化：

  roll : T[μα.T / α] → μα.T

  unroll : μα.T → T[μα.T / α]

  必须在术语层面上明确地应用这些操作，以反映上面的方程(每个展开级别应用一次)。

像ML或Haskell这样的函数式语言通常使用后者来解释数据类型。然而，roll/unroll内置于数据构造函数的使用中。因此，每个构造函数都是一个注入到等值递归类型中的注入，与求和类型的注入相组合(匹配时反之亦然)。

在等值递归解释下，你提供的示例都是不同的。如果采用等价递归解释，则第一个和第三个示例相同，因为当你应用上述等式时，外部μ就会消失。

(*)编辑：一个不规则的递归类型是其无限扩展不对应于正常树形结构(或等效地，不能由有限循环图表示)的递归类型。这种情况只能用递归类型构造函数表示，即，在μ下出现的λ。例如，μα.λβ.1+α(β×β)——对应于递归方程t(β)=1+t(β×β)——将是不规则的，因为递归类型构造函数α被递归地应用于一个比其参数“更大”的类型，因此每个应用都是一个递归类型，它“不断增长”(因此，你不能将其绘制为图形)。

值得注意的是，在大多数具有μ的类型理论中，其绑定变量被限制为基本种类，因此根本无法表示不规则类型。特别是，具有不受限制的等价递归类型构造函数的理论将具有非终止类型规范化，因此类型等价性(因此类型检查)将是不可判定的。对于等值递归类型，你需要更高阶的roll/unroll，这是可能的，但我不知道有多少文献在研究它。

- Andreas Rossberg

---

那么不规则的类型必须包含一个λ吗？你能举个例子吗？ - user2023370

Answer 2

你的μ类型表达式是有效的。我相信你的类型也是规则的，因为你只使用了递归、求和和乘积。

类型是：

T1 = μγ.1+(μβ.1+γβ)γ

不等于

T2 = μβ.μγ.1+(1+γβ)γ

自从inr (inr (inl *, inr (inl *)), inl *)具有第二型但没有第一型以来。

最后一种类型。

T3 = μβ.μγ.1+(μβ.1+γβ)γ

等于（将第一个β转换为α）

μ_.μγ.1+(μβ.1+γβ)γ

展开顶层的μ。

μγ.1+(μβ.1+γβ)γ

这里的 T1 是什么意思？

基本上，μ-bound 变量的作用范围遵循与 λ-bound 变量相同的规则。也就是说，变量 β 的每次出现所对应的值由其上方最近的 μβ 提供。

- chi