类型推断器可以检测类型错误吗？

Question

我正在开发一个函数式编程语言的解释器，它使用Hindley-Milner类型的系统。

问题是，类型错误应该在哪里发生(被检测到)？

例如，如果我对一个类型为Bool -> Integer的函数应用Integer类型值，这显然是一个类型错误。类型推断器总是能检测到这个吗？

我的猜测是，类型推断器并不总是完全知道表达式的类型，即在推理过程中。因此，由类型推断器检测到的一些错误将是错误的，或者一些错误将不被检测到。

但是，表达式计算器应该正确地检测类型错误，因为计算器完全知道表达式的类型。

如果类型推断器不能正确检测类型错误，那么像OCaml这样的静态类型解释语言如何处理静态类型错误检查呢？

Answer 1

...类型错误。类型推断器总是能检测到这个吗？

如果你的类型推断是合理的，那么是的，它应该总是检测到错误。

特别是对于Hindley-Milner类型系统，该算法依赖于统一来找到主要类型。在没有的情况下，您将以统一错误结束。