{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:12:43Z","timestamp":1770282763726,"version":"3.49.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>ML modules come as an additional layer on top of a core language to offer  \nlarge-scale notions of composition and abstraction. They largely  \ncontributed to the success of OCaml and SML. While modules are easy to write  \nfor common cases, their advanced use may become tricky. Additionally,  \ndespite a long line of works, their meta-theory remains difficult to  \ncomprehend, with involved soundness proofs. In fact, the module layer of  \nOCaml does not currently have a formal specification and its implementation  \nhas some surprising behaviors.<\/jats:p>\n          <jats:p>Building on previous translations from ML modules to F\u03c9, we propose a type  \nsystem, called M\u03c9, that covers a large subset of OCaml modules, including  \nboth applicative and generative functors, and extended with transparent  \nascription. This system produces signatures in an OCaml-like syntax extended  \nwith F\u03c9 quantifiers. We provide a reverse translation from M\u03c9 signatures to  \npath-based source signatures along with a characterization of signature  \navoidance cases, making M\u03c9 signatures well suited to serve as a new internal  \nrepresentation for a typechecker.<\/jats:p>\n          <jats:p>The soundness of the type system is shown by elaboration in F\u03c9. We improve  \nover previous encodings of sealing within applicative functors, by the  \nintroduction of transparent existential types, a weaker form of existential  \ntypes that can be lifted out of universal and arrow types. This shines a new  \nlight on the form of abstraction provided by applicative functors and brings  \ntheir treatment much closer to those of generative functors.<\/jats:p>","DOI":"10.1145\/3649818","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"194-222","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Fulfilling OCaml Modules with Transparency"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6333-6092","authenticated-orcid":false,"given":"Blaudeau","family":"Clement","sequence":"first","affiliation":[{"name":"Inria, Paris, France \/ Universit\u00e9 de Paris Cit\u00e9, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0693-6278","authenticated-orcid":false,"given":"Didier","family":"R\u00e9my","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2107-7678","authenticated-orcid":false,"given":"Gabriel","family":"Radanne","sequence":"additional","affiliation":[{"name":"Inria, Lyon, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199478"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Blaudeau Didier R\u00e9my and Gabriel Radanne. 2024. Fulfilling OCaml modules with transparency (supplementary material). https:\/\/doi.org\/10.1145\/3649818 10.1145\/3649818","DOI":"10.1145\/3649818"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009892"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290323"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000222"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006429"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604151"},{"key":"e_1_2_2_8_1","unstructured":"Derek Dreyer Robert Harper and Karl Crary. 2005. Understanding and evolving the ML module system. Ph. D. Dissertation. USA. isbn:0542015501 AAI3166274"},{"key":"e_1_2_2_9_1","volume-title":"ML Family\/OCaml Users and Developers workshops. https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/papers\/modalias.pdf","author":"Guarrigue Jacques","year":"2014","unstructured":"Jacques Guarrigue and Leo White. 2014. Type-level module aliases: independent and equal. ML Family\/OCaml Users and Developers workshops. https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/papers\/modalias.pdf"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96744"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199476"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512670"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318606"},{"key":"e_1_2_2_18_1","unstructured":"Beno\u00eet Montagu. 2010. Programming with first-class modules in a core language with subtyping singleton kinds and open existential types. (Programmer avec des modules de premi\u00e8re classe dans un langage noyau pourvu de sous-typage sortes singletons et types existentiels ouverts). \u00c9cole Polytechnique Palaiseau France. https:\/\/tel.archives-ouvertes.fr\/tel-00550331"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480926"},{"key":"e_1_2_2_20_1","unstructured":"Gabriel Radanne Thomas Gazagnaire Anil Madhavapeddy Jeremy Yallop Richard Mortier Hannes Mehnert Mindy Perston and David Scott. 2019. Programming Unikernels in the Large via Functor Driven Development. arxiv:1905.02529."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000205"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450137"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000264"},{"key":"e_1_2_2_24_1","first-page":"348","article-title":"First-Class Structures for Standard ML","volume":"7","author":"Russo Claudio V.","year":"2000","unstructured":"Claudio V. Russo. 2000. First-Class Structures for Standard ML. Nord. J. Comput., 7, 4 (2000), 348\u2013374.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82621-0"},{"key":"e_1_2_2_26_1","unstructured":"Chung-Chieh Shan. 2004. Higher-order modules in System F^\u03c9 and Haskell. 01."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317801"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632866"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.198.2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649818","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649818","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649818"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":29,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649818"],"URL":"https:\/\/doi.org\/10.1145\/3649818","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}