OCaml 类型的推理算法是如何工作的？答案

【问题标题】：How does the OCaml type inferencing algorithm work?OCaml 类型的推理算法是如何工作的？
【发布时间】：2012-10-05 04:15:50
【问题描述】：

我目前正在学习 OCaml，我很好奇 OCaml 如何进行类型推断。我知道这是通过一个称为统一的过程完成的，我尝试在已发表的论文中阅读有关该算法的信息，但符号让我失望。谁能帮我描述一下分步过程？

【问题讨论】：

和 Prolog 中的一模一样。并且有很多关于 Prolog 的优秀教科书可供选择。事实上，Hindley-Milner 算法最简单的实现是通过生成 Prolog 方程，然后使用某种嵌入式 Prolog 实现来求解它们。

【解决方案1】：

实际上，可以说统一是算法的一个实现细节。类型系统只是一组规则。规则允许检查现有的类型推导。规则没有明确提到统一，尽管统一是一种在考虑实现自动从表达式生成类型推导的算法时自然会想到的技术。

当我和你有同样的问题时，我真的很喜欢阅读这篇“使用 Caml Light 进行函数式编程”tutorial by Michel Mauny。该教程现在显示了它的年龄，但是您感兴趣的章节（第 15 章）现在仍然和以前一样好。

【讨论】：

【解决方案2】：

学习 ML 中的 HM 类型推断的规范参考可能是 Ben Pierce 的“类型和编程语言”。您可以在该书的第 22 章中找到该主题。

类型推断算法的第一个实例称为Algorithm W。

但是，您可能会惊讶地发现——事实上——OCaml 的实现并不简单地生成约束并解决它们！事实上，它为类型推断提供了一种更有效的基于图的算法，该算法（虽然速度很快）会导致偶尔报告奇怪的类型错误。您可以查看有关解释 ML 中的类型错误的参考资料。

【讨论】：