Scala 中的类型系统是图灵完备的。证明？例子？好处？
有人声称 Scala 的类型系统是图灵完备的。我的问题是：
这有正式的证明吗？
简单计算在 Scala 类型系统中是什么样子？
这对 Scala 这种语言有什么好处吗？与没有图灵完整类型系统的语言相比，这是否使 Scala 在某种程度上更加“强大”？
我想这通常适用于语言和类型系统。
There are claims that Scala's type system is Turing complete. My questions are:
Is there a formal proof for this?
How would a simple computation look like in the Scala type system?
Is this of any benefit to Scala - the language? Is this making Scala more "powerful" in some way compared languages without a Turing complete type system?
I guess this applies to languages and type systems in general.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
有一篇博客文章介绍了 SKI 组合器演算的类型级实现，众所周知，它是图灵完备的。
图灵完备类型系统与图灵完备语言具有基本相同的优点和缺点：你可以做任何事情，但你可以证明的很少。特别是，你无法证明你最终会真正做某事。
类型级计算的一个例子是 Scala 2.8 中新的类型保留集合转换器。在 Scala 2.8 中，
map、filter等方法保证返回与调用它们的类型相同的集合。因此，如果您过滤一个Set[Int]，您会得到一个Set[Int]，并且如果您映射List[String]你会得到一个List[无论匿名函数的返回类型是什么]。现在，如您所见，
map实际上可以转换元素类型。那么，如果新的元素类型无法用原始集合类型表示，会发生什么情况呢？示例：BitSet只能包含固定宽度的整数。那么，如果您有一个 BitSet[Short] 并且将每个数字映射到其字符串表示形式，会发生什么情况？结果将是一个
BitSet[String]，但这是不可能的。因此，Scala 选择BitSet的最派生超类型，它可以保存String，在本例中是Set[String]。所有这些计算都是在编译时期间进行的，或者更准确地说是在类型检查时期间使用类型级函数进行的。因此，它静态地保证类型安全，即使类型实际上是计算出来的，因此在设计时是未知的。
There is a blog post somewhere with a type-level implementation of the SKI combinator calculus, which is known to be Turing-complete.
Turing-complete type systems have basically the same benefits and drawbacks that Turing-complete languages have: you can do anything, but you can prove very little. In particular, you cannot prove that you will actually eventually do something.
One example of type-level computation are the new type-preserving collection transformers in Scala 2.8. In Scala 2.8, methods like
map,filterand so on are guaranteed to return a collection of the same type that they were called on. So, if youfilteraSet[Int], you get back aSet[Int]and if youmapaList[String]you get back aList[Whatever the return type of the anonymous function is].Now, as you can see,
mapcan actually transform the element type. So, what happens if the new element type cannot be represented with the original collection type? Example: aBitSetcan only contain fixed-width integers. So, what happens if you have aBitSet[Short]and you map each number to its string representation?The result would be a
BitSet[String], but that's impossible. So, Scala chooses the most derived supertype ofBitSet, which can hold aString, which in this case is aSet[String].All of this computation is going on during compile time, or more precisely during type checking time, using type-level functions. Thus, it is statically guaranteed to be type-safe, even though the types are actually computed and thus not known at design time.
我关于编码 SKI 的博客文章 Scala 类型系统中的微积分显示了图灵完备性。
对于一些简单的类型级别计算，还有一些关于如何对自然数和加法进行编码的示例/乘法。
最后，还有关于类型级别编程的精彩系列文章在 Apocalisp 的博客上。
My blog post on encoding the SKI calculus in the Scala type system shows Turing completeness.
For some simple type level computations there are also some examples on how to encode the natural numbers and addition/multiplication.
Finally there is a great series of articles on type level programming over on Apocalisp's blog.