57

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

  1. 有正式的证明吗？

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

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

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

4

2 回答 2

39

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

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

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

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

someBitSet map { _.toString() }

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

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

于 2010-10-28T22:44:22.467 回答
34

我关于在 Scala 类型系统中编码 SKI 演算的博文展示了图灵完备性。

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

最后，Apocalisp 的博客上有一系列关于类型级编程的精彩文章。

于 2010-10-29T10:02:55.743 回答