类型论中 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+γβ)γ

以上都是正则类型吗？

Answer 1

μ的作用域与其他活页夹没有什么不同，所以是的，你所有的例子都是有效的。它们也是正则的，因为它们甚至不包含 λ。 (*)

至于相等，这取决于你有什么样的 μ-types。基本上有两种不同的概念：

• 等递归：在这种情况下，输入规则假定等价

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

  即，递归类型被认为等于它的一级“展开”，其中 μ 被删除，μ 绑定变量被类型本身替换（并且因为该规则可以重复应用，所以可以展开任意多次）。

• iso-recursive：这里不存在这样的等价性。取而代之的是，μ-type 是一种单独的类型形式，它有自己的表达形式来引入和消除它——它们通常被称为 roll 和 unroll（或 fold 和展开），类型如下：

  滚动：T[μα.T / α] → μα.T

  展开：μα.T → T[μα.T / α]

  这些必须明确应用于术语级别以反映上述等式（每个展开级别一次）。

像 ML 或 Haskell 这样的函数式语言通常使用后者来解释数据类型。但是，滚动/展开是内置在数据构造函数的使用中的。因此，每个构造函数都是对等递归类型的注入，由对 sum 类型的注入组成（匹配时相反）。

在等递归解释下，您的示例都是不同的。第一个和第三个在等递归解释下是相同的，因为当您应用上述等价时，外部 μ 就消失了。

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

然而值得注意的是，在大多数带有 μ 的类型理论中，它的界变量仅限于基类，因此根本不能表达不规则类型。特别是，具有不受限制的等递归类型构造函数的理论将具有非终止类型规范化，因此类型等价（以及类型检查）将是不可判定的。对于 iso-recursive 类型，您需要更高阶的滚动/展开，这是可能的，但我不知道有多少文献研究它。

Answer 2

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

类型

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

看起来不等于

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

因为inr (inr (inl *, inr (inl *)), inl *) 有第二种但没有第一种。

最后一种

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

等于（α-转换第一个β）

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

也就是展开顶层μ，

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

这是T1。

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