{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:13:00Z","timestamp":1787062380428,"version":"build-2736575974"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    Modern functional languages rely on sophisticated type inference algorithms. However, there often exists a gap between the theoretical presentation of these algorithms and their practical implementations. Specifically, implementations employ techniques not explicitly included in formal specifications, causing undesirable consequences. First, this leads to confusion and unforeseen challenges for developers adhering to the formal specification. Moreover, theoretical guarantees established for a formal presentation may not directly translate to the implementation. This paper focuses on formalizing one such technique, known as\n                    <jats:italic toggle=\"yes\">levels<\/jats:italic>\n                    , which is widely used in practice but whose theoretical treatment remains largely understudied. We present the first comprehensive formalization of levels and demonstrate their applicability to type inference implementations.\n                  <\/jats:p>","DOI":"10.1145\/3729338","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"2180-2203","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Practical Type Inference with Levels"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2124-9625","authenticated-orcid":false,"given":"Andong","family":"Fan","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2548-6866","authenticated-orcid":false,"given":"Han","family":"Xu","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5961-1493","authenticated-orcid":false,"given":"Ningning","family":"Xie","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9225-2"},{"key":"e_1_3_2_3_2","unstructured":"James Cheney and Ralf Hinze. 2003. First-class phantom types. Technical Report. Cornell University."},{"key":"e_1_3_2_4_2","unstructured":"Team Coq. 2024. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_3_2_5_2","first-page":"207","article-title":"Principal type-schemes for functional programs","author":"Damas Luis","year":"1982","unstructured":"Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 207\u2013212.","journal-title":"Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473569"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535856"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386003"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Andong Fan Han Xu and Ningning Xie. 2025. Practical Type Inference with Levels (Artifact). 10.5281\/zenodo.15334601","DOI":"10.5281\/zenodo.15334601"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"Jacques Garrigue. 2004. Relaxing the value restriction. In International Symposium on Functional and Logic Programming. Springer 196\u2013213.","DOI":"10.1007\/978-3-540-24754-8_15"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000066"},{"key":"e_1_3_2_14_2","doi-asserted-by":"crossref","unstructured":"Jacques Garrigue and Didier R\u00e9my. 2013. Ambivalent types for principal type inference with GADTs. In Programming Languages and Systems: 11th Asian Symposium APLAS 2013 Melbourne VIC Australia December 9-11 2013. Proceedings. Springer 257\u2013272.","DOI":"10.1007\/978-3-319-03542-0_19"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Adam Gundry Conor McBride and James McKinna. 2010. Type inference in context. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (Baltimore Maryland USA) (MSFP \u201910). Association for Computing Machinery New York NY USA 43\u201354. 10.1145\/1863597.1863608","DOI":"10.1145\/1863597.1863608"},{"key":"e_1_3_2_16_2","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley Roger","year":"1969","unstructured":"Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (1969), 29\u201360.","journal-title":"Transactions of the American Mathematical Society"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","unstructured":"Kazuki Ikemori Youyou Cong Hidehiko Masuhara and Daan Leijen. 2022. Sound and Complete Type Inference for Closed Effect Rows. In Trends in Functional Programming. Wouter Swierstra and Nicolas Wu (Eds.). Springer International Publishing Cham 144\u2013168.","DOI":"10.1007\/978-3-031-21314-4_8"},{"key":"e_1_3_2_18_2","unstructured":"Oleg Kiselyov. 2022. How OCaml type checker works \u2013 or what polymorphism and garbage collection have in common. (2022). https:\/\/okmij.org\/ftp\/ML\/generalization.html"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292538"},{"key":"e_1_3_2_20_2","first-page":"78","article-title":"An extension of ML with first-class abstract types","author":"L\u00e4ufer Konstantin","year":"1992","unstructured":"Konstantin L\u00e4ufer and Martin Odersky. 1992. An extension of ML with first-class abstract types. In ACM SIGPLAN Workshop on ML and its Applications. 78\u201391.","journal-title":"ACM SIGPLAN Workshop on ML and its Applications"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Daan Leijen. 2013. Koka: Programming with Row-Polymorphic Effect Types. Technical Report MSR-TR-2013-79. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/koka-programming-with-row-polymorphic-effect-types\/","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3386336"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Martin Odersky and Konstantin L\u00e4ufer. 1996. Putting type annotations to work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg Beach Florida USA) (POPL \u201996). Association for Computing Machinery New York NY USA 54\u201367. 10.1145\/237721.237729","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632890"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/1160074.1159811"},{"key":"e_1_3_2_28_2","unstructured":"Gordon Plotkin and John Power. 2001. Adequacy for algebraic effects. In Foundations of Software Science and Computation Structures: 4th International Conference FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2001 Genova Italy April 2\u20136 2001 Proceedings. Springer 1\u201324."},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","unstructured":"Gordon Plotkin and Matija Pretnar. 2009. Handlers of algebraic effects. In Programming Languages and Systems: 18th European Symposium on Programming ESOP 2009 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS 2009 York UK March 22\u201329 2009 Proceedings. Springer 80\u201394.","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_30_2","unstructured":"Didier R\u00e9my. 1992. Extension of ML type system with a sorted equation theory on types. Ph. D. Dissertation. INRIA."},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804314"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"},{"key":"e_1_3_2_35_2","article-title":"Higher-rank polymorphism: type inference and extensions","author":"Xie Ningning","year":"2021","unstructured":"Ningning Xie. 2021. Higher-rank polymorphism: type inference and extensions. HKU Theses Online (HKUTO) (2021).","journal-title":"HKU Theses Online (HKUTO)"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371121"},{"key":"e_1_3_2_37_2","first-page":"53","article-title":"Giving Haskell a promotion","author":"Yorgey Brent A","year":"2012","unstructured":"Brent A Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and Jos\u00e9 Pedro Magalh\u00e3es. 2012. Giving Haskell a promotion. In Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation. 53\u201366.","journal-title":"Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_36"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341716"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729338","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:04:31Z","timestamp":1784196271000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729338"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":38,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729338"],"URL":"https:\/\/doi.org\/10.1145\/3729338","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}