Loading...
Please wait, while we are loading the content...
Similar Documents
F-ing modules
| Content Provider | Scilit |
|---|---|
| Author | Rossberg, Andreas Russo, Claudio Dreyer, Derek |
| Copyright Year | 2014 |
| Abstract | 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_{ω}$ (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_{ω}$.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 second-class modules and generative functors. We then extend this sublanguage with the ability to package modules as first-class values (a very simple extension, as it turns out) and OCaml-style applicative 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 pure versus impure 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. |
| Related Links | https://www.cambridge.org/core/services/aop-cambridge-core/content/view/B573FA00832D55D4878863DE1725D90B/S0956796814000264a.pdf/div-class-title-f-ing-modules-div.pdf |
| Ending Page | 607 |
| Page Count | 79 |
| Starting Page | 529 |
| ISSN | 09567968 |
| e-ISSN | 14697653 |
| DOI | 10.1017/s0956796814000264 |
| Journal | Journal of Functional Programming |
| Issue Number | 5 |
| Volume Number | 24 |
| Language | English |
| Publisher | Cambridge University Press (CUP) |
| Publisher Date | 2014-09-01 |
| Access Restriction | Open |
| Subject Keyword | Journal of Functional Programming History and Philosophy of Science Ml Modules Applicative Functors |
| Content Type | Text |
| Resource Type | Article |
| Subject | Software |
