问题描述
有人声称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[Whatever the return type of the anonymous function is]
.
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中的字体系统已完成图灵化.证明?例子?好处?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!