type-inference - ML 中类型推断的局限性

Question

我读过一些在行业中使用 ML 的人的轶事，他们说经常遇到类型推断限制并且必须在他们的程序中使用显式类型注释。谁能给出 ML 的类型推断在哪里遇到问题的明确示例，并可能解释这些限制是否与不可判定性有关？

Answer 1

我现在不能举一个例子（我已经几个月没有在 Ocaml 中编码了），但在实践中可能发生的情况是当你犯了类型错误时（即传递了错误类型的参数），尤其是在使用 high -order 函数，类型错误消息的发生可能与您真正的错误相去甚远。

为了缓解这种情况，我养成了显式键入大多数内部顶级函数的习惯，例如

let f (x: int) : string = 

Answer 2

可能是这个问题/答案的副本。快速回答：Hindley/Milner 类型推断（在 ML 中使用）仅限于 rank-1 多态性，也就是说，多态类型是类型系统的二等公民，例如函数参数本身不能是多态的。众所周知，更高级别的多态性（如 System F 又名多态 lambda 演算）的类型推断是不可判定的。