Claudio Russo

Derek Dreyer

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 give a *very simple* elaboration
semantics for a full-featured, higher-order ML-like module
language. Our elaboration defines the meaning of module expressions
by a straightforward, compositional translation into vanilla System F_{ω}
(the higher-order polymorphic λ-calculus), under
plain F_{ω} typing environments. We thereby show that ML modules are
merely a particular mode of use of System F_{ω}.

We start out with a module language that supports the usual
second-class modules with Standard ML-style *generative*
functors, and includes local module definitions. To demonstrate the
versatility of our approach, we further extend the language with the
ability to package modules as first-class values — a very simple
extension, as it turns out — and a novel treatment of OCaml-style
*applicative* functors. Unlike previous work combining both
generative and applicative functors, we do not require two distinct
forms of functor or sealing expressions. 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 what is best understood as *pure* vs.\
*impure* functors. This approach results in a semantics that we
feel is simpler and more natural, and moreover prohibits breaches of
data abstraction that are possible under earlier semantics for
applicative functors.

We also revive (in refined form) the long-lost notion of
*structure sharing* from SML'90. Although previous work
on module type systems has disparaged structure sharing as
type-theoretically questionable, we observe that (1) some variant of it is in fact
*necessary* in order to provide a proper treatment of abstraction
in the presence of applicative functors, and (2) it is straightforward
to account for using ``phantom types''.
Based on this, we can even justify the (previously poorly understood) "`where module`" operator for signatures and the related notion of manifest module specifications.

Altogether, we describe a comprehensive, unified, and yet simple semantics of a full-blown module language that — with the main exception of cross-module recursion — covers almost all interesting features that can be found in either the literature or in practical implementations of ML modules. We prove the language sound and its type checking decidable.

- F-ing Modules. Draft extended version of TLDI paper, covering applicative functors.

(We recommend printing in colour.) - F-ing Modules. TLDI 2010.

- F-ing Modules with Coq. Proof script for the Coq 8.1 theorem prover.
- F-ing Modules with Coq. Proof script for the Coq 8.2pl1 theorem prover.

*Note: If you do not have 8.2 at pl1 yet (e.g., because you are on Mac), you have to edit line 175 of Metatheory_Var.v and change "at level 67" to "at level 70". Sorry for that.*