问题标签 [hindley-milner]

当存在重载函数时，Hindley-Milner 算法如何工作？

以简单的形式（没有重载），它看起来很干净：

但我还没有找到任何关于它如何与重载函数一起工作的解释。

例如：我有 4 个“+”函数重载：

例子：

或复杂情况：

问题是我必须记住所有这些情况：

y2 案例引用 y1 案例，它看起来像一个方程式树，听起来很吓人。

这种算法是否有任何形式化？

我正在做学术练习（为了个人成长）。我想找到允许您定义能够接受自身（即指向自身的指针）作为参数的函数的编程语言。

例如，在 JavaScript 中：

上面的代码将在y达到零之前恰好执行foo() 11 次，从而导致递归终止。

我尝试在 OCaml 中定义一个类似的函数，如下所示：

但它因类型错误而失败：

我想知道，是否可以在 OCaml 中定义这样的函数？我对 OCaml 特别感兴趣，因为我知道它有一个全局类型推断系统。我想知道这些函数是否与全局类型推断兼容。因此，我正在寻找具有全局类型推断的任何语言中这些类型的函数的示例。

我试图理解关于类型推断的规则，因为我想将它融入我自己的语言中，并且本着这种精神，我一直在玩 F# 的类型推断，下面的内容让我觉得很奇怪。

这会编译，并且idis 'a -> 'a，这（如果我没记错的话）意味着每次调用都使用“新鲜”类型。

但是在使用运算符时，似乎第一次调用决定了该函数的签名。

在这里，mul被报告为int -> int -> int

如果我重新排序它们，那么mul是float -> float -> float：

你能解释一下（最好是非学术性的）规则是什么，也许从类型检查实现的角度来看它是如何工作的？每次引用它们时，它是否会遍历函数来检查它们的类型？还是有其他方法？

我已经看到了各种形式的问题“给定类型签名XXX，在 Haskell 中找到实现”。因此很自然地要问这是否可以概括或算法化。一个类似的问题是here。但是，很明显，通常这项任务是不可能的。所以下一个问题是用一些通用性换取实用性。

问题：如果所有类型签名都由刚性类型变量和一些约束组成，那么问题是否可以确定，这些约束是从一个固定的集合中提取的（例如Monad, Traversable, Foldable？）

一个典型的问题是，为了方便起见(Monad m) => (m j -> [m d]) -> m [j] -> [m [d]]，我使用了它[]而不是。(..Constraints t) => t

假设您有一个函数 f 将按如下方式使用：

关于 f 的类型，你能推断出什么？

它似乎是递归的，即f :: (ftype) -> int -> int。

假设我有A, B代表类型变量的字母，这些变量最初是未绑定的并a,b,c代表类型构造函数。然后我需要展示通过统一获得的类型变量的绑定（或者解释为什么失败）。

我得到了以下两种类型：

我有两个问题：

1）类型构造函数是什么意思？对我来说这个；a(A,b(c))，看起来像是a这里的类型构造函数，它是一个带有两个参数的函数。

2）有人可以告诉我他们会采取什么方法吗？我看这里来理解这个概念：http ://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-in​​ference/type-in​​ference.htm

是否有任何类型推断算法可以总是（或几乎总是）推断出正确的类型？我知道 Hindley Milner 算法可以在很多情况下做到这一点，但不是所有情况（即更高等级的多态类型）。

有人可以解释 Haskell 中的类型统一吗？例如：snd . snd :: (a1, (a2, c)) -> c

例子

我们如何到达 , (a1, (a2, c)) -> c, 从snd . snd?

在此先感谢您的帮助。

我一直在尝试使用 Hindley-Milner 算法构建一个类型系统，并遇到了以下挑战，我很好奇是否有任何资源或论文可以查看。

假设我有一种编程语言，它具有某种形式的属性访问器（类似javascript），它适用于数组和对象，数组括号内的属性需要是数字，对象括号内的属性需要成为一个字符串。

例如

假设我们想在下面的代码片段上使用hindley-milner

然后如果后来我们意识到这B是一个数字，那么我们立即推断 A 是一个数组。类似地，如果我们推断 A 是一个对象，那么 B 立即是一个数字。

是否有任何论文或类型系统具有这种条件替换概念？

我对类型推断还是很陌生，想知道是否有任何好的扩展或论文允许 HM 允许多个错误。

我可能会遗漏一些东西，但是如果出现统一错误，那么类型检查器是否可以在类型上下文“中毒”的情况下继续进行？