广义 HM 与高阶统一

Posted 2023-05-08

【中文标题】广义 HM 与高阶统一

【英文标题】：Generalized HM vs. Higher-Order Unification

【发布时间】：2021-05-05 16:21:42

【问题描述】：

AFAIK，Hindley-Milner 类型系统中使用的统一可以通过在构造函数位置允许类型 var 并在这种情况下放宽 arity 约束来推广以统一更高种类的类型：

f a ~ T a1 b1
f ~ T a1 -- generatifity + partial application
a ~ b1   -- injectivity

我猜也涉及到种类，但我不知道如何。

根据我的一点经验，我认为这足以实现高种类型的健全统一。与高阶统一的主要区别可能是

广义的HM是可判定的，HOU不是一般的 广义 HM 受到更多限制，即拒绝在 HOU 中合法的类型

虽然我以某种方式回答了我的问题，高阶统一给了我们什么，但我不知道应用高阶统一时涉及哪些（简化的）规则。该算法与广义 HM 有何不同？

【问题讨论】：

我认为，如果您在 app(f, a) ~ app(app(T, a1), b1) 中使用显式应用程序编写类型，它遵循编译器/类型检查器中的实际 AST，那么您可以使用标准统一。

好吧，如果你同意 HOU 是不可判定的，那么问题是“[HOU] 算法与广义 HM 有何不同？”没有多大意义，因为不可能有 HOU 算法。这是这里唯一带问号的句子，这使得这篇文章很难做出明智的回应。

@DanielWagner 公平点。我的印象是 HOU 只是在某些情况下是不可判定的，你可以相应地限制类型系统，有点像 System Fω？很抱歉这么手残。我缺乏必要的逻辑/类型论知识。

那么...你的问题是什么？

还值得注意的是，虽然注入性和生成性是必要的，但保持一阶事物的很大一部分只是不允许部分应用类型同义词，因为它们等同于类型级 lambdas。这与不可预测性密切相关：你不能将forall 类型作为构造函数的参数（除了(->) 和RankNTypes），除非你将它包装在newtype 中——通常解释为“隐藏”不可预测性，但也可以认为是告诉编译器在哪里泛化和实例化 forall ≈ 抽象并应用类型级 lambda。

【参考方案1】：

这不是我真正的驾驶室，但我也许可以提供一个非常笼统的答案。

根本区别在于，广义 HM 将统一视为旨在产生唯一匹配的纯句法匹配过程，而 HOU 算法涉及类型/种类的语义考虑（作为类型化 lambda 演算中的术语/类型）和通过可能的统一树进行系统搜索，包括考虑内部节点的替代统一。

（HM方法存在局限性的原因在于，对于一​​阶类型，纯句法匹配基本上等价于对类型的语义考虑和通过可能的统一进行系统搜索。）

不管怎样，取一个微不足道的高阶统一：

Either String Int ~ f String

您提出的广义 HM 算法在这种统一上失败了，原因很荒谬，Either 的参数顺序错误，纯粹的语法细节与类型的语义统一性无关。您可以进一步概括您的算法以在句法上处理这种特殊情况，但总会有一些其他琐碎的统一与句法模式不匹配。你也会在统一时遇到一个奇怪的“不连续性”：

Either String String ~ f String

您可以让您的算法对具有统一性的程序进行类型检查：

Either Int String ~ f Int
Either String String ~ f String
 ==> f x = Either x String

或：

Either String Int ~ f Int
Either String String ~ f String
 ==> f x = Either String x

但可能不是两者兼而有之。

相比之下，任何自尊的 HOU 算法都可以轻松地对这些程序进行类型检查。

基于 Huet 算法的 HOU 算法通过构建“匹配树”来实现。树中的每个节点都标有“分歧集”（基本上是一组未解决的统一），分支标有替代替换。终端节点表示统一的“成功”或“失败”。

Huet 论文中提出的示例 3.2 是统一：

f x A ~ B

任何广义的 HM 都会立即放弃，因为 B 类型属于 *，无法在语法上与涉及 f :: * -> * -> * 的类型表达式统一。

对于类似 Huet 的算法，匹配树的构造是在根节点上使用此单例不一致集，并在其分支上对 f 进行三种可能的正确替换：

f :: * -> * -> *
f u v = u
f u v = v
f u v = B

给树：

                        f x A ~ B
                             |
        --------------------------------------------
        | (f u v = u)        | (f u v = v)         | (f u v = B)
        |                    |                     |
      x ~ B              Failure                 Success
        |
        | (x = B)
        |
      Success

如果您仔细考虑一下，您会发现通用 HM 类型检查器与 HOU 检查器的强大功能甚至无法相提并论。您还将看到 HOU 类型检查器在实践中可能是程序员可能难以控制的一种能力。可能有点难以推理一个类型检查器可以推断出 either f x = Either x String 或 f x = Either String x。

【讨论】：

在第一次浏览您的答案后，我已经可以说它包含适量的信息，并且需要适量的先验知识才能让我理解。谢谢！

我在这里注意到 Huet 的算法不是语言实现中常用的算法，而是 Miller 的模式统一。模式统一不检查边的类型（在其最基本的版本中），仅假设边具有相同的类型，也不寻找可能的解决方案。此外，由于Either String Int ~ f String 没有唯一的解决方案，模式统一必然会失败。

更难的是，f 还有更多解决方案，比如f u v = if v == A then B else u；在任何“足够丰富”类型的语言中确实是无限多的。