Damas-Hindley-Milner 类型推理算法实现答案

【问题标题】：Damas-Hindley-Milner type inference algorithm implementationDamas-Hindley-Milner 类型推理算法实现
【发布时间】：2010-09-04 11:01:59
【问题描述】：

我正在寻找有关知名Damas-Hindley-Milner algorithm 的信息对函数式语言进行类型推断，尤其是有关实现的信息。

我已经知道如何处理Algorithm W，但我听说了最近基于约束生成器/求解器而不是通常的统一的新算法。但是，我找不到任何关于这些新算法的实现的讨论。

知道在哪里可以找到有关 ML 推理的部分信息吗？

【问题讨论】：

您确定约束生成/解决不适用于具有子类型的类型系统，例如HM(X) 家族之一（由子类型关系参数化的 Hindley-Milner）？
我读到它可以用于带有子类型的 HM(X) 系列，也可以用于类型类（参数多态）之类的东西，所以我有点困惑
类型类与参数多态性有些正交。我认为 Pascal Cuoq 可能是正确的。例如，我不确定在标准 ML 中我是否看到过任何可以替代普通 ol' 约束生成和统一用于类型重构的严肃替代方案。不过，替代方法对于已经提出的扩展类型肯定会变得有用。
自从您询问 ML 以来，答案不是 100%，但我想知道您是否听说过：Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism，Gerg˝ 博士o 埃尔迪gergo.erdi.hu/projects/tandoori/…。正如你可能从“typeclass”这个词的出现中猜到的那样，这是关于 Haskell 的。

【解决方案1】：

如果您对 ML 代码感到满意，那么找到这些东西的最佳方法就是简单地查看实际的实现。 HaMLet 是一个很好的参考实现，它被设计为更多的测试平台而不是生产实现。

最近几乎所有关于这些问题的严肃讨论都将在学术场所进行。一篇可能感兴趣的论文是Generalising Hindley-Milner type inference algorithms。

此外，在 Pierce 的“Types and Programming Languages”和 Appel 的“Modern Compiler Implementation in ML”中，各种类型系统（包括 let 多态性）的实现比算法 W 的普通描述更接近实现这一点的现代方法。

【讨论】：