使用模块无限循环OCaml类型检查器如何工作？

html5 • • 问答

此示例中的 OCaml 类型检查器无限循环：

     module type I =
     sig
       module type A
       module F :
         functor(X :
         sig
           module type A = A
           module F : functor(X : A) -> sig end
         end) -> sig end
     end

     module type J =
     sig
       module type A = I
       module F : functor(X : I) -> sig end
     end

     (* Try to check J <= I *)

     module Loop(X : J) = (X : I)

资料来源：Andreas Rossberg 改编 Mark Lillibridge 的例子

我不太清楚这是如何/为什么工作的。特别是：

  • 这个例子是最小的吗？
  • 所有共享约束都在A = I, A = A, etc.做什么工作？是否需要共享约束才能导致这种无限循环？
  • 第一个函子中的内联签名做了什么工作？这对于这个例子来说似乎是必不可少的。
  • 这个技巧只对无限循环有用，还是可以在模块系统中进行任意计算？
  • 这样的例子可以翻译成其他语言吗？具有类型成员和参数化类型别名的特征和类看起来很像上面的代码。

回答

  • 这个例子非常小，它依赖于两个基本要素：
    • 抽象模块类型
    • 使抽象模块类型同时出现在协变和逆变位置的函子。

在返回示例之前回答您的高级问题：

  • 使用这个技巧，只有模块类型系统的子类型检查器正在做无限量的工作。您无法观察此计算的结果。然而，使用抽象模块类型是欺骗模块类型系统进行扩展计算的关键（例如一个具有 4??4 个子模块链的模块）

  • 重现这个确切的问题可能需要子类型化和不可预测性，我不确定这种组合在模块系统之外出现的频率。

回到手头的示例，我建议使用 OCaml 4.13 及其with module type约束向未来迈进一点。我希望这能让这个技巧背后的成分更加明显：

module type e = sig end

module type Ieq = sig
  module type X
  module type A = X
  module F : X -> e
end

module type I = sig
  module type A
  module F : Ieq with module type X = A -> e
end

module type J = Ieq with module type X = I

意见可能会有所不同，但我发现这种形式更明显的是，在这种I情况下，我们有更多关于函子F组件的方程，而在这种Ieq with module type X = ...情况下，我们有更多关于模块类型A组件的方程。

在试图证明J< 时I，我们最终在这些等式之间移动而没有取得任何进展。让我们试着看看这是如何一步一步地发生的。首先，我们看一下模块类型A：

J 一世
JA = module type A = I IA = module type A（抽象）

因为I.A是抽象的，所以这是真的。然后，我们需要比较J.F和I.F，但只有在添加A=I来自的等式之后J。

J I 模块类型 A = I
JF = I -> e 如果 = (Ieq with module type X = (*A =*) I) -> e

现在，我们有了一个函子。函子的论证是逆变的。换句话说，要证明X -> e< Y -> e，我们需要证明Y < X。

因此，我们需要证明Ieq with module type X = I< I... 但是这个不等式看起来有点熟悉。事实上，我们已经定义了：

module type J = Ieq with module type X = I

重用这个定义，这意味着我们又回到了尝试证明J< 的过程中I，但没有取得任何进展。

如果我们查看之前的步骤，问题就开始于我们扩展I自身的另一个副本时I with module type A = I。然后逆变允许我们将这种规模的增加分散到比较的双方。因此，我们的包含检查总是为它未来的自己产生更多的工作，而且这个特定的包含检查永远不会结束。

以上是使用模块无限循环OCaml类型检查器如何工作？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>