F-ing modules. Issue 5 (September 2014)

• Record Type: Journal Article
• Authors: ROSSBERG, ANDREAS; RUSSO, CLAUDIO; DREYER, DEREK
• Is Part Of: Journal of functional programming. Volume 24:Issue 5(2014)
• Page Start: 529
• Page End: 607
• Publication Date: 2014-09
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796814000264
• Languages: English
• ISSNs: 0956-7968

Abstract

<abstract abstract-type="normal"> <title>Abstract</title> <p>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 present a novel formalization of ML modules, which defines their semantics directly by a compositional "elaboration" translation into plain System F<sub>ω</sub> (the higher-order polymorphic λ-calculus). To demonstrate the scalability of our "F-ing" semantics, we use it to define a representative, higher-order ML-style module language, encompassing all the major features of existing ML module dialects (except for recursive modules). We thereby show that ML modules are merely a particular mode of use of System F<sub>ω</sub>.</p> <p>To streamline the exposition, we present the semantics of our module language in stages. We begin by defining a subset of the language supporting a Standard ML-like language with <italic>second-class</italic> modules and <italic>generative</italic> functors. We then extend this sublanguage with the ability to package modules as <italic>first-class</italic> values (a very simple extension, as it turns out) and OCaml-style <italic>applicative</italic> functors (somewhat harder). Unlike previous work combining both generative and applicative functors, we do not require two distinct forms of functor or signature sealing. 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 <italic>pure</italic> versus <italic>impure</italic> functors. This approach results in a semantics that we feel is simpler and more natural than previous accounts, and moreover prohibits breaches of abstraction safety that were possible under them.</p> </abstract>