4

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

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

我想还涉及种类，但我不知道如何。

以我的一点经验，我会说这对于高级类型的声音统一来说已经足够了。与高阶统一的主要区别可能是

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

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

4

1 回答 1

4

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

根本区别在于，广义 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 都会立即放弃，因为 typeB是 kind *，不能在句法上与涉及 的类型表达式统一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。

于 2021-02-01T19:57:21.413 回答