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

Question

本例中的 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

我不太了解how/why这个作品。特别是：

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

Answer 1

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

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

有了这个技巧，只有模块类型系统的子类型检查器正在做无限量的工作。您无法观察到此计算的结果。然而，使用抽象模块类型是欺骗模块类型系统进行扩展计算的关键（例如，具有 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	I
J.A = `module type A = I`	I.A = `module type A` (abstract)

因为I.A是抽象的，所以这是真的。然后，我们需要比较 J.F 和 I.F，但仅在从 J.

添加等式 A=I 之后

J	I with module type 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

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

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

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

How does infinite-looping the OCaml type checker using modules work?

ocaml