haskell - Haskell 如何为 System F 添加图灵完备性？

Question

我一直在阅读各种类型系统和 lambda 演算，我发现 lambda 立方体中的所有类型化 lambda 演算都是强标准化，而不是图灵等价物。这包括 System F、简单类型的 lambda 演算加上多态性。

这让我想到了以下问题，但我一直无法找到任何可以理解的答案:

• (例如)Haskell 的形式主义与其表面上所基于的微积分有何不同？
• Haskell 中的哪些语言功能不属于 System F 形式主义？
• 允许图灵完成计算所需的最小更改是什么？

非常感谢任何帮助我理解这一点的人。

Answer 1

总而言之，就是一般递归。

Haskell 允许任意递归，而 System F 没有任何形式的递归。缺乏无限类型意味着 fix 无法表达为封闭术语。

不存在名称和递归的原始概念。事实上，纯系统 F 没有任何定义之类的概念!

因此，在 Haskell 中，这个单一定义增加了图灵完备性

fix :: (a -> a) -> a
fix f = let x = f x in x

实际上，这个函数代表了一个更普遍的想法，通过完全递归绑定(bind)，我们获得了图灵完备性。请注意，这适用于类型，而不仅仅是值。

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

使用无限类型，我们可以编写 Y 组合器(对某些展开求模)并通过它进行一般递归!

在纯系统 F 中，我们经常有一些非正式的定义概念，但这些只是需要在头脑中完全内嵌的简写。这在 Haskell 中是不可能的，因为这会产生无限项。

Haskell 术语的核心没有任何 let、where 或 = 的概念是强规范化的，因为我们没有无限的类型。甚至这个核心术语微积分也不是真正 System F。System F 具有“大 lambda”或类型抽象。系统 F 中 id 的完整术语是

id := /\ A -> \(x : A) -> x

这是因为系统 F 的类型推断是不可判定的!无论何时何地，我们都会明确指出我们期望多态性。在 Haskell 中，这样的属性会很烦人，因此我们限制 Haskell 的功能。特别是，我们永远在没有注释的情况下推断 Haskell lambda 参数的多态类型(条款和条件可能适用)。这就是 ML 和 Haskell 中的原因

let x = exp in foo

不与

相同

(\x -> foo) exp

即使 exp 不是递归的!这就是HM类型推断和算法W的关键，称为“let泛化”。