图灵完备型系统的原因是什么

Question

Scala和Haskell都有"图灵完备型系统"。通常，图灵完备性指的是计算和语言。在类型的上下文中，它到底意味着什么？

有人能举一个程序员如何从中受益的例子吗？

附言：我不想比较Haskell和Scala的类型系统。它更多的是关于这个术语的一般性。

PSS如果可能的话还有更多Scala的例子。

Answer 1

在类型的上下文中，它到底意味着什么？

这意味着类型系统中有足够的特征来表示任意计算。作为一个非常简短的证明，我在下面介绍了SK演算的类型级实现；有很多地方讨论这个微积分的图灵完备性及其含义，所以我不在这里重复了。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
infixl 1 `App`
data Term = S | K | App Term Term
type family Reduce t where
    Reduce S = S
    Reduce K = K
    Reduce (S `App` x `App` y `App` z) = Reduce (x `App` z `App` (y `App` z))
    Reduce (K `App` x `App` y) = Reduce x
    Reduce (x `App` y) = Reduce (Reduce x `App` y)

你可以在ghci提示下看到这一点；例如，在SK演算中，术语SKSK（最终）减少为仅K:

> :kind! Reduce (S `App` K `App` S `App` K)
Reduce (S `App` K `App` S `App` K) :: Term
= 'K

这里也有一个有趣的尝试：

> type I = S `App` K `App` K
> type Rep = S `App` I `App` I
> :kind! Reduce (Rep `App` Rep)

我不会破坏乐趣的——你自己试试吧。但首先要知道如何终止带有极端偏见的节目。

有人能举一个程序员如何从中受益的例子吗？

任意类型级计算允许您在类型上表达任意不变量，并让编译器（在编译时）验证它们是否被保留。想要一棵红黑树吗？编译器可以检查的红黑树是否保留了红黑树不变量？这会很方便，对吧，因为这排除了一整类实现错误？对于静态已知的匹配特定模式的XML值的类型如何？事实上，为什么不更进一步，写下一个参数化类型，其参数表示模式？然后，您可以在运行时读取模式，并让编译时检查确保您的参数化值只能表示该模式中格式良好的值。美好的

或者，也许是一个更平淡无奇的例子：如果你想让编译器检查你是否从未用不存在的关键字为词典编制索引，该怎么办？有了足够先进的类型系统，你就可以了。

当然，总有代价的。在Haskell（可能还有Scala？）中，一次非常令人兴奋的编译时检查的代价是花费程序员大量的时间和精力来说服编译器你正在检查的事情是真的——这通常既是高昂的前期成本，也是高昂的持续维护成本。