一句话：提出 Mω 类型系统，覆盖 OCaml 模块中的 applicative/generative functor 与透明归属，并经 Fω 精化证明其可靠性。
ML 模块提供组合与抽象，但高级用法复杂，OCaml 模块层缺乏形式规范且实现有意外行为。本文在 ML 模块到 Fω 翻译基础上提出类型系统 Mω，覆盖 OCaml 模块较大子集，含 applicative/generative functor 与透明归属。Mω 生成带 Fω 量词的类 OCaml 签名，并给出到基于路径源签名的逆向翻译及签名规避刻画，适合作类型检查器内部表示。作者经 Fω 精化证明可靠性，引入透明存在类型（可从全称与箭头类型提升的弱存在类型），改进 applicative functor 中 sealing 编码，使 applicative 抽象处理更接近 generative functor。
ML modules come as an additional layer on top of a core language to offer large-scale notions of composition and abstraction. They largely contributed to the success of OCaml and SML. While modules are easy to write for common cases, their advanced use may become tricky. Additionally, despite a long line of works, their meta-theory remains difficult to comprehend, with involved soundness proofs. In fact, the module layer of OCaml does not currently have a formal specification and its implementation has some surprising behaviors. Building on previous translations from ML modules to Fω, we propose a type system, called Mω, that covers a large subset of OCaml modules, including both applicative and generative functors, and extended with transparent ascription. This system produces signatures in an OCaml-like syntax extended with Fω quantifiers. We provide a reverse translation from Mω signatures to path-based source signatures along with a characterization of signature avoidance cases, making Mω signatures well suited to serve as a new internal representation for a typechecker. The soundness of the type system is shown by elaboration in Fω. We improve over previous encodings of sealing within applicative functors, by the introduction of transparent existential types, a weaker form of existential types that can be lifted out of universal and arrow types. This shines a new light on the form of abstraction provided by applicative functors and brings their treatment much closer to those of generative functors.
@article{paperbot2535,
title = {Fulfilling OCaml Modules with Transparency},
author = {Blaudeau Clement and Didier Rémy and Gabriel Radanne},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649818}
}