46

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

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

  • （例如）Haskell 的形式主义与它表面上基于的微积分有何不同？
  • Haskell 中的哪些语言特性不属于 System F 形式主义？
  • 允许图灵完成计算所需的最小更改是多少？

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

4

1 回答 1

52

总之，一般递归。

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

没有名称和递归的原始概念。事实上，纯系统 F 没有定义之类的概念！

所以在 Haskell 中，这个单一的定义是增加图灵完整性的原因

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

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

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，因为我们没有无限类型，所以它是强归一化的。即使是这个核心术语微积分也不是真正的系统 F。系统 F 具有“大 lambdas”或类型抽象。系统 F 中的全称是where=id

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

这是因为系统 F 的类型推断是不可判定的！无论何时何地，我们都明确指出我们期望多态性。在 Haskell 中这样的属性会很烦人，所以我们限制了 Haskell 的能力。特别是，我们从不为没有注释的 Haskell lambda 参数推断多态类型（可能适用条款和条件）。这就是为什么在 ML 和 Haskell

let x = exp in foo

不一样

(\x -> foo) exp

即使exp不是递归的！这是 HM 类型推断和算法 W 的症结所在，称为“让泛化”。

于 2014-08-12T03:08:55.803 回答