ML modules are a powerful language mechanism for decomposing programs
into reusable components.  Unfortunately, they also have a reputation
for being "complex" and requiring fancy type theory that is mostly
opaque to non-experts.  While this reputation is certainly
understandable, given the many non-standard methodologies that have
been developed in the process of studying modules, we aim here to
demonstrate that it is undeserved.  To do so, we present a novel
formalization of ML modules, which defines their semantics directly by
a compositional "elaboration" translation into plain System F-omega
(the higher-order polymorphic lambda-calculus).  To demonstrate the
scalability of our "F-ing" semantics, we use it to define a
representative, higher-order ML-style module language, encompassing
all the major features of existing ML module dialects (except for
recursive modules).  We thereby show that ML modules are merely a
particular mode of use of System F-omega.

To streamline the exposition, we present the semantics of our module
language in stages.  We begin by defining a subset of the language
supporting a Standard ML-like language with *second-class* modules and
*generative* functors.  We then extend this sublanguage with the
ability to package modules as *first-class* values (a very simple
extension, as it turns out) and OCaml-style *applicative* functors
(somewhat harder).  Unlike previous work combining both generative and
applicative functors, we do not require two distinct forms of functor
or signature sealing.  Instead, whether a functor is applicative or
not depends only on the computational purity of its body.  In fact, we
argue that applicative/generative is rather incidental terminology for
*pure* vs. *impure* functors.  This approach results in a semantics
that we feel is simpler and more natural than previous accounts, and
moreover prohibits breaches of abstraction safety that were possible
under them.