Scala – 图灵完整型系统的原因是什么？

What does it really mean in the context of types?

这意味着类型系统具有足够的特征来表示任意计算。作为一个非常短的证据，我在下面提出了一个类型级别的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)

我不会破坏乐趣 – 自己尝试。但是首先要知道如何终止极端偏见的方案。

Could some one give an example how a programmer can benefit from it?

任意类型级别计算允许您在类型上表达任意不变量，并使编译器在编译时验证它们被保留。想要一个红黑色的树？编译器可以检查的红黑树如何保存红黑树不变量？那将是方便的，对，因为这排除了一整套的实现bug？一个静态地知道匹配特定模式的XML值的类型呢？事实上，为什么不进一步，写下参数表示一个模式的参数化类型？然后，您可以在运行时读取模式，并且您的编译时检查保证您的参数化值只能表示该模式中的格式正确的值。太好了！

或者，也许是一个更平淡的例子：如果你想让你的编译器检查你没有使用不在那里的键索引您的字典怎么办？拥有足够高级的系统，您可以。

当然，总有一个价格。在Haskell(可能是Scala？)中，一个非常令人兴奋的编译时检查的价格是花费大量程序员的时间和精力来说服编译器，你正在检查的东西是真实的 – 这通常都是高前期成本以及持续的维护成本。