是否有适用于所有情况的类型推理系统？答案

【问题标题】：Is there any type inference system that works in all cases?是否有适用于所有情况的类型推理系统？
【发布时间】：2020-04-01 00:35:15
【问题描述】：

是否有任何类型推断算法可以总是（或几乎总是）推断出正确的类型？我知道 Hindley Milner 算法可以在很多情况下做到这一点，但不是所有情况（即更高等级的多态类型）。

【问题讨论】：

任何认真的尝试都会让你早在成功之前就进入beza1e1.tuxen.de/articles/accidentally_turing_complete.html。
@btilly -- 能否请您了解一下您的意思？
在足够复杂的系统中，很容易意外发现可以对图灵机进行编码。在这一点上，您最终拥有编写任意程序的能力，并且不可能在所有情况下分析结果。例如，Rust、Haskell 和 Scala 的类型系统都是图灵完备的。这意味着你可以编写一个程序，甚至没有人知道它是否应该是可编译的。
@btilly -- 如果你不介意，你能举几个haskell的例子吗？
请参阅github.com/seliopou/typo，了解在 Haskell 类型系统中实现的编程语言。够好吗？

标签： algorithm type-inference hindley-milner

【解决方案1】：

您的问题并不完全恰当，因为“所有案例”的集合并不完全明确。

例如，您提到高级多态类型是 Hindley-Milner 类型推断不能总是推断出正确类型的情况，这是真的，除了标准 ML 和 Haskell 等语言使用 Hindley- Milner 类型推断并且没有更高级别的多态类型。事实上，Hindley-Milner 算法确实适用于 Hindley-Milner 类型系统所涵盖的所有情况。也就是说，Hindley-Milner 系统完全允许 Hindley-Milner 类型推断算法可以推断出的类型，因此在该系统中从不需要显式类型注释。

当然，使用 Hindley–Milner 的实际语言通常出于实用的原因以各种方式扩展系统，其中一些扩展会导致算法无法涵盖的情况。（例如，标准 ML 有一些内置的重载标识符，例如 + : real * real -> real 和 + : int * int -> int，这意味着程序员有时需要使用显式类型注释来选择正确的重载。）但这是一个设计决定，不是必需品；而且我注意到你在问题中没有提到任何现实世界的语言。

但从您的问题看来，您希望至少所有 Hindley-Milner 以及更高级别的多态类型。这意味着您需要至少全部 System F，即多态 lambda 演算。并且已知系统 F 中的类型推断是不可判定的。这意味着您的问题的答案是“否”：没有类型推断算法可以为您似乎想要的所有情况推断出正确的类型。

【讨论】：