ocaml - 使用模块无限循环 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

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

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

Answer 1

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

在回到示例之前回答您的高级问题:

• 有了这个技巧，只有模块类型系统的子类型检查器才能完成无限量的工作。您无法观察到此计算的结果。然而，使用抽象模块类型是欺骗模块类型系统进行扩展计算的关键(例如，具有 4↑↑4 子模块链的模块)

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

回到手头的例子，我建议使用 OCaml 4.13 及其 with module type 来飞跃 future 。约束。我希望这能让这个技巧背后的成分更加明显:

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 :

<表类="s-表"><头>J我<正文>J.A = module type A = I I.A = module type A (摘要)

自 I.A是抽象的，这是真的。然后，我们需要比较J.F和 I.F , 但仅在添加方程式 A=I 之后来自 J .

<表类="s-表"><头>JI 模块类型 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 时开始的与自身的另一个副本 I with module type A = I .然后逆变允许我们将这种大小的增加扩展到比较的两侧。因此，我们的包含检查总是为其 future 的自己产生更多的工作，并且这种特定的包含检查永远不会结束。