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

Question

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

1. 这有正式的证据吗？

2. 简单的计算在 Scala 类型系统中会是什么样子？

3. 这对 Scala 这种语言有什么好处吗？与没有图灵完备类型系统的语言相比，这是否使 Scala 在某种程度上更加“强大”？

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

Answer 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实际上可以转换元素类型。那么，如果新的元素类型无法用原始集合类型表示，会发生什么情况呢？示例:a BitSet只能包含固定宽度的整数。那么，如果您有 BitSet[Short] 会发生什么？然后将每个数字映射到其字符串表示形式？

someBitSet map { _.toString() }

结果将是 BitSet[String] ，但那是不可能的。因此，Scala 选择 BitSet 的最派生父类(super class)型，可以容纳 String ，在本例中是 Set[String] .

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