Scala中的types系统是图灵完整的。 certificate？ 例？ 好处？
有声称斯卡拉的types系统是图灵完整。 我的问题是：
-
有没有正式的证据呢？
-
Scalatypes系统中的简单计算如何？
-
这对Scala有什么好处 – 语言？ 这是否使得Scala在某种程度上比没有图灵完整types系统的语言更“强大”？
我想这一般适用于语言和types系统。
有一个博客文章的SKI combinator演算的types级别的实现，这是已知的图灵完成。
图灵完全型系统与图灵完备语言具有基本相同的优点和缺点：你可以做任何事情，但你可以certificate很less。 特别是，你不能certificate你实际上最终会做些什么。
types级计算的一个例子是Scala 2.8中的新型保存收集变换器。 在Scala 2.8中，像map ， filter等方法保证返回一个与它们被调用的相同types的集合。 所以，如果你filter一个Set[Int] ，你会得到一个Set[Int] ，如果你map一个List[String]你将得到一个List[Whatever the return type of the anonymous function is] 。
现在，正如您所看到的， map可以实际转换元素types。 那么，如果新的元素types不能用原始的集合types表示，会发生什么？ 例如：一个BitSet只能包含固定宽度的整数。 那么，如果你有一个BitSet[Short]并将每个数字映射到它的string表示，会发生什么？
someBitSet map { _.toString() }
结果将是一个BitSet[String] ，但这是不可能的。 所以，Scalaselect了BitSet派生超types，它可以容纳一个String ，在这个例子中是一个Set[String] 。
所有这些计算都是在编译期间进行的 ，或者在types检查时更精确地使用types级函数。 因此，即使types是实际计算出来的，因此在devise时不知道它是静态保证是types安全的。
我在Scalatypes系统中编写SKI演算的博客文章显示了Turing的完整性。
对于一些简单的types级别的计算，还有一些关于如何编码自然数和加法/ 乘法的例子。
最后，在Apocalisp的博客上有一系列关于types级编程的文章。
