{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:40:51Z","timestamp":1767926451868,"version":"3.49.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"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":["2238744"],"award-info":[{"award-number":["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":[[2023,4,6]]},"abstract":"<jats:p>\n            Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, support\n            <jats:italic>typed holes<\/jats:italic>\n            . Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in a\n            <jats:italic>live<\/jats:italic>\n            manner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.\n          <\/jats:p>","DOI":"10.1145\/3586048","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"609-635","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Live Pattern Matching with Typed Holes"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2619-2288","authenticated-orcid":false,"given":"Yongwei","family":"Yuan","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-1751-6470","authenticated-orcid":false,"given":"Scott","family":"Guest","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1693-6172","authenticated-orcid":false,"given":"Eric","family":"Griffis","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8502-1657","authenticated-orcid":false,"given":"Hannah","family":"Potter","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1081-2235","authenticated-orcid":false,"given":"David","family":"Moon","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4502-7971","authenticated-orcid":false,"given":"Cyrus","family":"Omar","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_2_1_2_1","unstructured":"William Aitken. 1992. SML\/NJ Match Compiler Notes. https:\/\/www.smlnj.org\/compiler-notes\/matchcomp.ps \t\t\t\t  William Aitken. 1992. SML\/NJ Match Compiler Notes. https:\/\/www.smlnj.org\/compiler-notes\/matchcomp.ps"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802038"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15975-4_48"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_2_1_6_1","volume-title":"The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics","author":"Barendregt Hendrik Pieter","unstructured":"Hendrik Pieter Barendregt . 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics , Vol. 103). North-Holland. isbn:978-0-444-86748- 3 Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics (Studies in logic and the foundations of mathematics, Vol. 103). North-Holland. isbn:978-0-444-86748-3"},{"key":"e_1_2_1_7_1","unstructured":"Marianne Baudinet and David MacQueen. 1985. Tree Pattern Matching for ML (Extended Abstract). https:\/\/smlfamily.github.io\/history\/Baudinet-DM-tree-pat-match-12-85.pdf \t\t\t\t  Marianne Baudinet and David MacQueen. 1985. Tree Pattern Matching for ML (Extended Abstract). https:\/\/smlfamily.github.io\/history\/Baudinet-DM-tree-pat-match-12-85.pdf"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236798"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/12.1.41"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802037"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547627"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341692"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242760"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408989"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139342131"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784748"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640122"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480927"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3495528"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408991"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547655"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485503"},{"key":"e_1_2_1_28_1","unstructured":"Luc Maranget. 1994. Two Techniques for Compiling Lazy Pattern Matching. HAL-Inria. https:\/\/hal.inria.fr\/inria-00074292\/document \t\t\t\t  Luc Maranget. 1994. Two Techniques for Compiling Lazy Pattern Matching. HAL-Inria. https:\/\/hal.inria.fr\/inria-00074292\/document"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006223"},{"key":"e_1_2_1_30_1","volume-title":"Computer aided manipulation of symbols. Ph. D. Dissertation","author":"McBride Frederick Valentine","unstructured":"Frederick Valentine McBride . 1970. Computer aided manipulation of symbols. Ph. D. Dissertation . Queen\u2019s University Belfast , UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.463849 Frederick Valentine McBride. 1970. Computer aided manipulation of symbols. Ph. D. Dissertation. Queen\u2019s University Belfast, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.463849"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_33_1","volume-title":"Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Department of Computer Science and Engineering","author":"Norell Ulf","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. https:\/\/www.cse.chalmers.se\/~ulfn\/papers\/thesis.pdf 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. https:\/\/www.cse.chalmers.se\/~ulfn\/papers\/thesis.pdf"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290327"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Omar Cyrus","year":"2017","unstructured":"Cyrus Omar , Ian Voysey , Michael Hilton , Jonathan Aldrich , and Matthew A. Hammer . 2017. Hazelnut: a bidirectionally typed structure editor calculus . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017 , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 86\u201399. http:\/\/dl.acm.org\/citation.cfm?id=3009900 Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. 2017. Hazelnut: a bidirectionally typed structure editor calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 86\u201399. http:\/\/dl.acm.org\/citation.cfm?id=3009900"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.11"},{"key":"e_1_2_1_37_1","unstructured":"Simon Peyton Jones Sean Leather and Thijs Alkemade. 2020. Glasgow Haskell Compiler 9.2.1 User\u2019s Guide (Typed Holes). https:\/\/downloads.haskell.org\/ ghc\/latest\/docs\/html\/users_guide\/exts\/typed_holes.html \t\t\t\t  Simon Peyton Jones Sean Leather and Thijs Alkemade. 2020. Glasgow Haskell Compiler 9.2.1 User\u2019s Guide (Typed Holes). https:\/\/downloads.haskell.org\/ ghc\/latest\/docs\/html\/users_guide\/exts\/typed_holes.html"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_2_1_39_1","volume-title":"A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61","author":"Plotkin Gordon D.","year":"2004","unstructured":"Gordon D. Plotkin . 2004. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61 ( 2004 ), 17\u2013139. Gordon D. Plotkin. 2004. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61 (2004), 17\u2013139."},{"key":"e_1_2_1_40_1","volume-title":"Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies. https:\/\/hazel.org\/hazeltutor-hatra2020.pdf","author":"Potter Hannah","year":"2020","unstructured":"Hannah Potter and Cyrus Omar . 2020 . Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies. https:\/\/hazel.org\/hazeltutor-hatra2020.pdf Hannah Potter and Cyrus Omar. 2020. Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies. https:\/\/hazel.org\/hazeltutor-hatra2020.pdf"},{"key":"e_1_2_1_41_1","unstructured":"John Reppy and Mona Zahir. 2019. Compiling Successor ML Pattern Guards. https:\/\/github.com\/JohnReppy\/compiling-pattern-guards\/blob\/master\/ml19-paper.pdf \t\t\t\t  John Reppy and Mona Zahir. 2019. Compiling Successor ML Pattern Guards. https:\/\/github.com\/JohnReppy\/compiling-pattern-guards\/blob\/master\/ml19-paper.pdf"},{"key":"e_1_2_1_42_1","volume-title":"ML pattern match compilation and partial evaluation","author":"Sestoft Peter","unstructured":"Peter Sestoft . 1996. ML pattern match compilation and partial evaluation . In Partial Evaluation, Olivier Danvy, Robert Gl\u00fcck, and Peter Thiemann (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 446\u2013464. isbn:978-3-540-70589-5 Peter Sestoft. 1996. ML pattern match compilation and partial evaluation. In Partial Evaluation, Olivier Danvy, Robert Gl\u00fcck, and Peter Thiemann (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 446\u2013464. isbn:978-3-540-70589-5"},{"key":"e_1_2_1_43_1","unstructured":"Jeremy Siek and Walid Taha. 2006. Gradual typing for functional languages. Scheme and Functional Programming http:\/\/scheme2006.cs.uchicago.edu\/13-siek.pdf \t\t\t\t  Jeremy Siek and Walid Taha. 2006. Gradual typing for functional languages. Scheme and Functional Programming http:\/\/scheme2006.cs.uchicago.edu\/13-siek.pdf"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LIVE.2013.6617346"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364554"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7713722"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586048","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586048","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586048","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:11Z","timestamp":1750178771000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586048"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":51,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586048"],"URL":"https:\/\/doi.org\/10.1145\/3586048","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}