{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:02:58Z","timestamp":1784199778048,"version":"3.55.0"},"reference-count":41,"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>At the heart of the Damas-Hindley-Milner (HM) type system lies the abstraction rule which derives a function type for a lambda expression. In this rule, the type of the parameter can be \"guessed\", and can be any type that fits the derivation. The beauty of the HM system is that there always exists a most general type that encompasses all possible derivations \u2013 Algorithm W is used to infer these most general types in practice.<\/jats:p>\n                  <jats:p>Unfortunately, this property is also the bane of the HM type rules. Many languages extend HM typing with additional features which often require complex side conditions to the type rules to maintain principal types. For example, various type systems for impredicative type inference, like HMF, FreezeML, or Boxy types, require let-bindings to always assign most general types. Such a restriction is difficult to specify as a logical deduction rule though, as it ranges over all possible derivations. Despite these complications, the actual implementations of various type inference algorithms are usually straightforward extensions of algorithm W , and from an implementation perspective, much of the complexity of various type system extensions, like boxes or polymorphic weights, is in some sense artificial.<\/jats:p>\n                  <jats:p>\n                    In this article we rephrase the HM\n                    <jats:italic toggle=\"yes\">type rules as type inference under a prefix<\/jats:italic>\n                    , called HMQ. HMQ is sound and complete with respect to the HM type rules, but always derives principal types that correspond to the types inferred by algorithm W. The HMQ type rules are close to the clarity of the declarative HM type rules, but also specific enough to \"read off\" an inference algorithm, and can form an excellent basis to describe type system extensions in practice. We show in particular how to describe the FreezeML and HMF systems in terms of inference under a prefix, and how we no longer require complex side conditions. We also show a novel formalization of static overloading in HMQ as implemented in Koka language.\n                  <\/jats:p>","DOI":"10.1145\/3729308","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1442-1465","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Principal Type Inference under a Prefix: A Fresh Look at Static Overloading"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1027-5430","authenticated-orcid":false,"given":"Daan","family":"Leijen","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3968-6201","authenticated-orcid":false,"given":"Wenjia","family":"Ye","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"},{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Damas and Milner. 1982. Principal Type-Schemes for Functional Programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 207-212. POPL'82. ACM Albuquerque New Mexico. doi:https:\/\/doi.org\/10.1145\/582153.582176 10.1145\/582153.582176.","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","unstructured":"Emrich Lindley Stolarek Cheney and Coates. 2020. FreezeML: Complete and Easy Type Inference for First-Class Polymorphism. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation 423-437. PLDI 2020. ACM London UK. doi:https:\/\/doi.org\/10.1145\/3385412.3386003 10.1145\/3385412.3386003.","DOI":"10.1145\/3385412.3386003"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547642"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2830"},{"key":"e_1_3_2_7_1","unstructured":"Gundry. 2013. Type Inference Haskell and Dependent Types. Phdthesis University of Strathclyde Department of Computer and Information Sciences."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Gundry McBride and McKinna. 2010. Type Inference in Context. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming 43-54. MSFP'10. ACM Baltimore Maryland USA. doi:https:\/\/doi.org\/10.1145\/1863597.1863608 10.1145\/1863597.1863608.","DOI":"10.1145\/1863597.1863608"},{"key":"e_1_3_2_9_1","unstructured":"Heeren. Sep. 2005. Top Quality Type Error Messages. Phdthesis Institute of Information and Computing Sciences Utrecht University. https:\/\/dspace.library.uu.nl\/bitstream\/handle\/1874\/7297\/full.pdf."},{"key":"e_1_3_2_10_1","unstructured":"Heeren Hage and Swierstra. 2002. Generalizing Hindley-Milner Type Inference Algorithms. UU-CS-2002-031. Institute of Information and Computing Sciences Utrecht University. https:\/\/ics-archive.science.uu.nl\/research\/techreps\/repo\/CS-2002\/2002-031.pdf."},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Heeren Leijen and IJzendoorn. 2003. Helium for Learning Haskell. In Proceedings of the 2003 ACM SIGPLAN Workshop on Haskell 62-71. Haskell\u201903. ACM Uppsala Sweden. doi:https:\/\/doi.org\/10.1145\/871895.871902 10.1145\/871895.871902.","DOI":"10.1145\/871895.871902"},{"key":"e_1_3_2_12_1","doi-asserted-by":"crossref","unstructured":"Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society 146. American Mathematical Society: 29-60.","DOI":"10.2307\/1995158"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Jones and Diatchki. 2008. Language and Program Design for Functional Dependencies. In Proc. of the First ACM SIGPLAN Symp. on Haskell 87-98. Haskell7\u201908. ACM Victoria BC Canada. doi:https:\/\/doi.org\/10.1145\/1411286.1411298 10.1145\/1411286.1411298.","DOI":"10.1145\/1411286.1411298"},{"key":"e_1_3_2_14_1","unstructured":"Kiselyov. 2022. How OCaml Type Checker Works \u2013 or What Polymorphism and Garbage.Collection Have in Common. https:\/\/okmij.org\/ftp\/ML\/generalization.html. Blog post."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292538"},{"key":"e_1_3_2_16_1","unstructured":"Le Botlan. 2004. MLF: Une Extension de ML Avec Polymorphisme de Second Ordre et Instanciation Implicite. Phdthesis l\u2019\u00e9cole polytechnique Paris."},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Le Botlan and R\u00e9my. 2003. MLF: Raising ML to the Power of System F. In Proc. of the 8th ACM SIGPLAN Int. Conf. on Functional Programming 27-38. ICFP'03. ACM press Uppsala Sweden. doi:https:\/\/doi.org\/10.1145\/944705.944709 10.1145\/944705.944709.","DOI":"10.1145\/944705.944709"},{"key":"e_1_3_2_18_1","unstructured":"Leijen. Sep. 2007. HMF: Simple Type Inference for First-Class Polymorphism. MSR-TR-2007-118. Microsoft Research."},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Leijen. Sep. 2008. HMF: Simple Type Inference for First-Class Polymorphism. In Proc. of the 13th ACM Symp. of the Int. Conf. on Functional Programming. ICFP'08. Victoria Canada. doi:https:\/\/doi.org\/10.1145\/1411204.1411245 10.1145\/1411204.1411245.","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Leijen. 2009. Flexible Types: Robust Type Inference for First-Class Polymorphism. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 66-77. POPL'09. ACM Savannah GA USA. doi:https:\/\/doi.org\/10.1145\/1480881.1480891 10.1145\/1480881.1480891.","DOI":"10.1145\/1480881.1480891"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Leijen. 2014. Koka: Programming with Row Polymorphic Effect Types. In MSFP'14 5th Workshop on Mathematically Structured Functional Programming. doi:https:\/\/doi.org\/10.4204\/EPTCS.153.8 10.4204\/EPTCS.153.8.","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_2_22_1","unstructured":"Leijen. 2021. The Koka Language. https:\/\/koka-lang.github.io."},{"key":"e_1_3_2_23_1","unstructured":"Leijen and Ye. Sep. 2024. Principal Type Inference under a Prefix \u2013 A Fresh Look at Static Overloading. MSR-TR-2024-34. Microsoft Research."},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Leroy and Mauny. 1993. Dynamics in ML. Journal of Functional Programming 3 (4): 431-463. doi:https:\/\/doi.org\/10.1017\/S0956796800000848 10.1017\/S0956796800000848.","DOI":"10.1017\/S0956796800000848"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Lewis Launchbury Meijer and Shields. 2000. Implicit Parameters: Dynamic Scoping with Static Types. In Proc. of the 27th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages 108-118. POPL'00. ACM Boston MA USA. doi:https:\/\/doi.org\/10.1145\/325694.325708 10.1145\/325694.325708.","DOI":"10.1145\/325694.325708"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48515-5_9"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Odersky and Laufer. 1996. Putting Type Annotations to Work. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 54-57. POPL \u201996. ACM St. Petersburg Beach Florida USA. doi:https:\/\/doi.org\/10.1145\/237721.237729 10.1145\/237721.237729.","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Odersky Zenger and Zenger. 2001. Colored Local Type Inference. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 41-53. POPL \u201901. ACM London United Kingdom. doi:https:\/\/doi.org\/10.1145\/360204.360207 10.1145\/360204.360207.","DOI":"10.1145\/360204.360207"},{"key":"e_1_3_2_30_1","unstructured":"Peyton Jones Jones and Meijer. Jan. 1997. Type Classes: An Exploration of the Design Space. In Haskell Workshop. https:\/\/www.microsoft.com\/en-us\/research\/publication\/type-classes-an-exploration-of-the-design-space\/."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Peyton Jones Vytiniotis Weirich and Shields. 2007. Practical Type Inference for Arbitrary-Rank Types. Journal of Functional Programming 17 (1): 1-82. doi:https:\/\/doi.org\/10.1017\/S0956796806006034 10.1017\/S0956796806006034.","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_2_32_1","unstructured":"Pierce. Feb. 2002. Types and Programming.Languages (TAPL). 1st edition. The MIT Press Cambridge Massachusetts 02142."},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_34_1","unstructured":"R\u00e9my. 1992. Extending ML Type System with a Sorted Equational Theory. Research Report 1766. Rocquencourt BP 105 78153 Le Chesnay Cedex France."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Robinson. Jan. 1965. A Machine-Oriented Logic Based on the Resolution Principle. f. ACM 12 (1). ACM: 23-41. doi:https:\/\/doi.org\/10.1145\/321250.321253 10.1145\/321250.321253.","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Selsam Ullrich and Moura. 2020. Tabled Typeclass Resolution. doi:https:\/\/doi.org\/10.48550\/arXiv.2001.04301 10.48550\/arXiv.2001.04301.","DOI":"10.48550\/arXiv.2001.04301"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Vytiniotis Peyton Jones and Schrijvers. 2010. Let Should Not Be Generalized. In Proc. of the 5th ACM SIGPLAN Workshop on Types in Language Design and Impl. 39-50. TLDI \u201910. ACM Madrid Spain. doi:https:\/\/doi.org\/10.1145\/1708016.1708023 10.1145\/1708016.1708023.","DOI":"10.1145\/1708016.1708023"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Vytiniotis Weirich and Peyton Jones. 2006. Boxy Types: Inference for Higher-Rank Types and Impredicativity. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming 251-262. ICFP \u201906. ACM press Portland Oregon USA. doi:https:\/\/doi.org\/10.1145\/1159803.1159838 10.1145\/1159803.1159838.","DOI":"10.1145\/1159803.1159838"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Wadler and Blott. 1989. How to Make Ad-Hoc Polymorphism Less Ad Hoc. In Proc. of the 16th ACM SIGPLAN-SIGACT Symp. on Principles of Prog. Lang. 60-76. POPL'89. ACM Austin Texas USA. doi:https:\/\/doi.org\/10.1145\/75277.75283 10.1145\/75277.75283.","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Wright and Felleisen. Nov. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115 (1): 38-94. doi:https:\/\/doi.org\/10.1006\/inco.1994.1093 10.1006\/inco.1994.1093.","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Xie and Oliveira. 2018. Let Arguments Go First. Edited by Amal Ahmed. Programming Languages and Systems LNCS 10801. Springer International Publishing: 272-299. doi:https:\/\/doi.org\/10.1007\/978-3-319-89884-1_10 10.1007\/978-3-319-89884-1_10. ESOP'18.","DOI":"10.1007\/978-3-319-89884-1_10"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729308","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:02:56Z","timestamp":1784196176000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729308"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":41,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729308"],"URL":"https:\/\/doi.org\/10.1145\/3729308","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","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"}}]}}