{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T21:18:25Z","timestamp":1764364705632,"version":"build-2065373602"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG-448316946"],"award-info":[{"award-number":["DFG-448316946"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general formal treatments in the published literature. Moreover, it is commonly believed to be incompatible with higher-rank polymorphism.\n \n \n \nIn this paper, we formally present a simple monomorphization technique based on a type-based flow analysis that generalizes to programs with higher-rank types, existential types, and arbitrary combinations. Inspired by algebraic subtyping, we track the flow of type instantiations through the program. Our approach only supports monomorphization up to polymorphic recursion, which we uniformly detect as cyclic flow. Treating universal and existential quantification uniformly, we identify a novel form of polymorphic recursion in the presence of existential types, which we coin polymorphic packing. We study the meta-theory of our approach, showing that our translation is type-preserving and preserves semantics step-wise.<\/jats:p>","DOI":"10.1145\/3720472","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1015-1041","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The Simple Essence of Monomorphization"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2904-5099","authenticated-orcid":false,"given":"Matthew","family":"Lutze","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8011-0506","authenticated-orcid":false,"given":"Philipp","family":"Schuster","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289435"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622812"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546196.3550163"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286957"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Henry Cejtin Suresh Jagannathan and Stephen Weeks. 2000. Flow-directed closure conversion for typed languages. In Programming Languages and Systems: 9th European Symposium on Programming ESOP 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2000 Berlin Germany March 25\u2013April 2 2000 Proceedings 9. 56\u201371.","DOI":"10.1007\/3-540-46425-5_4"},{"key":"e_1_2_1_6_1","volume-title":"Algebraic Subtyping: Distinguished Dissertation","author":"Dolan Stephen","year":"2017","unstructured":"Stephen Dolan. 2017. Algebraic Subtyping: Distinguished Dissertation 2017. BCS, Swindon, GBR. isbn:1780174152"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062357"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428217"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995158"},{"key":"e_1_2_1_11_1","volume-title":"High-Performance Defunctionalisation in Futhark. In International Symposium on Trends in Functional Programming. 136\u2013156","author":"Hovgaard Anders Kiel","year":"2018","unstructured":"Anders Kiel Hovgaard, Troels Henriksen, and Martin Elsman. 2018. High-Performance Defunctionalisation in Futhark. In International Symposium on Trends in Functional Programming. 136\u2013156."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378797"},{"volume-title":"Call-by-Push-Value: A Subsuming Paradigm","author":"Levy Paul Blain","key":"e_1_2_1_13_1","unstructured":"Paul Blain Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm. In Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 228\u2013243. isbn:978-3-540-48959-7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Matthew Lutze Philipp Schuster and Jonathan Immanuel Brachth\u00e4user. 2025. The Simple Essence of Monomorphization (Artifact). https:\/\/doi.org\/10.5281\/zenodo.14591555 10.5281\/zenodo.14591555","DOI":"10.5281\/zenodo.14591555"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-12925-1_41"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_2_1_18_1","unstructured":"Bjarne Stroustrup. 2013. The C++ programming language. Pearson Education."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjjip.26.54"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003086"},{"key":"e_1_2_1_21_1","first-page":"1","article-title":"Whole-program compilation in MLton","volume":"6","author":"Weeks Stephen","year":"2006","unstructured":"Stephen Weeks. 2006. Whole-program compilation in MLton. ML, 6 (2006), 1\u20131.","journal-title":"ML"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720472","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720472","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:10:26Z","timestamp":1760029826000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720472"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":21,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720472"],"URL":"https:\/\/doi.org\/10.1145\/3720472","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}