问题标签 [hindley-milner]

我遇到了这个术语Hindley-Milner，我不确定是否理解它的含义。

我已阅读以下帖子：

• Steve Yegge -动态语言反击
• Steve Yegge - 匹诺曹问题
• Daniel Spiewak -什么是 Hindley-Milner？（为什么它很酷？）

但是在维基百科中没有这个术语的单一条目，通常会为我提供简明的解释。
^{注意-现在已添加一个}

它是什么？
什么语言和工具实现或使用它？
你能提供一个简洁的答案吗？

Hindley-Milner 是一种类型系统，它是许多著名的函数式编程语言类型系统的基础。Damas-Milner 是一种在 Hindley-Milner 类型系统中推断（推断？）类型的算法。

维基百科给出了算法的描述，据我所知，它相当于一个词：“统一”。这就是它的全部吗？如果是这样，那意味着有趣的部分是类型系统本身，而不是类型推断系统。

如果 Damas-Milner 不仅仅是统一，我想要一个 Damas-Milner 的描述，其中包括一个简单的示例，理想情况下，还有一些代码。

此外，这种算法通常被称为进行类型推断。它真的是一个推理系统吗？我以为这只是推断类型。

相关问题：

• 什么是欣德利米勒？
• 统一问题的类型推断

类型推断的限制是什么？哪些类型的系统没有通用推理算法？

在 Andrew Koenig 的关于 ML 类型推断的轶事中，作者使用归并排序的实现作为 ML 的学习练习，并且很高兴发现“不正确”的类型推断。

令我惊讶的是，编译器报告了一种

换句话说，这个排序函数接受任何类型的列表并返回一个整数列表。

那是不可能的。输出必须是输入的排列；它怎么可能有不同的类型？读者肯定会发现我的第一个冲动很熟悉：我想知道我是否在编译器中发现了一个错误！

再想一想，我意识到还有另一种方法可以让函数忽略它的参数：也许它有时根本不返回。事实上，当我尝试它时，这正是发生的事情：sort(nil)确实 return nil，但是对任何非空列表进行排序都会进入无限递归循环。

翻译成 Haskell 时

GHC 推断出类似的类型：

Damas-Hindley-Milner 算法如何推断这种类型？

我试图制作这个非常简单的 SML 函数的尾递归版本：

在此过程中，我在参数上使用了类型注释。下面的代码显示了这一点，并导致类型错误（如下所示），而如果我只是删除类型注释，SML 会毫无问题地接受它，为整个函数提供与上面更简单的函数相同的签名。

错误：

给出了两个错误。后者在这里似乎不太重要，suffixes_helper 的两个子句不匹配。第一个是我不明白的。我注释说第一个参数是 type 'a:list，第二个参数是 type 'b:list。'b:listHindley-Milner 类型推理算法不应该是建立在我理解的一般统一之上的，能够'a:list list使用 的替换来统一'b ---> 'a list吗？

编辑：答案表明它可能与不允许推断类型的类型推断算法有关，从某种意义上说，推断类型比类型注释给出的更严格。我猜想这样的规则只适用于参数和整个函数的注释。我不知道这是否正确。无论如何，我尝试将类型注释移动到函数体，我得到了同样的错误：

现在的错误是：

我正在寻找有关著名的Damas-Hindley-Milner 算法 的信息，以对功能语言进行类型推断，尤其是有关实现的信息。

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

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

阅读Scala 类型系统与 Haskell 的缺点？，我不得不问：具体来说，是什么让 Haskell 的类型系统比其他语言的类型系统（C、C++、Java）更强大。显然，即使 Scala 也无法执行与 Haskell 类型系统相同的功能。具体来说，是什么让 Haskell 的类型系统（Hindley-Milner 类型推断）如此强大？能给我举个例子吗？

我在做什么：我正在编写一个小型解释器系统，它可以解析文件，将其转换为一系列操作，然后将数千个数据集输入该序列以从中提取一些最终值。编译的解释器由一个带有两个参数的纯函数列表组成：一个数据集和一个执行上下文。每个函数都返回修改后的执行上下文：

type ('data, 'context) interpreter = ('data -> 'context -> 'context) list

编译器本质上是一个标记器，具有最终标记到指令的映射步骤，该步骤使用如下定义的映射描述：

type ('data, 'context) map = (string * ('data -> 'context -> 'context)) list

典型的解释器用法如下所示：

问题：我希望我的pocket_calc解释器可以使用任何支持add、方法sub和mul相应data类型的类（一个上下文类可以是整数，另一个可以是浮点数）。

然而，pocket_calc被定义为一个值而不是一个函数，因此类型系统不会使其类型成为泛型：第一次使用它时，'dataand'context类型被绑定到我首先提供的任何数据和上下文的类型，解释器变成永远与任何其他数据和上下文类型不兼容。

一个可行的解决方案是对解释器的定义进行 eta-expand 以允许其类型参数是通用的：

但是，由于以下几个原因，此解决方案是不可接受的：

• 每次调用它都会重新编译解释器，这会显着降低性能。即使是映射步骤（使用映射列表将令牌列表转换为解释器）也会导致明显的减速。

• 我的设计依赖于在初始化时加载的所有解释器，因为只要加载文件中的标记与映射列表中的行不匹配，编译器就会发出警告，我希望在软件启动时看到所有这些警告（而不是单独解释器最终运行）。

• 我有时想在几个解释器中重用给定的映射列表，无论是单独使用还是通过附加指令（例如，"div"）。

问题：除了eta-expansion，还有什么方法可以使类型参数化？也许是一些涉及模块签名或继承的巧妙技巧？如果这是不可能的，有没有办法缓解我上面提到的三个问题，以使 eta-expansion 成为可接受的解决方案？谢谢！

我正在开发一个用 Java 编写的简单的基于数据流的系统（想象它像一个 LabView 编辑器/运行时）。用户可以在编辑器中将块连接在一起，我需要类型推断以确保数据流图是正确的，但是，大多数类型推断示例都是用数学符号、ML、Scala、Perl 等编写的，我不会“说” ”。

我阅读了有关 Hindley-Milner 算法的信息，并发现这个文档有一个我可以实现的很好的例子。它适用于一组 T1 = T2 类似的约束。但是，我的数据流图转换为 T1 >= T2 类约束（或 T2 扩展 T1，或协方差，或 T1 <: T2，正如我在各种文章中看到的那样）。没有 lambda 只是类型变量（用于通用函数，如T merge(T in1, T in2)）和具体类型。

回顾 HM 算法：

如何更改原始 HM 算法以使用这些关系而不是简单的相等关系？Java-ish 示例或解释将不胜感激。

有人可以在以下 F# 程序中逐步解释类型推断：

我特别想逐步了解 Hindley Milner 的统一过程是如何运作的。