Adr*_*ian 55 language-agnostic type-systems scala turing-complete
有人声称Scala的类型系统是图灵完整的.我的问题是:
这有正式的证据吗？
如何在Scala类型系统中进行简单的计算？
这对Scala有什么好处 - 语言？这是否使Scala在某种程度上比没有图灵完整类型系统的语言更"强大"？
我想这通常适用于语言和类型系统.
Jör*_*tag 37
某个博客文章中有一个SKI组合子微积分的类型级实现,已知它是图灵完备的.
图灵完整型系统具有与图灵完整语言基本相同的优点和缺点:你可以做任何事情,但你可以证明很少.特别是,你不能证明你最终会做某事.
类型级计算的一个示例是Scala 2.8中新的类型保留集合变换器.在斯卡拉2.8,类似的方法map,filter等等,保证返回,他们呼吁同一类型的集合.所以,如果你filter是a Set[Int],你就会回来Set[Int],如果你map是a,List[String]你就会回来List[Whatever the return type of the anonymous function is].
现在,正如您所看到的,map实际上可以转换元素类型.那么,如果新元素类型无法用原始集合类型表示会发生什么？示例:a BitSet只能包含固定宽度的整数.那么,如果你有一个BitSet[Short]并且你将每个数字映射到它的字符串表示会发生什么？
someBitSet map { _.toString() }
结果将是a BitSet[String],但这是不可能的.因此,Scala选择了最大的派生类型BitSet,它可以容纳一个String,在这种情况下是一个Set[String].
所有这些计算都是在编译期间进行的,或者更准确地说是在类型检查时,使用类型级函数.因此,静态地保证它是类型安全的,即使这些类型实际上是计算的并且因此在设计时不知道.
mic*_*hid 34
我在Scala类型系统中编写SKI演算的博客文章显示了图灵的完整性.
对于一些简单的类型级计算,还有一些关于如何编码自然数和加法/ 乘法的例子.
最后,在Apocalisp的博客上有一系列关于类型级编程的文章.