输入递归模块

Question

在Leroy关于如何在OCaml中输入递归模块的论文中,编写了在模块类型近似的环境中检查模块:

module rec A = ... and B = ... and C = ...

环境{A - >约(A); B - >约(B); 首先构建C - > approx(C)},然后用于计算A,B和C的类型.

我注意到,在某些情况下,近似值不够好,并且类型检查失败.特别是,当将编译单元源放在递归模块定义中时,类型检查可能会失败,而编译器则能够单独编译编译单元.

回到我的第一个例子,我发现一个解决方案是在初始近似环境中输入A,然后在新的计算类型A扩展的初始环境中输入B,并在前一个环境中输入C新计算的B类型,依此类推.

在进一步研究之前,我想知道是否有关于此主题的任何先前工作,表明这种递归模块的编译方案是安全还是不安全？是否有反例显示使用此方案正确键入的不安全程序？

Answer 1

首先,请注意Leroy(或Ocaml)不允许module rec没有明确的签名注释.所以它是相当的

module rec A : SA = ... and B : SB = ... and C : SC = ...

并且近似环境是{A:约(SA),B:约(SB),C:约(SC)}.

一些模块在单独定义时进行类型检查,而不是递归定义时,这并不奇怪.毕竟,对于核心语言声明也是如此:在'let rec'中,绑定变量的递归出现是单态的,而使用分离的'let'声明,您可以多态地使用先前的变量.直觉上,原因是在实际检查定义之前,你不可能拥有所需的所有知识来推断更自由的类型.

关于你的建议,它的问题是它使module rec构造不对称,即顺序可能以潜在的微妙方式.这违反了递归定义的精神(至少在ML中),它应该总是对排序无动于衷.

一般来说,递归输入的问题不是那么健全,而是完整性.您不希望类型系统一般是不可判定的,或者其规范依赖于算法假象(如检查顺序).

更一般地说,众所周知,Ocaml对递归模块的处理是相当严格的.有一些工作,例如Nakata和Garrigue,进一步推动了它的极限.但是,我确信,最终,你将无法像你想的那样获得自由(并且这也适用于其类型模块系统的其他方面,例如functor),而不会放弃Ocaml纯粹的语法模板语法方法.但后来,我有偏见.:)