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

Question

Scala和Haskell拥有"图灵完整型系统".通常,图灵完整性是指计算和语言.它在类型的背景下真正意味着什么？

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

PS我不想比较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？)中,一个非常令人兴奋的编译时检查的代价是花费了大量的程序员时间和精力来说服编译器你正在检查的东西是真的 - 这通常都很高前期成本以及高额的持续维护成本.