{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T21:50:05Z","timestamp":1723758605798},"reference-count":59,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2014,11,19]],"date-time":"2014-11-19T00:00:00Z","timestamp":1416355200000},"content-version":"unspecified","delay-in-days":79,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2014,9]]},"abstract":"Abstract<\/jats:title>ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being \u201ccomplex\u201d 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 \u201celaboration\u201d translation into plain System F\u03c9<\/jats:sub>(the higher-order polymorphic \u03bb-calculus). To demonstrate the scalability of our \u201cF-ing\u201d 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\u03c9<\/jats:sub>.<\/jats: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 withsecond-class<\/jats:italic>modules andgenerative<\/jats:italic>functors. We then extend this sublanguage with the ability to package modules asfirst-class<\/jats:italic>values (a very simple extension, as it turns out) and OCaml-styleapplicative<\/jats: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 forpure<\/jats:italic>versusimpure<\/jats: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.<\/jats:p>","DOI":"10.1017\/s0956796814000264","type":"journal-article","created":{"date-parts":[[2014,11,19]],"date-time":"2014-11-19T06:44:33Z","timestamp":1416379473000},"page":"529-607","source":"Crossref","is-referenced-by-count":31,"title":["F-ing modules"],"prefix":"10.1017","volume":"24","author":[{"given":"ANDREAS","family":"ROSSBERG","sequence":"first","affiliation":[]},{"given":"CLAUDIO","family":"RUSSO","sequence":"additional","affiliation":[]},{"given":"DEREK","family":"DREYER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,11,19]]},"reference":[{"key":"S0956796814000264_ref58","unstructured":"Torgersen M. , Ernst E. & Hanser C. P. (2005) Wild FJ. In International Workshop on Foundations of Object-Oriented Languages, 1\u201315."},{"key":"S0956796814000264_ref57","doi-asserted-by":"crossref","unstructured":"Sulzmann M. , Chakravarty M. M. T. , Peyton Jones S. & Donnelly K. (2007) System F with type equality coercions. In ACM SIGPLAN Workshop on Types in Language Design and Implementation, 53\u201366.","DOI":"10.1145\/1190315.1190324"},{"key":"S0956796814000264_ref55","unstructured":"SML\/NJ Development Team (1993) Standard ML of New Jersey user's guide. 0.93 ed., AT&T Bell Laboratories."},{"key":"S0956796814000264_ref54","unstructured":"Shields M. & Peyton Jones S. (2002) First-class modules for Haskell. In International Workshop on Foundations of Object-Oriented Language, pp. 28\u201340."},{"key":"S0956796814000264_ref53","doi-asserted-by":"crossref","unstructured":"Shao Z. (1999) Transparent modules with fully syntactic signatures. In ACM SIGPLAN International Conference on Functional Programming, 220\u2013232.","DOI":"10.21236\/ADA436465"},{"key":"S0956796814000264_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82621-0"},{"key":"S0956796814000264_ref49","first-page":"348","article-title":"First-class structures for Standard ML","volume":"7","author":"Russo","year":"2000","journal-title":"Nord. J. Comput."},{"key":"S0956796814000264_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_5"},{"key":"S0956796814000264_ref22","volume-title":"Advanced Topics in Types and Programming Languages","author":"Harper","year":"2005"},{"key":"S0956796814000264_ref21","first-page":"341","article-title":"Higher-order modules and the phase distinction","author":"Harper","year":"1990","journal-title":"ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"S0956796814000264_ref40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511811326"},{"key":"S0956796814000264_ref18","unstructured":"Harper R. (2012) Programming in Standard ML. Available at: http:\/\/www.cs.cmu.edu\/~rwh\/smlbook\/."},{"key":"S0956796814000264_ref19","doi-asserted-by":"crossref","unstructured":"Harper R. & Lillibridge M. . (1994) A type-theoretic approach to higher-order modules with sharing. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 123\u2013137.","DOI":"10.1145\/174675.176927"},{"key":"S0956796814000264_ref16","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/S0304-3975(96)00300-3","article-title":"Bounded existentials and minimal typing","volume":"193","author":"Pierce","year":"1998","journal-title":"Theor. Comput. Sci."},{"key":"S0956796814000264_ref11","doi-asserted-by":"crossref","unstructured":"Dreyer D. & Blume M. . (2007) Principal type schemes for modular programs. In European Symposium on Programming, pp. 441\u2013457.","DOI":"10.1007\/978-3-540-71316-6_30"},{"key":"S0956796814000264_ref15","unstructured":"Geuvers H. (1992) The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In IEEE Symposium on Logic in Computer Science, 453\u2013460."},{"key":"S0956796814000264_ref13","doi-asserted-by":"crossref","unstructured":"Dreyer D. , Crary K. & Harper R. . (2003) A type system for higher-order modules. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 236\u2013249.","DOI":"10.1145\/604131.604151"},{"key":"S0956796814000264_ref39","doi-asserted-by":"crossref","unstructured":"Montagu B. & R\u00e9my D. (2009) Modeling abstract types in modules with open existential types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 354\u2013365.","DOI":"10.1145\/1594834.1480926"},{"key":"S0956796814000264_ref2","unstructured":"Atkey R. (2012) Relational parametricity for higher kinds. EACSL Annual Conference on Computer Science Logic, pp. 46\u201361."},{"key":"S0956796814000264_ref10","doi-asserted-by":"crossref","unstructured":"Dreyer D. (2007b) A type system for recursive modules. In ACM SIGPLAN International Conference on Functional Programming, 289\u2013302.","DOI":"10.1145\/1291151.1291196"},{"key":"S0956796814000264_ref7","unstructured":"Coq Development Team. (2007) The Coq proof assistant reference manual. INRIA. Available at: http:\/\/coq.inria.fr\/+."},{"key":"S0956796814000264_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199478"},{"key":"S0956796814000264_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006429"},{"key":"S0956796814000264_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480925"},{"key":"S0956796814000264_ref29","doi-asserted-by":"crossref","unstructured":"Leroy X. (1994) Manifest types, modules, and separate compilation. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 109\u2013122.","DOI":"10.1145\/174675.176926"},{"key":"S0956796814000264_ref52","unstructured":"Shan C.-C. (2004) Higher-order modules in System F\u03c9 and Haskell. Technical Report. Available at: http:\/\/www.cs.rutgers.edu\/~ccshan\/xlate\/xlate.pdf."},{"key":"S0956796814000264_ref4","unstructured":"Aydemir B. , Weirich S. & Zdancewic S. . (2009) Abstracting syntax. Technical report."},{"key":"S0956796814000264_ref8","unstructured":"Dreyer D. (2005) Understanding and Evolving the ML Module System. Ph.D. thesis, Carnegie Mellon University."},{"key":"S0956796814000264_ref56","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"key":"S0956796814000264_ref23","doi-asserted-by":"crossref","first-page":"341","DOI":"10.7551\/mitpress\/5641.003.0019","volume-title":"Proof, Language, and Interaction: Essays in Honor of Robin Milner","author":"Harper","year":"2000"},{"key":"S0956796814000264_ref24","doi-asserted-by":"crossref","unstructured":"Jones M. P. (1996) Using parameterized signatures to express modular structure. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 68\u201378.","DOI":"10.1145\/237721.237731"},{"key":"S0956796814000264_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018827"},{"key":"S0956796814000264_ref33","unstructured":"Lillibridge M. (1997) Translucent Sums: A Foundation for Higher-Order Module Systems. Ph.D. thesis, Carnegie Mellon University."},{"key":"S0956796814000264_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16478-1_13"},{"key":"S0956796814000264_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"S0956796814000264_ref42","unstructured":"Romanenko S. , Russo C. V. & Sestoft P. (2000) Moscow ML Version 2.0. Available at: http:\/\/www.dina.kvl.dk\/~sestoft\/mosml."},{"key":"S0956796814000264_ref51","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006442"},{"key":"S0956796814000264_ref27","doi-asserted-by":"crossref","unstructured":"Lee D. K. , Crary K. & Harper R. (2007) Towards a mechanized metatheory of Standard ML. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 173\u2013184.","DOI":"10.1145\/1190216.1190245"},{"key":"S0956796814000264_ref35","doi-asserted-by":"crossref","unstructured":"MacQueen D. B. & Tofte M. (1994) A semantics for higher-order functors. In In European Symposium on Programming, 409\u2013423.","DOI":"10.1007\/3-540-57880-3_27"},{"key":"S0956796814000264_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/169701.169696"},{"key":"S0956796814000264_ref28","doi-asserted-by":"crossref","unstructured":"Leifer J. , Peskine G. , Sewell P. & Wansbrough K. (2003) Global abstraction-safe marshalling with hash types. In ACM SIGPLAN International Conference on Functional Programming, 87\u201398.","DOI":"10.1145\/944705.944714"},{"key":"S0956796814000264_ref30","doi-asserted-by":"crossref","unstructured":"Leroy X. (1995) Applicative functors and fully transparent higher-order modules. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 142\u2013153.","DOI":"10.1145\/199448.199476"},{"key":"S0956796814000264_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001933"},{"key":"S0956796814000264_ref3","doi-asserted-by":"crossref","unstructured":"Aydemir B. , Chargu\u00e9raud A. , Pierce B. C. , Pollack R. . & Weirich S. . (2008) Engineering formal metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 3\u201315.","DOI":"10.1145\/1328438.1328443"},{"key":"S0956796814000264_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"S0956796814000264_ref12","unstructured":"Dreyer D. , Crary K. & Harper R. . (2002) Moscow ML's higher-order modules are unsound. Posting to Types forum, 17 September."},{"key":"S0956796814000264_ref37","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML","author":"Milner","year":"1997"},{"key":"S0956796814000264_ref14","unstructured":"Elsman M. (1999) Program Modules, Separate Compilation, and Intermodule Optimisation. Ph.D. thesis, University of Copenhagen."},{"key":"S0956796814000264_ref34","doi-asserted-by":"crossref","unstructured":"MacQueen D. B. (1986) Using dependent types to express modular structure. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 277\u2013286.","DOI":"10.1145\/512644.512670"},{"key":"S0956796814000264_ref36","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796814000264_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0956796814000264_ref47","unstructured":"Russo C. V. (1998) Types for Modules. Ph.D. thesis, LFCS, University of Edinburgh."},{"key":"S0956796814000264_ref41","unstructured":"Peyton Jones S. (2003) Wearing the hair shirt: a retrospective on Haskell. Invited talk, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Available at: http:\/\/research.microsoft.com\/~simonpj."},{"key":"S0956796814000264_ref43","unstructured":"Rossberg A. (1999) Undecidability of OCaml type checking. Posting to Caml mailing list, 13 July."},{"key":"S0956796814000264_ref6","first-page":"479","volume-title":"Programming Concepts and Methods","author":"Cardelli","year":"1990"},{"key":"S0956796814000264_ref44","article-title":"Mixin' up the ML module system","volume":"35","author":"Rossberg","year":"2013","journal-title":"ACM Trans. Lang. Syst."},{"key":"S0956796814000264_ref45","unstructured":"Rossberg A. , Le Botlan D. , Tack G. & Smolka G. (2004) Alice through the looking glass. In Trends in Functional Programming, 79\u201385."},{"key":"S0956796814000264_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"S0956796814000264_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1708016.1708028"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796814000264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,5]],"date-time":"2024-06-05T04:46:19Z","timestamp":1717562779000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796814000264\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9]]},"references-count":59,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,9]]}},"alternative-id":["S0956796814000264"],"URL":"https:\/\/doi.org\/10.1017\/s0956796814000264","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9]]}}}