Scala 中的类型系统是图灵完备的。证明？例子？好处？答案

【问题标题】：The type system in Scala is Turing complete. Proof? Example? Benefits?Scala 中的类型系统是图灵完备的。证明？例子？好处？
【发布时间】：2011-05-02 03:25:19
【问题描述】：

有人声称 Scala 的类型系统是图灵完备的。我的问题是：

这有正式的证明吗？
简单的计算在 Scala 类型系统中是什么样子的？
这对 Scala 有什么好处吗？与没有图灵完备类型系统的语言相比，这是否让 Scala 在某些方面更“强大”？

我想这通常适用于语言和类型系统。

【问题讨论】：

我更喜欢使用非通用类型系统和快速编译器。
@ziggystar 您在编译速度方面获得的收益可能会在开发和调试时间中损失。

标签： language-agnostic scala type-systems turing-complete

【解决方案1】：

某处有一篇博客文章，其中包含 SKI 组合器演算的类型级实现，众所周知，它是图灵完备的。

图灵完备的类型系统与图灵完备的语言具有基本相同的优点和缺点：你可以做任何事情，但你能证明的很少。特别是，你无法证明你最终会做某事。

类型级计算的一个例子是 Scala 2.8 中新的类型保留集合转换器。在 Scala 2.8 中，map、filter 等方法保证返回与调用它们的类型相同的集合。所以，如果你 filter 和 Set[Int]，你会得到一个 Set[Int]，如果你是 map 一个 List[String]，你会得到一个 List[Whatever the return type of the anonymous function is]。

现在，如您所见，map 实际上可以转换元素类型。那么，如果新的元素类型不能用原来的集合类型来表示怎么办？示例：BitSet 只能包含固定宽度的整数。那么，如果您有一个 BitSet[Short] 并将每个数字映射到它的字符串表示，会发生什么？

someBitSet map { _.toString() }

结果会是BitSet[String]，但这是不可能的。因此，Scala 选择了派生最多的超类型BitSet，它可以容纳String，在本例中为Set[String]。

所有这些计算都在编译时间，或者更准确地说是在类型检查时间，使用类型级函数进行。因此，它静态地保证是类型安全的，即使类型是实际计算出来的，因此在设计时是未知的。

【讨论】：

我想这是您正在寻找的博客文章？ michid.wordpress.com/2010/01/29/… 。当我第一次看到 Scala 时，它似乎是一门简洁的语言。超类推理是一个真的很酷的功能。
很好的答案，虽然集合示例有点短。虽然类型检查器肯定会做一些有趣的启发式方法来在编译时获得最佳结果集合类型，但它不是类型级计算的一个很好的例子，因为类型系统 itself 并没有真正做任何事情工作。不幸的是（或者也许幸运的是），没有多少真实世界的代码可以进行实际的类型级编程，仅仅是因为它太难、太笨重且无法维护了。
感谢 Jörg 提供的出色示例和 Daniel 的澄清。现在我不敢问类型检查器是否是图灵完备的......

【解决方案2】：

我的blog post 在 Scala 类型系统中编码 SKI 演算显示了图灵完备性。

对于一些简单的类型级计算，还有一些关于如何编码自然数和加法/multiplication 的示例。

Apocalisp 的博客上终于有一篇关于类型级编程的精彩 series of articles。

【讨论】：

michid，这看起来令人印象深刻。我保证长大后会好好看看……这可能不是正式的证明，但它可能属于这个列表？ en.wikipedia.org/wiki/…
@Adrian，唯一已知的图灵完备的正式证明是实现其他图灵完备的能力。通常这意味着通用图灵机，但即使您使用其他已知的图灵完备的东西，如 SKI 演算或 Perl 或 Javascript，该理论仍然成立。因此，我认为这是一个正式的证明。
还应该注意的是，实际上没有什么可实现的，因为不可能有无限的内存。即使你用尽了宇宙中的所有物质来构建你的 CPU/解释器，它仍然不会真正完成图灵。我们实际上所说的图灵完备实际上是在可用内存的限制范围内实现图灵完备。