问题描述
AFAIK，在 Hindley-Milner 类型系统中使用的统一可以通过在构造函数位置允许类型变量并在这种情况下放宽元数约束来推广以统一更高级的类型：
f a ~ T a1 b1
f ~ T a1 -- generatifity + partial application
a ~ b1 -- injectivity
我猜也涉及到种类，但我不知道如何。
以我的一点经验，我认为这足以将高级类型的声音统一起来。与高阶统一的主要区别可能是
- 广义 HM 是可判定的，HOU 不是一般的
- 广义 HM 受到更多限制，即拒绝 HOU 中合法的类型
虽然我以某种方式回答了我的问题，高阶统一给了我们什么，但我不知道应用高阶统一时涉及哪些（简化的）规则。该算法与广义 HM 有何不同？
解决方法
这不是我真正的驾驶室，但我也许可以提供一个非常笼统的答案。
根本区别在于广义 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 类型检查器可能是程序员可能难以控制的一种能力。可能有点难以推断类型检查器可以推断出 f x = Either x String 或 f x = Either String x。