F-ing modules. Issue 5 (September 2014)
- Record Type:
- Journal Article
- Title:
- F-ing modules. Issue 5 (September 2014)
- Main Title:
- F-ing modules
- Authors:
- ROSSBERG, ANDREAS
RUSSO, CLAUDIO
DREYER, DEREK - 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><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> … (more)
- Is Part Of:
- Journal of functional programming. Volume 24:Issue 5(2014)
- Journal:
- Journal of functional programming
- Issue:
- Volume 24:Issue 5(2014)
- Issue Display:
- Volume 24, Issue 5 (2014)
- Year:
- 2014
- Volume:
- 24
- Issue:
- 5
- Issue Sort Value:
- 2014-0024-0005-0000
- Page Start:
- 529
- Page End:
- 607
- Publication Date:
- 2014-09
- Subjects:
- Functional programming (Computer science) -- Periodicals
- Journal URLs:
- http://journals.cambridge.org/action/displayJournal?jid=JFP ↗
http://firstsearch.oclc.org ↗ - DOI:
- 10.1017/S0956796814000264 ↗
- Languages:
- English
- ISSNs:
- 0956-7968
- Deposit Type:
- Legaldeposit
- View Content:
- Available online (eLD content is only available in our Reading Rooms) ↗
- Physical Locations:
- British Library STI - ELD Digital store
- Ingest File:
- 4105.xml