haskell - 广义 HM 与高阶统一

Question

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

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

我想种类也涉及到，但我不知道如何。
以我的一点经验，我会说这足以使高级类型的声音统一。高阶统一的主要区别可能是

广义 HM 是可判定的，HOU 不是一般的

广义 HM 受到更多限制，即拒绝 HOU 中合法的类型

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

Answer 1

这不是我真正的驾驶室，但我也许可以提供一个非常笼统的答案。
根本区别在于广义 HM 将统一视为旨在产生唯一匹配的纯句法匹配过程，而 HOU 算法涉及类型/种类的语义考虑(如类型化 lambda 演算中的术语/类型)和系统搜索通过可能统一的树，包括考虑内部节点的替代统一。
(HM 方法的局限性在于，对于一​​阶类型，纯句法匹配基本上相当于对类型的语义考虑和通过可能的统一进行系统搜索。)
无论如何，采取一个微不足道的高阶统一:

Either String Int ~ f String

由于 Either 的 absurd 原因，您提出的广义 HM 算法在这种统一上失败了。的参数顺序错误，纯粹是句法细节，与类型的语义统一性无关。您可以进一步概括您的算法以在句法上处理这种特殊情况，但总会有一些其他微不足道的统一与句法模式不匹配。您最终还会在统一时遇到奇怪的“不连续性”:

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 算法通过构建“匹配树”来实现。树中的每个节点都标有“分歧集”(基本上，一组 Unresolved 统一)，分支标有替代替换。终端节点表示统一的“成功”或“失败”。
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 .