类型理论中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

您的?类型表达式有效.我相信你的类型也是常规的,因为你只使用递归,求和和产品.

类型

T1 = ??.1+(??.1+??)?

看起来不一样

T2 = ??.??.1+(1+??)?

因为inr (inr (inl *, inr (inl *)), inl *)有第二种但不是第一种.

最后一种

T3 = ??.??.1+(??.1+??)?

等于(α转换第一个β)

?_.??.1+(??.1+??)?

也就是说,展开顶级μ,

??.1+(??.1+??)?

是的T1.

基本上,μ-约束变量的范围遵循相同的λ-约束变量规则.也就是说,变量的每次出现的值?由最接近 ??的顶部提供.

Answer 2

μ的范围与其他绑定器没有区别,所以是的,所有示例都是有效的.它们也是常规的,因为它们甚至不包含λ.(*)

至于平等,这取决于你有什么样的μ型.基本上有两种不同的概念:

• equi-recursive:在这种情况下,输入规则假定等价

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

  即,递归类型被认为等于其一级"展开",其中μ被移除并且μ-约束变量被类型本身替换(并且因为该规则可以重复应用,所以可以多次展开任意).

• iso-recursive:这里不存在这样的等价.相反,μ型是一种单独的类型形式,具有自己的表达形式以引入和消除它 - 它们通常被称为滚动和展开(或折叠和展开),并且键入如下:

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

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

  这些必须明确地应用于术语级别以反映上面的等式(对于每个展开级别一次).

ML或Haskell等函数式语言通常使用后者来解释数据类型.但是,roll/unroll内置于数据构造函数的使用中.因此,每个构造函数都是一个iso-recursive类型的注入,注入一个sum类型(当匹配时反向).

在iso-recursive解释下,您的示例都是不同的.第一个和第三个在等效递归解释下是相同的,因为当应用上述等价时,外部μ只会消失.

(*)编辑:不规则递归类型是其无限扩展不对应于常规树(或等效地,不能用有限循环图表示)的类型.这种情况只能用递归型构造函数表示,即在 μ 下发生的λ .例如,μα.λβ.1+α(β×β) - 对应于递归方程t(β)= 1 + t(β×β) - 将是不规则的,因为递归类型构造函数α被递归地应用对于比其参数"更大"的类型,因此每个应用程序都是一个无限期"增长"的递归类型(因此,您无法将其绘制为图形).

然而值得注意的是,在μ的大多数类型理论中,其约束变量仅限于地面类型,因此根本不能表达不规则类型.特别是,具有不受限制的等递归类型构造函数的理论将具有非终止类型规范化,因此类型等价(因此类型检查)将是不可判定的.对于iso-recursive类型,你需要更高阶的滚动/展开,这是可能的,但我不知道有很多文献在研究它.