{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T15:41:55Z","timestamp":1787067715796,"version":"build-2736575974"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"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":[[2022,8,29]]},"abstract":"<jats:p>FreezeML is a new approach to first-class polymorphic type inference that  \nemploys term annotations to control when and how polymorphic types are  \ninstantiated and generalised. It conservatively extends Hindley-Milner type  \ninference and was first presented as an extension to Algorithm W. More modern  \ntype inference techniques such as HM(X) and OutsideIn(X) employ constraints to  \nsupport features such as type classes, type families, rows, and other  \nextensions. We take the first step towards modernising FreezeML by presenting  \na constraint-based type inference algorithm. We introduce a new constraint  \nlanguage, inspired by the Pottier\/R\u00e9my presentation of HM(X), in order to allow  \nFreezeML type inference problems to be expressed as constraints. We present a  \ndeterministic stack machine for solving FreezeML constraints and prove its  \ntermination and correctness.<\/jats:p>","DOI":"10.1145\/3547642","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T15:39:26Z","timestamp":1661960366000},"page":"570-595","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Constraint-based type inference for FreezeML"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8591-2740","authenticated-orcid":false,"given":"Frank","family":"Emrich","sequence":"first","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0140-5689","authenticated-orcid":false,"given":"Jan","family":"Stolarek","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1307-9286","authenticated-orcid":false,"given":"James","family":"Cheney","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_2_1","unstructured":"Frank Emrich Sam Lindley Jan Stolarek James Cheney and Jonathan Coates. 2020. FreezeML: Complete and Easy Type Inference for First-class Polymorphism. In PLDI. ACM 423\u2013437. Extended version available at https:\/\/doi.org\/10.48550\/arXiv.2004.00396 \t\t\t\t  Frank Emrich Sam Lindley Jan Stolarek James Cheney and Jonathan Coates. 2020. FreezeML: Complete and Easy Type Inference for First-class Polymorphism. In PLDI. ACM 423\u2013437. Extended version available at https:\/\/doi.org\/10.48550\/arXiv.2004.00396"},{"key":"e_1_2_1_3_1","unstructured":"Frank Emrich Jan Stolarek James Cheney and Sam Lindley. 2022. Constraint-based type inference for FreezeML (extended version). https:\/\/doi.org\/10.48550\/arXiv.2207.09914 arXiv:2207.09914 \t\t\t\t  Frank Emrich Jan Stolarek James Cheney and Sam Lindley. 2022. Constraint-based type inference for FreezeML (extended version). https:\/\/doi.org\/10.48550\/arXiv.2207.09914 arXiv:2207.09914"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2830"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804305"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2830"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00005-0"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17685-2_8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292538"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944709"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000848"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/175469.175475"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628145"},{"key":"e_1_2_1_19_1","volume-title":"The Essence of ML Type Inference","author":"Pottier Fran\u00e7ois","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my . 2005. The Essence of ML Type Inference . MIT Press , 389\u2013489. Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. The Essence of ML Type Inference. MIT Press, 389\u2013489."},{"key":"e_1_2_1_20_1","volume-title":"Extension of ML Type System with a Sorted Equational Theory on Types","author":"R\u00e9my Didier","unstructured":"Didier R\u00e9my . 1992. Extension of ML Type System with a Sorted Equational Theory on Types . Institut National de Recherche en Informatique et en Automatique . Didier R\u00e9my. 1992. Extension of ML Type System with a Sorted Equational Theory on Types. Institut National de Recherche en Informatique et en Automatique."},{"key":"e_1_2_1_21_1","volume-title":"Russo and Dimitrios Vytiniotis","author":"Claudio","year":"2009","unstructured":"Claudio V. Russo and Dimitrios Vytiniotis . 2009 . QML : Explicit First-class Polymorphism for ML. In ML. ACM , 3\u201314. Claudio V. Russo and Dimitrios Vytiniotis. 2009. QML: Explicit First-class Polymorphism for ML. In ML. ACM, 3\u201314."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180476"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159838"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Mitchell Wand. 1987. A simple algorithm and proof for type inference. Fundamenta Informaticae. \t\t\t\t  Mitchell Wand. 1987. A simple algorithm and proof for type inference. Fundamenta Informaticae.","DOI":"10.3233\/FI-1987-10202"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316068"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01018828"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547642","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547642","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:43:29Z","timestamp":1750257809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547642"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":29,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547642"],"URL":"https:\/\/doi.org\/10.1145\/3547642","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}