Haskell如何在系统F中添加图灵完备性？(How did Haskell add Turing

Haskell如何在系统F中添加图灵完备性？(How did Haskell add Turing-completeness to System F?)

我一直在阅读各种类型的系统和lambda计算结果，并且我看到lambda立方体中的所有类型lambda结石强烈归一化，而不是Turing等价。 这包括系统F，简单类型的lambda演算加多态性。

这导致我出现以下问题，对此我一直无法找到任何可理解的答案：

（例如）Haskell的形式主义与它表面上基于的演算有什么不同？ Haskell中的哪些语言功能不属于F系统形式？ 允许Turing完整计算所需的最小变化是多少？

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

I've been reading up on various type systems and lambda calculi, and i see that all of the typed lambda calculi in the lambda cube are strongly normalizing rather than Turing equivalent. This includes System F, the simply typed lambda calculus plus polymorphism.

This leads me to the following questions, for which I've been unable to find any comprehensible answer:

How does the formalism of (e.g.) Haskell differ from the calculus on which it is ostensibly based? What language features in Haskell don't fall within System F formalism? What's the minimum change necessary to allow Turing complete computation?

Thank you so much to whomever helps me understand this.

最满意答案

总之，一般递归。

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

没有原始的名字和递归概念。 事实上，纯系统F没有定义这样的东西的概念！

所以在Haskell中，这个单一定义是增加了turing的完整性

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概念， where or =强烈规范化，因为我们没有无限类型。 即使这个核心术语微积分也不是真正的系统F.系统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的关键，称为“让泛化”。

In a word, general recursion.

Haskell allows for arbitrary recursion while System F has no form of recursion. The lack of infinite types means fix isn't expressible as a closed term.

There is no primitive notion of names and recursion. In fact, pure System F has no notion of any such thing as definitions!

So in Haskell this single definition is what adds turing completeness

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

Really this function is indicative of a more general idea, by having fully recursive bindings, we get turing completeness. Notice that this applies to types, not just values.

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

With infinite types we can write the Y combinator (modulo some unfolding) and through it general recursion!

In pure System F, we often have some informal notion of definitions, but these are simply shorthands that are to be mentally inlined fully. This isn't possible in Haskell as this would create infinite terms.

The kernel of Haskell terms without any notion of let, where or = is strongly normalizing, since we don't have infinite types. Even this core term calculus isn't really System F. System F has "big lambdas" or type abstraction. The full term for id in System F is

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

This is because type inference for System F is undecidable! We explicitly notate wherever and whenever we expect polymorphism. In Haskell such a property would be annoying, so we limit the power of Haskell. In particular, we never infer a polymorphic type for a Haskell lambda argument without annotation (terms and conditions may apply). This is why in ML and Haskell

let x = exp in foo

isn't the same as

(\x -> foo) exp

even when exp isn't recursive! This is the crux of HM type inference and algorithm W, called "let generalization".