输入递归模块
在 Leroy 的论文中，关于如何在 OCaml 中输入递归模块，它写道，在由模块类型的近似组成的环境中检查模块：
module rec A = ... and B = ... and C = ...
环境{A -> >大约（A）； B->大约（B）； C-> approx(C) } 首先构建，然后用于计算 A、B 和 C 的类型。
我注意到，在某些情况下，近似值不够好，并且类型检查失败。特别是，当将编译单元源放入递归模块定义中时，类型检查可能会失败，而编译器能够单独编译编译单元。
回到我的第一个示例，我发现解决方案是在初始近似环境中键入 A，然后在使用 A 的新计算类型扩展的初始环境中键入 B，并在之前的环境中键入 C B 的新计算类型，等等。
在进行更多调查之前，我想知道是否有关于此主题的任何先前工作，表明这种递归模块的编译方案是安全的还是不安全的？是否有一个反例显示使用此方案正确键入的不安全程序？
In Leroy's paper on how recursive modules are typed in OCaml, it is written that modules are checked in an environment made of approximations of module types:
module rec A = ... and B = ... and C = ...
An environment {A -> approx(A); B -> approx(B); C -> approx(C) } is first built, and then used to compute the types of A, B and C.
I noticed that, in some cases, approximations are not good enough, and typechecking fails. In particular, when putting compilation units sources in a recursive module definition, typechecking can fail whereas the compiler was able to compile the compilation units separately.
Coming back to my first example, I found that a solution would be to type A in the initial approximated environment, but then to type B in that initial environment extended with the new computed type of A, and to type C in the previous env with the new computed type of B, and so on.
Before investigating more, I would like to know if there is any prior work on this subject, showing that such a compilation scheme for recursive modules is either safe or unsafe ? Is there a counter-example showing an unsafe program correctly typed with this scheme ?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
首先，请注意，Leroy（或 Ocaml）不允许没有显式签名注释的
模块记录。因此，近似环境是 {A : approx(SA), B : approx(SB), C : approx(SC)}。
毫不奇怪，某些模块在单独定义时进行类型检查，但在递归定义时则不进行类型检查。毕竟，对于核心语言声明来说也是如此：在“let rec”中，绑定变量的递归出现是单态的，而使用单独的“let”声明，您可以多态地使用先前的变量。直观上，原因是在实际检查定义之前，您无法拥有推断更自由类型所需的所有知识。
关于您的建议，它的问题在于它使
module rec构造不对称，即顺序可能会以潜在微妙的方式产生影响。这违反了递归定义的精神（至少在机器学习中），递归定义应该始终对排序漠不关心。一般来说，递归类型的问题不在于健全性，而在于完整性。您不希望类型系统总体上是不可判定的，或者其规范依赖于算法制品（例如检查顺序）。
更一般地说，众所周知，Ocaml 对递归模块的处理相当严格。已经有一些工作，例如 Nakata & 的作品。加里格，这进一步突破了它的极限。然而，我相信最终，如果不放弃 Ocaml 纯粹的模块类型语法方法，您将无法获得您想要的自由（这也适用于其类型模块系统的其他方面，例如函子） 。但是，我有偏见。 :)
First, note that Leroy (or Ocaml) does not allow
module recwithout explicit signature annotations. So it's ratherand the approximative environment is {A : approx(SA), B : approx(SB), C : approx(SC)}.
It is not surprising that some modules type-check when defined separately, but not when defined recursively. After all, the same is already true for core-language declarations: in a 'let rec', recursive occurrences of the bound variables are monomorphic, while with separated 'let' declarations, you can use previous variables polymorphically. Intuitively, the reason is that you cannot have all the knowledge that you'd need to infer the more liberal types before you have actually checked the definitions.
Regarding your suggestion, the problem with it is that it makes the
module recconstruct unsymmetric, i.e. order would matter in potentially subtle ways. That violates the spirit of recursive definitions (at least in ML), which should always be indifferent to ordering.In general, the issue with recursive typing is not so much soundness, but rather completeness. You don't want a type system that is either undecidable in general, or whose specification is dependent on algorithmic artefacts (like checking order).
On a more general note, it is well-known that Ocaml's treatment of recursive modules is rather restrictive. There has been work, e.g. by Nakata & Garrigue, that pushes its limits further. However, I am convinced that ultimately, you won't be able to get as liberal as you'd like (and that applies to other aspects of its type module system as well, e.g. functors) without abandoning Ocaml's purely syntactic approach to module typing. But then, I'm biased. :)