Haskell 类型系统的本质：静态/动态，手动/推断？答案

【问题标题】：The nature of Haskell type system: static/dynamic, manual/inferred?Haskell 类型系统的本质：静态/动态，手动/推断？
【发布时间】：2014-11-20 01:37:42
【问题描述】：

我正在学习 Haskell，并试图掌握 Haskell 类型系统的工作原理，重新确定事物的类型：动态、静态、手动设置、推断？

我懂一点的语言：

C、Java：由程序员手动设置，在编译时验证，如int i;，强类型（从字符串中减去整数是编译错误）。典型的静态类型系统。
Python：由运行时自动推断的类型（动态类型），强类型（从str 中减去int 会引发异常）。
Perl、PHP：在运行时自动推断类型（动态类型）、弱类型。
Haskell：类型通常在编译时自动推断（此类型或类型在编译时由程序员显式设置），强类型。

Haskell 的类型系统真的值得描述为“静态”吗？我的意思是自动类型推断不是（经典）静态类型。

【问题讨论】：

在文献中，“静态”意味着在编译时已知，所以是的。 “静态，推断”可能是最好的描述（或者也许"Hindley-Milner" 是最好的，这是静态推断系统的特定风格，与 SML 和 OCaml 以及少数其他语言共享）。
从字符串中减去整数不是 C 语言中的编译错误。
在我看来，动态类型是无法推断的。类型推断本质上是静态的。在运行时，您可以进行类型检查，但不能进行推理。

标签： haskell type-systems typing dynamic-typing static-typing

【解决方案1】：

Haskell 的类型系统真的值得描述为“静态”吗？我的意思是自动类型推断不是（经典）静态类型。

类型推断在编译时完成。在编译时检查所有类型。 Haskell 实现可能会在运行时擦除类型，因为它们具有类型安全的编译时证明。

所以说 Haskell 有一个“静态”类型系统是正确的。 “静态”是指编译时和运行时阶段区别的一方面。

引用罗伯特·哈珀的话：

大多数编程语言在处理的静态和动态阶段。静态阶段包括解析和类型检查以确保程序格式正确；动态阶段包括执行格式良好的程序。一种当格式良好的程序运行良好时，语言被认为是安全的执行时的行为。

来自Practical Foundations for Programming Languages，2014 年。

根据这种描述，Haskell 是一种具有静态类型系统的安全语言。

作为旁注，我强烈向那些有兴趣学习了解编程语言及其功能的基本技能的人推荐上述书籍。

【讨论】：

【解决方案2】：

静态-动态轴和手动推断（或清单推断）的比例不是正交的。静态类型系统可以是明显的或推断的，区别不适用于动态类型。 Python、Perl、PHP 不推断类型，因为类型推断是通过静态分析（即在编译时）推断静态类型。

动态语言不会这样推断类型，它们只是在实际计算的同时计算值的类型。 Haskell 确实会静态推断类型，它是静态类型的，您不必手动编写静态类型。它的类型系统确实与主流类型系统不同，但它的不同之处在于推断而不是表现（以及许多其他特性），而不是不是静态的。

至于强/弱类型：Stop using that term，它被重载到了无用的地步。如果“类型系统强/弱”的意思是“类型系统允许/禁止 X”，那么就说 that，因为如果你称它为强/弱，则键入大部分受众会有不同的定义，并且不同意您对这些术语的使用。此外，正如您所看到的，对于 X 的大多数选择，它与您在标题中提到的两个区别相当独立（但是还有相当大的群体使用强作为静态的同义词和弱作为动态的同义词，哦，我的！）。

【讨论】：

【解决方案3】：

在去 SO 之前，最好检查一下，例如维基百科，其中说“Haskell 有一个基于 Hindley-Milner 类型推断的强大的静态类型系统。”静态是指何时完成类型检查，因此类型是否被推断并不重要。

【讨论】：