F-ing modules

9 years 10 months ago
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, 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ω. Our module language supports the usual second-class modules with Standard ML-style generative functors and local module definitions. To demonstrate the ve...
Andreas Rossberg, Claudio V. Russo, Derek Dreyer
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where TLDI
Authors Andreas Rossberg, Claudio V. Russo, Derek Dreyer
Comments (0)