{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:51:00Z","timestamp":1770288660182,"version":"3.49.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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,1,2]]},"abstract":"<jats:p>\n            We propose a new language feature for ML-family languages, the ability to selectively\n            <jats:italic toggle=\"yes\">unbox<\/jats:italic>\n            certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusion, that is, distinct values with the same representation.\n          <\/jats:p>\n          <jats:p>We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes.<\/jats:p>\n          <jats:p>\n            Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>\u03bb<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our algorithm turns out to be closely related to the normalization strategy for macro expansion in the\n            <jats:monospace>cpp<\/jats:monospace>\n            preprocessor.\n          <\/jats:p>","DOI":"10.1145\/3632893","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1509-1539","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Unboxed Data Constructors: Or, How cpp Decides a Halting Problem"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-4174-2088","authenticated-orcid":false,"given":"Nicolas","family":"Chataing","sequence":"first","affiliation":[{"name":"ENS Paris, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4609-9101","authenticated-orcid":false,"given":"Stephen","family":"Dolan","sequence":"additional","affiliation":[{"name":"Jane Street, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1758-3938","authenticated-orcid":false,"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1650-6340","authenticated-orcid":false,"given":"Jeremy","family":"Yallop","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"\u00d6mer S\u00ednan A\u011facan. 2016. GHC unboxed sums. https:\/\/github.com\/ghc\/ghc\/commit\/714bebff44076061d0a719c4eda2cfd213b7ac3d"},{"key":"e_1_3_1_3_1","unstructured":"Noah Lev Bartell-Mangel. 2022. Filling a Niche: Using Spare Bits to Optimize Data Representations. https:\/\/www.noahlev.org\/papers\/popl22src-filling-a-niche.pdfPOPL\u201922 student research presentation."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607858"},{"key":"e_1_3_1_5_1","unstructured":"Aria Beingessner. 2015. Rust RFC 1230: More Exotic Enum Layout Optimizations. https:\/\/github.com\/rust-lang\/rfcs\/issues\/1230"},{"key":"e_1_3_1_6_1","unstructured":"Michael Benfield. 2022. rustc PR 94075: Use niche-filling optimization even when multiple variants have data. https:\/\/github.com\/rust-lang\/rust\/pull\/94075"},{"key":"e_1_3_1_7_1","article-title":"Full Reduction at Full Throttle","author":"Boespflug Mathieu","year":"2011","unstructured":"Mathieu Boespflug, Maxime D\u00e9n\u00e8s, Benjamin Gr\u00e9goire. 2011. Full Reduction at Full Throttle. In CPP. https:\/\/inria.hal.science\/hal-00650940","journal-title":"In CPP"},{"key":"e_1_3_1_8_1","unstructured":"Eduard-Mihai Burtescu. 2017. rustc PR 45225: Refactor type memory layouts and ABIs to be more general and easier to optimize. https:\/\/github.com\/rust-lang\/rust\/pull\/45225"},{"key":"e_1_3_1_9_1","unstructured":"Lloyd Chan. 2017. Scala Pre-SIP: Unboxed wrapper types. https:\/\/contributors.scala-lang.org\/t\/pre-sip-unboxed-wrapper-types\/987"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571240"},{"key":"e_1_3_1_11_1","unstructured":"Simon Colin Rodolphe LepigreGabriel Scherer. 2019. In JFLA Unboxing Mutually Recursive Type Definitions in OCaml. https:\/\/hal.inria.fr\/hal-01929508"},{"key":"e_1_3_1_12_1","unstructured":"Stephen Compall. 2017. Blog post: the high cost of AnyVal classes. https:\/\/failex.blogspot.com\/2017\/04\/the-high-cost-of-anyval-subclasses.html"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086387"},{"key":"e_1_3_1_14_1","unstructured":"Torbj\u00f6rn Granlund and contributors. 1991. GMP. https:\/\/gmplib.org\/"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/800068.802129"},{"issue":"2","key":"e_1_3_1_16_1","article-title":"A short proof of the decidability of normalization in recursive program schemes","volume":"25","author":"Khasidashvil Zurab","year":"2020","unstructured":"Zurab Khasidashvil. 2020. A short proof of the decidability of normalization in recursive program schemes. In Shalva Pkhakadze\u2019s Festschrift, AMIM Vol. 25 No. 2. http:\/\/www.viam.science.tsu.ge\/Ami\/2020_2\/5_zura.pdf","journal-title":"In Shalva Pkhakadze\u2019s Festschrift, AMIM"},{"key":"e_1_3_1_17_1","unstructured":"Simon Marlow. 2003. GHC\u2019s UNPACK pragma. https:\/\/github.com\/ghc\/ghc\/commit\/abbc5a0be1df84a33015470319062ed7a3aa3153"},{"key":"e_1_3_1_18_1","unstructured":"Antoine Min\u00e9 and Xavier Leroy. 2012. Zarith. https:\/\/github.com\/ocaml\/Zarith\/"},{"key":"e_1_3_1_19_1","unstructured":"Martin Odersky and Adriaan Moors. 2018. dotty PR 5300: Opaque types. https:\/\/github.com\/lampepfl\/dotty\/pull\/5300"},{"key":"e_1_3_1_20_1","unstructured":"Erik Osheim Jorge Vicente Cantero and S\u00e9bastien Doeraene. 2017. Scala SIP 35: Opaque types. https:\/\/contributors.scala-lang.org\/t\/pre-sip-unboxed-wrapper-types\/987"},{"key":"e_1_3_1_21_1","unstructured":"Simon Peyton-Jones. 2007. GHC view patterns. https:\/\/gitlab.haskell.org\/ghc\/ghc\/-\/wikis\/view-patterns"},{"key":"e_1_3_1_22_1","unstructured":"Gordon Plotkin. 2022. Recursion does not always help. https:\/\/arxiv.org\/pdf\/2206.08413.pdf"},{"key":"e_1_3_1_23_1","unstructured":"Dave Prosser. 1986. X3J11\/86-196: Complete macro expansion algorithm. https:\/\/www.spinellis.gr\/blog\/20060626\/x3J11-86-196.pdf"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"Sylvain Salvati and Igor Walukiewicz. 2015. Using models to model-check recursive schemes. Logical Methods in Computer Science Volume 11 Issue 2 (June 2015). http:\/\/doi.org\/10.2168\/LMCS-11(2:7)2015","DOI":"10.2168\/LMCS-11(2:7)2015"},{"key":"e_1_3_1_25_1","unstructured":"Diomidis Spinellis. 2008. A corrected and annotated version of the X4J11\/86-196 document. https:\/\/www.spinellis.gr\/blog\/20060626\/"},{"key":"e_1_3_1_26_1","unstructured":"Don Syme. 2016. Fsharp PR 1395: struct discriminated unions. https:\/\/github.com\/dotnet\/fsharp\/pull\/1395"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Don Syme Gregory Neverov and James Margetson. 2007. Extensible Pattern Matching via a Lightweight Language Extension. In ICFP\u201907 (ICFP \u201907). https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/p29-syme.pdf","DOI":"10.1145\/1291151.1291159"},{"key":"e_1_3_1_28_1","unstructured":"The C++ standard committee working group SG12. 2014. n3882; An update to the preprocessor specification. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2014\/n3882.pdf"},{"key":"e_1_3_1_29_1","unstructured":"The C standard committee working group WG14. 1992. Defect report 017. https:\/\/www.open-std.org\/Jtc1\/sc22\/wg14\/www\/docs\/dr_017.html"},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"David A. Turner. 1979. A new implementation technique for applicative languages. In Software - Practice and Experience.","DOI":"10.1002\/spe.4380090105"},{"key":"e_1_3_1_31_1","volume-title":"In ML Workshop Whole-Program Compilation in MLton","author":"Weeks Stephen","year":"2006","unstructured":"Stephen Weeks. 2006. In ML Workshop Whole-Program Compilation in MLton. http:\/\/www.mlton.org\/References.attachments\/060916-mlton.pdf"},{"key":"e_1_3_1_32_1","author":"Yallop Jeremy","year":"2020","unstructured":"Jeremy Yallop. 2020. OCaml RFC: constructor unboxing. https:\/\/github.com\/ocaml\/RFCs\/pull\/14","journal-title":"OCaml RFC: constructor unboxing"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632893","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632893","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:03Z","timestamp":1751659503000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632893"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632893"],"URL":"https:\/\/doi.org\/10.1145\/3632893","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}