问题描述
有人声称 Scala 的类型系统是图灵完备的.我的问题是:
There are claims that Scala's type system is Turing complete. My questions are:
这有正式的证明吗?
Is there a formal proof for this?
一个简单的计算在 Scala 类型系统中会是什么样子?
How would a simple computation look like in the Scala type system?
这对 Scala - 语言有什么好处吗?与没有图灵完备类型系统的语言相比,这是否让 Scala 在某些方面更强大"?
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.
推荐答案
某处有一篇博客文章,其中介绍了 SKI 组合子演算的类型级实现,该算法被称为图灵完备.
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.
类型级计算的一个例子是 Scala 2.8 中新的类型保留集合转换器.在 Scala 2.8 中,map
、filter
等方法保证返回与调用它们相同类型的集合.所以,如果你filter
一个Set[Int]
,你会得到一个Set[Int]
,如果你map
> 一个 List[String]
你得到一个 List[无论匿名函数的返回类型是什么]
.
One example of type-level computation are the new type-preserving collection transformers in Scala 2.8. In Scala 2.8, methods like map
, filter
and so on are guaranteed to return a collection of the same type that they were called on. So, if you filter
a Set[Int]
, you get back a Set[Int]
and if you map
a List[String]
you get back a List[Whatever the return type of the anonymous function is]
.
现在,如您所见,map
实际上可以转换元素类型.那么,如果新元素类型不能用原始集合类型表示,会发生什么?示例:BitSet
只能包含固定宽度的整数.那么,如果你有一个 BitSet[Short]
并且你将每个数字映射到它的字符串表示会发生什么?
Now, as you can see, map
can actually transform the element type. So, what happens if the new element type cannot be represented with the original collection type? Example: a BitSet
can only contain fixed-width integers. So, what happens if you have a BitSet[Short]
and you map each number to its string representation?
someBitSet map { _.toString() }
结果将是一个BitSet[String]
,但这是不可能的.因此,Scala 选择了 BitSet
的最派生超类型,它可以保存一个 String
,在本例中是一个 Set[String]
.
The result would be a BitSet[String]
, but that's impossible. So, Scala chooses the most derived supertype of BitSet
, which can hold a String
, which in this case is a Set[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.
这篇关于Scala 中的类型系统是图灵完备的.证明?例子?好处?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!