Scala 和 Haskell 拥有“图灵完备的类型系统”。通常，图灵完备性指的是computations and languages。它在类型上下文中的真正含义是什么？
有人能举例说明程序员如何从中受益吗？
PS 我不想比较 Haskell 和 Scala 的类型系统。更多的是关于一般术语。
PSS 如果可能的话，可以提供更多 Scala 示例。
【问题讨论】：
标签： scala haskell turing-complete
在类型的上下文中它的真正含义是什么？
这意味着类型系统中有足够的特征来表示任意计算。作为一个非常简短的证明，我在下面展示了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？）中，一个非常令人兴奋的编译时检查的代价是花费大量程序员的时间和精力来说服编译器你正在检查的东西是真实的——这通常都是很高的前期成本以及高昂的持续维护成本。
【讨论】：
Uppercase 字有不同的颜色，我会很高兴。但是，我也必须承认，我真的很不喜欢那些坚持给非关键字上色的荧光笔，比如print，就好像它们“特别”一样。