问题标签 [hindley-milner]

有人曾经向我展示了 SML 中的一个小“技巧”​​，他们在他们的 REPL 中写出了大约 3 或 4 个函数，最后一个值的结果类型非常长（就像许多页面滚动一样长）。

有谁知道什么代码会生成这么长的类型，或者是否有这种行为的名称？

我正在研究方案编译器斯大林。它庞大而复杂。另外，如果我理解正确的话，作者正计划写一系列论文来详细说明实现的各个方面，但一直没有时间去做。

我感兴趣的斯大林方面是全局类型推断：根据事物在程序中其他地方的使用情况来推断事物的类型。斯大林真的这样做了吗？如果是，如何以及在其代码库中的位置？它是否使用 Hindley-Milner 算法的变体/扩展？

Haskell 类型系统 (*) 的有趣特性之一是，有时您可以仅根据其类型签名准确地判断函数的作用（假设没有涉及unsafe IO黑魔法）。

例如，任何具有类型签名a -> a的函数都必须是恒等函数，任何类型的函数(a,b) -> a都等价于fst. 在某些情况下，您无法完全确定函数：类型有无数种不同的可能函数a -> Int，但它们都是常量——它们都忽略了第一个参数。

我觉得这个属性很吸引人，但我怀疑它只适用于“微不足道”的函数，例如idand const。我对么？

此外，我在这里的推理仅基于直觉 - 例如，在 中a -> a，我们“一无所知” a（与像 等受约束的函数相反Num a => a -> a），因此除了原样返回之外，“不能做任何事情”。有没有正式的方法来处理这些扣除？

_{* 我知道 Haskell 的类型系统是基于Hindley-Milner 类型系统的，但我对它还不够熟悉，无法对此做出任何假设}

在“什么是欣德利·米尔纳”下，它指出：

Hindley-Milner 是System F的一个限制，它允许更多类型但需要程序员注释。

我的问题是，什么是 System F 中可用的类型的示例，但在 Hindley Milner 中不可用（类型推断）？

（假设系统 F 类型的推断已被证明是不可判定的）

考虑以下示例：

非递归函数

GHC 推断f :: a -> a

相互递归函数

现在 GHC 推断f :: Char -> Char，即使类型可能a -> a只是前一种情况。

多态递归

size除非给出明确的类型，否则GHC 无法推断 的类型。

因此，Haskell (GHC) 似乎没有使用多态递归（如Alan Mycroft：多态类型方案和递归定义中所述），因为它无法在示例 2 和 3 中推断多态类型。但在第一种情况下它是正确的推断f. 确切的程序是什么？GHC 是否分析表达式的依赖关系，将它们组合在一起（如第二个示例中的f和g）并在这些组上使用单态递归类型推断？

runST是一个 Haskell 函数，它通过类型静态地限制资源的可用生命周期。为此，它使用 rank-2 多态性。标准 ML 更简单的类型系统仅提供 rank-1 多态性。

标准 ML 是否仍然可以使用类型将资源的生命周期限制为类似的最终结果？

本页和本页演示了一些将代码重组为只需要更简单类型的方法。如果我理解正确，核心是将表达式包装起来，以便将其替换为上下文中可能的观察结果，这些观察结果是有限的。这种技术通用吗？是否可以将它或相关的编码与（显然与签名不同）之类runST的东西一起使用，以防止观察到从包装表达式中转义的值的类型？如果是这样，怎么做？

我想象的场景是这样的：

...wheremagic...提供了用户提供的代码无法以任何方式共享的资源。显然，像这样带有单个库函数的简单接口是不可能的，但也许有不同的包装层、手动内联和提取......？

我已经看到了这个，但是如果我理解正确（......很可能不是），那实际上并不能阻止对资源的所有引用被共享，只能确保对它的一个引用必须是“关闭的”。

基本上我想在 SML 中实现安全类型的显式（不是推断的 MLKit 样式）区域。

考虑以下程序（在 Haskell 中，但可以是任何 HM 推断语言）：

使用 HM（或通过运行编译器），我们推断：

我理解这是如何发生的，按照通常的泛化/实例化规则进行操作，但我不确定是否需要像forall a. a.

一个问题是：由于我们在这里有一个越界访问，因此可以排除该程序作为有效示例的可能性。相反，我们可以说我们推断的通用类型是程序中出现问题的标志吗？如果是，我们是否可以利用这个“事实”在其他情况下故意不检查无效程序？

下一个程序得到更奇怪的类型：

推断类型：

...虽然d是从c!

我们能否在不排除有效程序的情况下增加 HM 以在这里做得更好？

编辑：我怀疑这是使用部分函数的工件（!!0在这种情况下）。但请看：

现在没有使用偏函数。然而，c :: forall t. [t]和d :: Int。

我试图在 Haskell 中编写一个关系问题，但我不得不发现以类型安全的方式执行此操作远非显而易见。比如谦虚

已经提出了一些问题：

• 这个函数的类型是什么？
• 投影的类型是什么1,a,b？一般投影的类型是什么？
• 什么是结果类型，如何表达结果类型和投影之间的关系？
• 接受任何有效投影的这种函数的类型是什么？
• 如何在编译时检测无效预测？
• 如何将列添加到表格或投影中？

我相信即使是 Oracle 的 PL/SQL 语言也不能完全正确地做到这一点。虽然无效预测大多在编译时检测到，但大量类型错误仅在运行时显示。大多数其他与 RDBMS 的绑定（例如 Java 的 jdbc 和 perl 的 DBI）使用包含在字符串中的 SQL，因此完全放弃了类型安全。

进一步的研究表明，有一些 Haskell 库（HList、vinyl和 TRex）提供类型安全的可扩展记录等等。但是这些库都需要 Haskell 扩展，例如DataKinds、FlexibleContexts等等。此外，这些库并不容易使用并且有诡计的味道，至少对于像我这样的未初始化的观察者来说是这样。

这表明，类型安全的关系操作不适合函数范式，至少不像在 Haskell 中实现的那样。

我的问题如下：

• 以类型安全的方式对关系操作建模困难的根本原因是什么？Hindley-Milner 的不足之处在哪里？或者问题是否已经起源于类型化的 lambda 演算？
• 有没有一种范式，关系操作是一等公民？如果是这样，是否有现实世界的实施？

我无法理解维基百科上给出的 HM 系统的 letrec 定义，这里：https ://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

对我来说，该规则大致转换为以下算法：

1. 推断letrec定义部分 中所有内容的类型
   1. 将临时类型变量分配给每个定义的标识符
   2. 递归处理所有具有临时类型的定义
   3. 成对，将结果与原始临时变量统一起来
2. 关闭（用forall）推断的类型，将它们添加到基础（上下文）并用它推断表达式部分的类型

我在使用这样的程序时遇到问题：

我观察到的行为如下：

• p获取临时类型的定义a
• 的定义也x有一些临时类型，但这已经超出了我们的范围
• in x, 的定义test得到一个临时类型t
• p从作用域中获取临时类型a，对变量使用 HM 规则
• (f 5)由应用程序的 HM 规则处理，结果类型是b（以及（a统一与）的统一Uint -> b）
• ((p 5) 5)由相同的规则处理，产生更多的统一和类型c，a现在结果统一为Uint -> Uint -> c
• 现在，测试关闭输入forall c.c
• 变量测试in test获取类型实例（或forall c.c）带有新鲜变量，根据变量的HM规则，导致test :: d（即与test::t右上统一）
• 结果x具有有效的类型d（或t，取决于统一的心情）

问题：x显然应该有 type Uint，但我认为这两者不可能统一产生类型。当类型test被关闭并再次实例化时会丢失信息，我不确定如何克服或连接替换/统一。

知道如何更正算法以x::Uint正确生成打字吗？或者这是 HM 系统的一个属性，它根本不会输入这种情况（我怀疑）？

请注意，这对于 standard 来说是完全可以的let，但我不想用无法处理的递归定义来混淆示例let。

提前致谢

我有两个用于控制循环的功能，continue并且break：

然后，我想简化Control类型同义词。因此，我写道：

然而，当我试图进一步简化它时，我得到了一个错误：

我不明白为什么我会收到这个错误。也许你可以启发我。