{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:56Z","timestamp":1780994696101,"version":"3.54.1"},"reference-count":51,"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\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2238744"],"award-info":[{"award-number":["CCF-2238744"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,1,2]]},"abstract":"<jats:p>Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states.<\/jats:p>\n          <jats:p>\n            The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e., the system identifies unfillable holes using a system of traced provenances, rather than localized in an\n            <jats:italic toggle=\"yes\">ad hoc<\/jats:italic>\n            manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.\n          <\/jats:p>","DOI":"10.1145\/3632910","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2041-2068","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Total Type Error Localization and Recovery with Holes"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-4969-2376","authenticated-orcid":false,"given":"Eric","family":"Zhao","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5097-6519","authenticated-orcid":false,"given":"Raef","family":"Maroof","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3141-9144","authenticated-orcid":false,"given":"Anand","family":"Dukkipati","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6938-7379","authenticated-orcid":false,"given":"Andrew","family":"Blinn","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5141-5666","authenticated-orcid":false,"given":"Zhiyi","family":"Pan","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4502-7971","authenticated-orcid":false,"given":"Cyrus","family":"Omar","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3550355.3552452"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622812"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/VL\/HCC53370.2022.9833110"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236798"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_1_7_1","unstructured":"Yair Chuchem and Eyal Lotem. 2019. Steady Typing."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462161"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2019.102373"},{"key":"e_1_3_1_11_1","article-title":"Bidirectional Typing","author":"Dunfield Jana","year":"2019","unstructured":"Jana Dunfield and Neel Krishnaswami. 2019. Bidirectional Typing. CoRR abs\/1908.05839 (2019). arXiv:1908.05839 http:\/\/arxiv.org\/abs\/1908.05839","journal-title":"CoRR"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36575-3_20"},{"key":"e_1_3_1_15_1","unstructured":"HaskellWiki. 2014. GHC\/Typed holes \u2014 HaskellWiki. https:\/\/wiki.haskell.org\/index.php?title=GHC\/Typed_holes&oldid=58717 [Online; accessed 2-March-2023]."},{"key":"e_1_3_1_16_1","unstructured":"Hazel Development Team. 2023. Hazel. http:\/\/hazel.org\/. http:\/\/hazel.org\/"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/871895.871902"},{"key":"e_1_3_1_18_1","volume-title":"Resolution d\u2019Equations dans les langages d\u2019ordre 1, 2, \u2026, omega","author":"Huet G\u00e9rard P.","year":"1976","unstructured":"G\u00e9rard P. Huet. 1976. Resolution d\u2019Equations dans les langages d\u2019ordre 1, 2, \u2026, omega. Ph. D. Dissertation. Universit\u00e9 de Paris VII."},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000599"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"e_1_3_1_21_1","volume-title":"Bidirectional Typing for the Calculus of Inductive Constructions. (Typage Bidirectionnel pour le Calcul des Constructions Inductives)","author":"Lennon-Bertrand Meven","year":"2022","unstructured":"Meven Lennon-Bertrand. 2022. Bidirectional Typing for the Calculus of Inductive Constructions. (Typage Bidirectionnel pour le Calcul des Constructions Inductives). Ph. D. Dissertation. University of Nantes, France. https:\/\/tel.archives-ouvertes.fr\/tel-03848595"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48515-5_9"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3546196.3550164"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/VL-HCC57772.2023.00016"},{"key":"e_1_3_1_25_1","volume-title":"Towards a practical programming language based on dependent type theory","author":"Norell Ulf","year":"2007","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden."},{"key":"e_1_3_1_26_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_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290327"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2017.11"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660230"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563835.3567654"},{"key":"e_1_3_1_34_1","article-title":"Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies","author":"Potter Hannah","year":"2020","unstructured":"Hannah Potter and Cyrus Omar. 2020. Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies. Human Aspects of Types and Reasoning Assistants (HATRA) (2020).","journal-title":"Human Aspects of Types and Reasoning Assistants (HATRA)"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628145"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32037-8_1"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951915"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3138818"},{"key":"e_1_3_1_39_1","article-title":"Gradual Typing for Functional Languages","author":"Siek Jeremy G.","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop.","journal-title":"Scheme and Functional Programming Workshop"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1408681.1408688"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SNAPL.2015.274"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-012-0249-7"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1943371.1943391"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358755"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/366378.366379"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276502"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1002\/SPE.2187"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512648"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586048"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535870"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Eric Zhao Raef Maroof Anand Dukkipati Andrew Blinn Zhiyi Pan and Cyrus Omar. 2023. Artifact for Total Type Error Localization and Recovery with Holes. https:\/\/doi.org\/10.5281\/zenodo.10129703 10.5281\/zenodo.10129703","DOI":"10.5281\/zenodo.10129703"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632910","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632910","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632910","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:18Z","timestamp":1751659638000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632910"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":51,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632910"],"URL":"https:\/\/doi.org\/10.1145\/3632910","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"}}]}}