Scala中的类型系统是图灵完整的。证据？举例？福利？

Question

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

1. 有这方面的正式证据吗？
2. ，在Scala类型系统中，一个简单的计算会是什么样子？
3. ，这对Scala这种语言有什么好处吗？这是否使Scala在某种程度上比没有图灵完整类型系统的语言更“强大”呢？

我想这适用于一般的语言和类型系统。

Answer 1

在某个地方有一篇博客文章，其中包含了滑雪组合子演算的类型级实现，这是众所周知的图灵-完整的。

图灵-完全类型系统与图灵-完全语言有着相同的优点和缺点:你可以做任何事情，但你只能证明很少。特别是，你不能证明你最终会做些什么。

类型级计算的一个例子是Scala2.8中新的保持类型的集合变压器。在Scala2.8中，map、filter等方法被保证返回与调用它们相同类型的集合。因此，如果您filter a Set[Int]，您将得到一个Set[Int]，如果您返回一个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]。

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

Answer 2

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

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

最后，在Apocalisp的博客上有一个关于类型级编程的伟大的series of articles。