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...

• Type: Conference
• Year: 2010
• Where: TLDI
• Authors: Andreas Rossberg, Claudio V. Russo, Derek Dreyer
• Keywords: Applicative Functor Semantics, Formal Methods, ML Modules, Simple Elaboration Semantics, TLDI 2010