25

Scala 和 Haskell 有“图灵完备的类型系统”。通常，图灵完备性是指计算和语言。在类型的上下文中它的真正含义是什么？

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

PS 我不想比较 Haskell 和 Scala 的类型系统。它更多地是关于一般的术语。

PSS 如果可能有更多 Scala 示例。

4

1 回答 1

31

在类型的上下文中它的真正含义是什么？

这意味着类型系统中有足够的特性来表示任意计算。作为一个非常简短的证明，我在下面展示了微积分的类型级实现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？）中，一个非常令人兴奋的编译时检查的代价是花费大量程序员的时间和精力来说服编译器你正在检查的东西是真实的——这通常都是很高的前期成本以及高昂的持续维护成本。

于 2015-11-30T16:44:54.257 回答