Andreas Rossberg, F-ing Modules

F-ing Modules

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, I aim to
demonstrate that it is undeserved.  To do so, I give a very simple
elaboration semantics for a full-featured, higher-order ML-like module
language.  The elaboration defines the meaning of module expressions
by a straightforward, compositional translation into vanilla System F
(the polymorphic lambda-calculus), under plain F typing environments.
We thereby show that ML modules are merely a particular mode of use
of System F.

If time allows, I will also briefly discuss the problem of recursive modules,
why System F provides no adequate model for them, and why previous
accounts fail to support separate compilation properly. Our recent work
on combining ML modules with mixin composition addresses this problem.