Andreas Rossberg, 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.