ML modules come as an additional layer on top of the core language that offers large-scale notions of composition and modularity. They have been essential for developing complex applications and largely contributed to the success of OCaml and SML. While modules are easy to write for common cases, their intensive or advance use may become tricky. Additionally, despite a long line of work, 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.

We propose a new comprehensive description of a large subset of OCaml modules, with both applicative and generative functors, and extended with transparent ascription. Building on a previous translation from ML modules to Fω, we introduce an intermediate system, called Mω, that mediates between the source language and Fω, combining the convenient path-based syntactic notation of ML modules with the precise and well-established type-theory of Fω. From the Mω system, we elaborate terms into Fω using the new technique of transparent existential types, which ensures type soundness.