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

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

此示例中的 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)

source: Andreas Rossberg adapting Mark Lillibridge's example

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

• 这个例子是最小的吗？
• 所有共享约束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 组件上还有一个等式。

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

J	我
J.A = module type A = I	I.A = module type A（抽象）

由于 I.A 是抽象的，所以这是真的。然后，我们需要比较 J.F 和 I.F，但前提是将 A=I 中的方程 J 相加。

J	I 模块类型 A = I
J.F = I -> e	I.F = (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

重复使用这个定义，这意味着我们又要重新尝试证明 JI，但没有取得任何进展。

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