是否有任何类型推断算法可以总是（或几乎总是）推断出正确的类型？我知道 Hindley Milner 算法可以在很多情况下做到这一点，但不是所有情况（即更高等级的多态类型）。
1 回答
1
您的问题并不完全恰当，因为“所有案例”的集合并不完全明确。
例如，您提到高阶多态类型是 Hindley-Milner 类型推断不能总是推断出正确类型的情况，这是真的，除了标准 ML 和 Haskell 等语言使用 Hindley-Milner 类型推断并且没有更高级别的多态类型。事实上，Hindley-Milner 算法确实适用于 Hindley-Milner 类型系统所涵盖的所有情况。也就是说，Hindley-Milner 系统完全允许 Hindley-Milner 类型推断算法可以推断出的类型，因此在该系统中从不需要显式类型注释。
当然，使用 Hindley-Milner 的实际语言通常出于实用的原因以各种方式扩展系统，其中一些扩展会导致算法无法涵盖的情况。（例如，标准 ML 有一些内置的重载标识符，例如+ : real * real -> realand + : int * int -> int，这意味着程序员有时需要使用显式类型注释来选择正确的重载。）但这是设计决策，而不是必需的；而且我注意到无论如何您都没有在问题中提及任何现实世界的语言。
但是从您的问题看来，您至少需要所有 Hindley-Milner 以及更高级别的多态类型。这意味着您至少需要所有System F，即多态 lambda 演算。众所周知，系统 F 中的类型推断是不可判定的。这意味着您的问题的答案是“否”：没有类型推断算法可以为您似乎想要的所有情况推断出正确的类型。
于 2020-04-02T04:30:39.070 回答