本文介绍了Scala 中的类型系统是图灵完备的.证明?例子?好处?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

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

There are claims that Scala's type system is Turing complete. My questions are:

  1. 这有正式的证明吗?

  1. 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 中,mapfilter 等方法保证返回与调用它们相同类型的集合.所以,如果你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 中的类型系统是图灵完备的.证明?例子?好处?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

09-02 10:51