{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:48:08Z","timestamp":1750308488384,"version":"3.41.0"},"reference-count":51,"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\/"}],"funder":[{"DOI":"10.13039\/501100004663","name":"Ministry of Science and Technology, Taiwan","doi-asserted-by":"publisher","award":["109-2222-E-001-002-MY3"],"award-info":[{"award-number":["109-2222-E-001-002-MY3"]}],"id":[{"id":"10.13039\/501100004663","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,8,29]]},"abstract":"<jats:p>Datatype-generic programming is natural and useful in dependently typed languages such as Agda. However, datatype-generic libraries in Agda are not reused as much as they should be, because traditionally they work only on datatypes decoded from a library\u2019s own version of datatype descriptions; this means that different generic libraries cannot be used together, and they do not work on native datatypes, which are preferred by the practical Agda programmer for better language support and access to other libraries. Based on elaborator reflection, we present a framework in Agda featuring a set of general metaprograms for instantiating datatype-generic programs as, and for, a useful range of native datatypes and functions \u2014including universe-polymorphic ones\u2014 in programmer-friendly and customisable forms. We expect that datatype-generic libraries built with our framework will be more attractive to the practical Agda programmer. As the elaborator reflection features used by our framework become more widespread, our design can be ported to other languages too.<\/jats:p>","DOI":"10.1145\/3547629","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"225-253","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Datatype-generic programming meets elaborator reflection"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2439-1048","authenticated-orcid":false,"given":"Hsiang-Shang","family":"Ko","sequence":"first","affiliation":[{"name":"Academia Sinica, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3250-1331","authenticated-orcid":false,"given":"Liang-Ting","family":"Chen","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7656-6225","authenticated-orcid":false,"given":"Tzu-Chi","family":"Lin","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-79108-1_1"},{"key":"e_1_2_1_2_1","unstructured":"Agda Issue. 2022. Loss of Subject Reduction with Set\u03c9. https:\/\/github.com\/agda\/agda\/issues\/5810 Accessed: 2022-03-02 \t\t\t\t  Agda Issue. 2022. Loss of Subject Reduction with Set\u03c9. https:\/\/github.com\/agda\/agda\/issues\/5810 Accessed: 2022-03-02"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290353"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76786-2_4"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/985799.985801"},{"volume-title":"Algebra of Programming","author":"Bird Richard","key":"e_1_2_1_9_1","unstructured":"Richard Bird and Oege de Moor . 1997. Algebra of Programming . Prentice-Hall . isbn:9780135072455 Richard Bird and Oege de Moor. 1997. Algebra of Programming. Prentice-Hall. isbn:9780135072455"},{"volume-title":"Type-Driven Development with Idris","author":"Brady Edwin","key":"e_1_2_1_10_1","unstructured":"Edwin Brady . 2017. Type-Driven Development with Idris . Manning Publications . isbn:9781617293023 Edwin Brady. 2017. Type-Driven Development with Idris. Manning Publications. isbn:9781617293023"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951932"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000182"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000174"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000069"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-b"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"volume-title":"Specializing Type-Indexed Values by Partial Evaluation. Master\u2019s thesis","author":"de Vries Martijn","key":"e_1_2_1_18_1","unstructured":"Martijn de Vries . 2004. Specializing Type-Indexed Values by Partial Evaluation. Master\u2019s thesis . University of Groningen. https :\/\/fse.studenttheses.ub.rug.nl\/8943\/ Martijn de Vries. 2004. Specializing Type-Indexed Values by Partial Evaluation. Master\u2019s thesis. University of Groningen. https:\/\/fse.studenttheses.ub.rug.nl\/8943\/"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976031"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.07.001"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/10704567_23"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76786-2_1"},{"key":"e_1_2_1_25_1","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones Neil D.","year":"2024","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial Evaluation and Automatic Program Generation . Prentice-Hall . isbn:9780130 2024 99 https:\/\/www.itu.dk\/people\/sestoft\/pebook\/ Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall. isbn:9780130202499 https:\/\/www.itu.dk\/people\/sestoft\/pebook\/"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:10)2020"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2021\/5\/7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6954977"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.2201\/NiiPi.2013.10.5"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000307"},{"key":"e_1_2_1_31_1","volume-title":"Siek","author":"Kokke Wen","year":"2020","unstructured":"Wen Kokke , Philip Wadler , and Jeremy G . Siek . 2020 . Programming Language Foundations in Agda (Version 20.07). http:\/\/plfa.inf.ed.ac.uk\/20.07\/ Wen Kokke, Philip Wadler, and Jeremy G. Siek. 2020. Programming Language Foundations in Agda (Version 20.07). http:\/\/plfa.inf.ed.ac.uk\/20.07\/"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.28"},{"volume-title":"Exploring Generic Haskell. Ph. D. Dissertation","author":"Andres L\u00f6h.","key":"e_1_2_1_33_1","unstructured":"Andres L\u00f6h. 2004. Exploring Generic Haskell. Ph. D. Dissertation . Utrecht University . https:\/\/www.andres-loeh.de\/ExploringGH.pdf Andres L\u00f6h. 2004. Exploring Generic Haskell. Ph. D. Dissertation. Utrecht University. https:\/\/www.andres-loeh.de\/ExploringGH.pdf"},{"volume-title":"Less Is More: Generic Programming Theory and Practice. Ph. D. Dissertation","author":"Magalh\u00e3es Jos\u00e9 Pedro","key":"e_1_2_1_34_1","unstructured":"Jos\u00e9 Pedro Magalh\u00e3es . 2012. Less Is More: Generic Programming Theory and Practice. Ph. D. Dissertation . Utrecht University . https:\/\/dreixel.net\/research\/pdf\/thesis.pdf Jos\u00e9 Pedro Magalh\u00e3es. 2012. Less Is More: Generic Programming Theory and Practice. Ph. D. Dissertation. Utrecht University. https:\/\/dreixel.net\/research\/pdf\/thesis.pdf"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41582-1_7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04132-2_15"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_2_1_38_1","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli. \t\t\t\t  Per Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis Napoli."},{"key":"e_1_2_1_39_1","unstructured":"Conor McBride. 2011. Ornamental Algebras Algebraic Ornaments. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/pub\/OAAO\/LitOrn.pdf \t\t\t\t  Conor McBride. 2011. Ornamental Algebras Algebraic Ornaments. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/pub\/OAAO\/LitOrn.pdf"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680500568X"},{"volume-title":"Inductive-inductive definitions. Ph. D. Dissertation","author":"Forsberg Fredrik Nordvall","key":"e_1_2_1_42_1","unstructured":"Fredrik Nordvall Forsberg . 2013. Inductive-inductive definitions. Ph. D. Dissertation . Swansea University . Fredrik Nordvall Forsberg. 2013. Inductive-inductive definitions. Ph. D. Dissertation. Swansea University."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976013"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409021"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_2"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_32"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2841316"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158109"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110273"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Zhixuan Yang and Nicolas Wu. 2022. Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes. To appear at the International Conference on Mathematics of Program Construction (MPC). arxiv:2202.13633 \t\t\t\t  Zhixuan Yang and Nicolas Wu. 2022. Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes. To appear at the International Conference on Mathematics of Program Construction (MPC). arxiv:2202.13633","DOI":"10.1007\/978-3-031-16912-0_9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547629","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547629","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":51,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547629"],"URL":"https:\/\/doi.org\/10.1145\/3547629","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}