Haskell 的类型系统是 Curry 风格还是 Church 风格？

在研究 Haskell 的类型系统时，我遇到了 Curry 风格和 Church 风格这两个术语。我想了解它们之间的区别。

  • Curry 风格是一种类型信息位于程序外部的系统，执行程序时无需进行类型检查。编译器会自动推断类型，而无需显式类型注释。
  • Church 风格是一种将类型集成到语言语义中的系统。类型注释是强制性的，还会执行类型推断。鉴于 Haskell 的类型系统包含类型推断，并且类型注释不是强制性的，我最初认为它应该归类为 Curry 风格。然而，一些文献表明它也具有 Church 风格的特征。

Haskell 的类型系统应该被认为是 Curry 风格还是 Church 风格？另外，您能解释一下您的看法吗？

1

  • 3
    我认为这些术语主要用于描述从理论角度研究语言的不同方法。举个例子：如果你在证明助手（如 Coq 或 Agda）中讨论编程语言的属性，你可以将其设置为，你可以讨论的每个术语都必须是类型良好的。这是一种“内在类型”。但你也可以将其设置为允许类型错误的术语，并且你稍后只会将它们限制为类型良好的术语。这是一种“外在类型”。但请注意，我们正在研究的语言并没有改变。


    – 



最佳答案
2

Haskell 的类型系统是 Haskell 风格的。事实证明，可能性不止两种！

总体来说，我倾向于像使用 curry 风格的系统一样与它交互。但还是存在一些显著差异：

  • 在许多情况下，可以推断出程序所需的所有类型信息。但在很多情况下，需要类型注释来指导推理引擎；示例包括多态递归、模糊类型类用法、高阶类型、类型系列恶作剧和 GADT。
  • 在大多数情况下，类型检查对于执行程序而言是必需的。评估程序的一部分涉及选择类型类实例，如果没有类型检查，则无法可靠地完成此操作。
  • 将类型声明附加到顶级定义的原因有

2

  • 1
    +1。如果这种区别是 Church 和 Curry 风格的类型系统，主要在于类型是否明显是强制性的，那么我认为它对 Haskell 的分类不是一个非常有用的轴。使用类型类，所选类型甚至会影响程序的实际功能！您可以制作两个程序，它们都可以成功编译和执行，仅在类型上有所不同，并且执行不同的操作。写下类型通常是可选的（至少在“原始”Haskell 中），因此它们很容易完全不可见，但在我看来，类型的概念是语言语义的牢固组成部分。


    – 

  • 感谢您的回复和解释。我很欣赏您的见解。我很清楚 Haskell 拥有两种类型系统的元素，从而形成了其独特的风格。您的回答非常有帮助。谢谢。


    – 

最初应用于 lambda 演算的 Church 风格类型确实包括绑定器上的显式类型注释。但如今，“Church 风格”主要指内在类型，而这正是 Haskell 所拥有的。每个术语和变量都只有一个内在类型，错误类型的代码作为程序没有定义的含义。

添加类型推断并不一定会改变类型系统，它只是为您重建一些类型注释。

同样，现在 Curry 式类型通常意味着外部类型，其中程序具有独立于类型检查的含义。给定术语可能有多种有效类型，其中没有一种是最通用的，并且类型的选择不会改变语义。这就是为什么它在其原始的 lambda 演算环境中不需要类型注释的原因。

在定义语言时假设了内在类型。它不仅指出了“静态错误发生的时间”，而且某些语言特性（例如模式匹配和类型类）的语义也是根据内在类型定义的。

GHC 的延迟类型错误 ( -fdefer-type-errors) 似乎可以让您运行部分定义的程序。但是，如果表达式有类型错误，它仍然不会产生值，因此这不会改变类型的性质 – 它只是用类型良好的术语替换代码中一些不可类型化的部分，以便throw (TypeError "…")制作一个类型良好的程序。

1

  • 感谢您的回复。我理解 Haskell 主要被认为是 Church 风格，因为它具有内在类型，这与我的理解一致。虽然类型理论的最新发展可能会使简单的分类变得不那么合适，但我相信这种区别对于概念清晰度仍然很重要。您的回复非常有帮助。谢谢。


    –