问题标签 [hindley-milner]

这是我对这个问题的看法。任何人都可以确认、否认或详细说明吗？

我写道：

Scala 没有将协变与分配 给List[A]的 GLB ⊤统一起来，bcz afaics 在子类型化“biunification”</a> 中分配的方向很重要。因此必须有类型（即），同上类型不能分别接受来自or的赋值。因此，价值限制问题起源于无方向的统一，并且在最近的上述研究之前，全球双统一被认为是不可判定的。 List[Int]NoneOption[⊥]Option[Nothing]NilList[Nothing]Option[Int]List[Int]

您可能希望查看上述评论的上下文。

ML 的值限制将在（以前被认为是罕见但可能更普遍的）情况下不允许参数多态性，否则这样做是合理的（即类型安全），例如特别是对于 curried 函数的部分应用（这在函数式编程中很重要)，因为替代类型解决方案在函数式编程和命令式编程之间创建了分层，并打破了模块化抽象类型的封装。Haskell 有一个类似的双重单态限制。OCaml 在某些情况下放宽了限制。我详细阐述了其中一些细节。

编辑：我在上面引用中表达的原始直觉（子类型可以消除值限制）是不正确的。IMO 的答案很好地阐明了问题，我无法确定包含 Alexey、Andreas 或我的集合中的哪个应该是选定的最佳答案。IMO 他们都是值得的。

在显式类型注释的情况下，Haskell 检查推断类型是否至少与其签名一样多态，或者换句话说，推断类型是否是显式类型的子类型。因此，以下函数是错误类型的：

然而，在我的场景中，我只有一个函数签名并且需要验证它是否被一个潜在的实现“占据”——希望这个解释是有道理的！

由于参数化属性，我假设两者foo都bar没有实现，因此，两者都应该被拒绝。但我不知道如何以编程方式得出结论。

目标是整理出所有或至少一部分无效类型签名，如上面的那些。我很感激每一个提示。

对于如下循环：

根据 try.ocamlpro.com 的签名是：

为什么会这样？loop() 永远不会停止调用自己，所以它不应该返回任何东西吗？

我正在制作一种强类型玩具函数式编程语言。它使用 Hindley Milner 算法作为类型推断算法。

实现该算法，我有一个关于如何推断相互递归函数的类型的问题。

f并且g是相互递归的函数。现在，当类型检查器推断 function 的类型时f，它也应该能够推断 function 的类型g，因为它是一个子表达式。

但是，在那一刻，功能g还没有定义。因此，类型检查器显然甚至不知道 function 的存在以及 functiong的类型g。

现实世界的编译器/解释器使用哪些解决方案？

我正在开发一种函数式编程语言的解释器，它使用 Hindley-Milner 类型系统。

问题是，类型错误应该在哪里发生（被检测到）？

例如，如果我将Integertype value 应用于具有 type 的函数Bool -> Integer，这显然是一个类型错误。类型推断器总是能检测到这一点吗？

我的猜测是，类型推断器并不总是完全知道表达式的类型，即在推断过程中。因此类型推断器检测到的一些错误是错误的，或者一些错误不会被检测到。

但是，表达式求值器应该正确检测类型错误，因为求值器完全知道表达式的类型。

如果类型推断器无法正确检测类型错误，那么静态类型解释语言（如 OCaml）如何处理静态类型错误检查？

根据Haskell 2010 语言报告，它的类型检查器是基于Hindley-Milner 的。所以考虑f这种类型的函数，

例如，它可能是长度函数。根据 Hindley-Milner 的说法，f []类型检查到Int. 我们可以通过实例化fto的类型[Int] -> Int和to 的类型[]来证明这一点[Int]，然后得出应用程序([Int] -> Int) [Int]是类型的结论Int。

在这个证明中，我选择实例化类型forall a. [a] -> Int并forall a. [a]替换Int为a. 我可以Bool代替，证明也有效。在 Hindley-Milner 中我们可以将多态类型应用于另一个，而不指定我们使用哪些实例，这不是很奇怪吗？

更具体地说，Haskell 中的什么阻止我a在实现中使用类型f？我可以想象这f是一个18在 any 上[Bool]等于的函数，并且在所有其他类型的列表上等于通常的长度函数。在这种情况下，将f []是18或0？Haskell 报告说“内核没有正式指定”，所以很难说。

我正在尝试在 Haskell 中执行函数组合，但我不确定哪个运算符是正确的。

文档包含这两种类型签名：

显然，这两个选项之间的区别在于 的存在/不存在Category cat，但是这个注释意味着什么，我应该如何使用这些信息来选择一个运算符而不是另一个运算符？

在比较其他两个运算符时，我还注意到上述两个签名的第三个变体：

forall注释是什么意思——>>用于第三种情况？

我最近一直在学习 λ-演算。我了解无类型和有类型 λ 演算之间的区别。但是，我不太清楚Hindley-Milner 类型系统和类型化 λ-calculus之间的区别。是关于参数多态性还是有其他差异？

谁能清楚地指出两者之间的差异（和相似之处）？

此代码编译：

如果将注释行添加回来，将导致错误：

为什么添加此方法调用会导致类型推断失败？

我看过这两个问题：

• Rust 的类型推断如何跨多个语句工作？
• Rust 如何从 From::<>::from() 推断结果类型？

从他们那里，我知道 Rust 使用了 Hindley-Milner 的（修改后的）版本。后一个问题的答案将 Rust 的类型推断描述为方程组。另一个答案明确指出“Rust 中的类型信息可以向后流动”。

使用应用于这种情况的这些知识，我们有：

1. example是类型?E
2. ?E必须有一个名为的方法some_method
3. ?E被退回
4. 返回类型是Example

向后工作，人类很容易看到?E必须是Example. 我能看到的和编译器能看到的差距在哪里？

我想将 W 算法扩展到 F# 中的元组和列表的推断，先验，只有两个规则要添加，我做了，但是结果部分不好。

事实上，如果我测试这样的代码：

另一方面，它可以工作，如下面的示例中详述的那样，这样的代码将无法工作：

并将pair被推断为(a, a)而不是(TInt, TInt).

列表也一样。

我用这篇论文来编写我的类型检查器。

我真的不明白什么是干扰。以下是用于这些示例的最小功能程序：

推理.fs

主文件

这是输出：

所以我们可以看到推理在第一个测试中正确工作，但在第二个测试中不正确（如上所示）。

我想解决和理解这个错误，我提前感谢你的帮助。