{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:57:36Z","timestamp":1787061456454,"version":"build-2736575974"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S028129\/1,EP\/T008911\/1"],"award-info":[{"award-number":["EP\/S028129\/1,EP\/T008911\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2022,1,16]]},"abstract":"<jats:p>Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs.<\/jats:p>\n                  <jats:p>\n                    We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus \u03bb\n                    <jats:sup>\u21d2<\/jats:sup>\n                    that elaborates into an explicit core calculus\n                    <jats:italic>F<\/jats:italic>\n                    . We show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations.\n                  <\/jats:p>\n                  <jats:p>Our design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation.<\/jats:p>","DOI":"10.1145\/3498723","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Staging with class: a specification for typed template Haskell"],"prefix":"10.1145","volume":"6","author":[{"given":"Ningning","family":"Xie","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Pickering","sequence":"additional","affiliation":[{"name":"Well-Typed LLP, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andres","family":"L\u00f6h","sequence":"additional","affiliation":[{"name":"Well-Typed LLP, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeremy","family":"Yallop","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-630X","authenticated-orcid":false,"given":"Meng","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Bristol, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.5"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122967"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173724"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/954186.954190"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1090189.1086397"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Daniel Gratzer GA Kavvos Andreas Nuyts and Lars Birkedal. 2020. Multimodal Dependent Type Theory. In submission.  Daniel Gratzer GA Kavvos Andreas Nuyts and Lars Birkedal. 2020. Multimodal Dependent Type Theory. In submission.","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_7"},{"key":"e_1_2_2_11_1","volume-title":"Coherence for qualified types","author":"Jones M.P.","unstructured":"M.P. Jones . 1993. Coherence for qualified types . Yale University , Dept . of Computer Science. M.P. Jones. 1993. Coherence for qualified types. Yale University, Dept. of Computer Science."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660241"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_4"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_6"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.241.1"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_15"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_11"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314625"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581498"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136040.3136049"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581499"},{"key":"e_1_2_2_25_1","volume-title":"Haskell Workshop.","author":"Jones Simon Peyton","year":"1997","unstructured":"Simon Peyton Jones , Mark Jones , and Erik Meijer . 1997 . Type classes: an exploration of the design space . In Haskell Workshop. Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: an exploration of the design space. In Haskell Workshop."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871845"},{"key":"e_1_2_2_28_1","unstructured":"Matthew Pickering. 2019. Overloaded Quotations. GHC proposal. https:\/\/github.com\/ghc-proposals\/ghc-proposals\/blob\/master\/proposals\/0246-overloaded-bracket.rst  Matthew Pickering. 2019. Overloaded Quotations. GHC proposal. https:\/\/github.com\/ghc-proposals\/ghc-proposals\/blob\/master\/proposals\/0246-overloaded-bracket.rst"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409021"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3331545.3342597"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868314"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.14288\/1.0166800"},{"key":"e_1_2_2_34_1","volume-title":"Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann","author":"Schuster Philipp","year":"2020","unstructured":"Philipp Schuster , Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann . 2020 . Zero-cost Effect Handlers by Staging. In submission. Philipp Schuster, Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann. 2020. Zero-cost Effect Handlers by Staging. In submission."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278122.3278139"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Walid Taha and Tim Sheard. 1998. Multi-stage programming: Axiomatization and type safety. In International Colloquium on Automata Languages and Programming. 918\u2013929.  Walid Taha and Tim Sheard. 1998. Multi-stage programming: Axiomatization and type safety. In International Colloquium on Automata Languages and Programming. 918\u2013929.","DOI":"10.1007\/BFb0055113"},{"key":"e_1_2_2_41_1","volume-title":"Multistage programming: its theory and applications","author":"Taha Walid Mohamed","unstructured":"Walid Mohamed Taha . 1999. Multistage programming: its theory and applications . Oregon Graduate Institute of Science and Technology . Walid Mohamed Taha. 1999. Multistage programming: its theory and applications. Oregon Graduate Institute of Science and Technology."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_14"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.198.2"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409002"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110273"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236795"},{"key":"e_1_2_2_49_1","volume-title":"Modular Macros. OCaml Users and Developers Workshop.","author":"Yallop Jeremy","year":"2015","unstructured":"Jeremy Yallop and Leo White . 2015 . Modular Macros. OCaml Users and Developers Workshop. Jeremy Yallop and Leo White. 2015. Modular Macros. OCaml Users and Developers Workshop."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498723","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498723","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:29Z","timestamp":1750174229000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498723"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498723"],"URL":"https:\/\/doi.org\/10.1145\/3498723","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}