{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:13:15Z","timestamp":1767928395443,"version":"3.49.0"},"reference-count":43,"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>Datatype-generic programming makes it possible to define a  \nconstruction once and apply it to a large class of datatypes.<\/jats:p>\n          <jats:p>It is often used to avoid code duplication in languages that  \nencourage the definition of custom datatypes, in particular  \nstate-of-the-art dependently typed languages where one can have  \nmany variants of the same datatype with different type-level invariants.<\/jats:p>\n          <jats:p>In addition to giving access to familiar programming  \nconstructions for free, datatype-generic programming in the  \ndependently typed setting also allows for the construction of generic proofs.  \nHowever, the current interfaces available for this  \npurpose are needlessly hard to use or are limited in the range of  \ndatatypes they handle.<\/jats:p>\n          <jats:p>In this paper, we describe the design of a library for safe and  \nuser-friendly datatype-generic programming in the Agda  \nlanguage. Generic constructions in our library are regular Agda  \nfunctions over a broad universe of datatypes, yet they can be  \nspecialized to native Agda datatypes with a simple one-liner.  \nFurthermore, we provide building blocks so that library designers can too  \ndefine their own datatype-generic constructions.<\/jats:p>","DOI":"10.1145\/3547644","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"625-649","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Practical generic programming over a universe of native datatypes"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9642-5641","authenticated-orcid":false,"given":"Lucas","family":"Escot","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3862-4073","authenticated-orcid":false,"given":"Jesper","family":"Cockx","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"David Abrahams and Aleksey Gurtovoy. 2004. C++ template metaprogramming: concepts tools and techniques from Boost and beyond. Pearson Education. \t\t\t\t  David Abrahams and Aleksey Gurtovoy. 2004. C++ template metaprogramming: concepts tools and techniques from Boost and beyond. Pearson Education."},{"key":"e_1_2_1_2_1","unstructured":"Agda Development Team. 2021. Agda 2.6.2 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2\/ Accessed [2021\/07\/10] \t\t\t\t  Agda Development Team. 2021. Agda 2.6.2 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2\/ Accessed [2021\/07\/10]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76786-2_4"},{"key":"e_1_2_1_4_1","unstructured":"Stevan Andjelkovic. 2011. A family of universes for generic programming. Master\u2019s thesis. https:\/\/publications.lib.chalmers.se\/records\/fulltext\/146810.pdf \t\t\t\t  Stevan Andjelkovic. 2011. A family of universes for generic programming. Master\u2019s thesis. https:\/\/publications.lib.chalmers.se\/records\/fulltext\/146810.pdf"},{"key":"e_1_2_1_5_1","first-page":"265","article-title":"Universes for Generic Programs and Proofs in Dependent Type Theory","volume":"10","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke , Peter Dybjer , and Patrik Jansson . 2003 . Universes for Generic Programs and Proofs in Dependent Type Theory . Nord. J. Comput. , 10 , 4 (2003), 265 \u2013 289 . Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput., 10, 4 (2003), 265\u2013289.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863592"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001556"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681800014X"},{"key":"e_1_2_1_13_1","unstructured":"Pierre-Evariste Dagand and Conor McBride. 2012. Elaborating Inductive Definitions. \t\t\t\t  Pierre-Evariste Dagand and Conor McBride. 2012. Elaborating Inductive Definitions."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.15760\/etd.5531"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502409.2502414"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633630"},{"key":"e_1_2_1_17_1","volume-title":"4th International Conference, TLCA 99, L Aquila, Italy, April 7-9, 1999, Proceedings, Jean-Yves Girard (Ed.) (Lecture Notes in Computer Science","volume":"146","author":"Dybjer Peter","year":"1999","unstructured":"Peter Dybjer and Anton Setzer . 1999 . A Finite Axiomatization of Inductive-Recursive Definitions. In Typed Lambda Calculi and Applications , 4th International Conference, TLCA 99, L Aquila, Italy, April 7-9, 1999, Proceedings, Jean-Yves Girard (Ed.) (Lecture Notes in Computer Science , Vol. 1581). Springer, 129\u2013 146 . isbn:3-540-65763-0 http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/1581\/15810129.htm Peter Dybjer and Anton Setzer. 1999. A Finite Axiomatization of Inductive-Recursive Definitions. In Typed Lambda Calculi and Applications, 4th International Conference, TLCA 99, L Aquila, Italy, April 7-9, 1999, Proceedings, Jean-Yves Girard (Ed.) (Lecture Notes in Computer Science, Vol. 1581). Springer, 129\u2013146. isbn:3-540-65763-0 http:\/\/link.springer.de\/link\/service\/series\/0558\/bibs\/1581\/15810129.htm"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_2_1_19_1","unstructured":"effectfully. 2016. Deriving eliminators of described data types. http:\/\/effectfully.blogspot.com\/2016\/06\/deriving-eliminators-of-described-data.html \t\t\t\t  effectfully. 2016. Deriving eliminators of described data types. http:\/\/effectfully.blogspot.com\/2016\/06\/deriving-eliminators-of-described-data.html"},{"key":"e_1_2_1_20_1","unstructured":"effectfully. 2016. Descriptions. http:\/\/effectfully.blogspot.com\/2016\/04\/descriptions.html \t\t\t\t  effectfully. 2016. Descriptions. http:\/\/effectfully.blogspot.com\/2016\/04\/descriptions.html"},{"key":"e_1_2_1_21_1","unstructured":"effectfully. 2016. Emulating cumulativity in Agda. http:\/\/effectfully.blogspot.com\/2016\/07\/cumu.html \t\t\t\t  effectfully. 2016. Emulating cumulativity in Agda. http:\/\/effectfully.blogspot.com\/2016\/07\/cumu.html"},{"key":"e_1_2_1_22_1","unstructured":"effectfully. 2020. Generic. https:\/\/github.com\/effectfully\/Generic \t\t\t\t  effectfully. 2020. Generic. https:\/\/github.com\/effectfully\/Generic"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6767057"},{"key":"e_1_2_1_24_1","volume-title":"Inductive-inductive definitions. Ph. D. Dissertation","author":"Forsberg Fredrik Nordvall","unstructured":"Fredrik Nordvall Forsberg . 2013. Inductive-inductive definitions. Ph. D. Dissertation . Swansea University, UK. https:\/\/cronfa.swan.ac.uk\/Record\/cronfa43083 British Library , EThOS Fredrik Nordvall Forsberg. 2013. Inductive-inductive definitions. Ph. D. Dissertation. Swansea University, UK. https:\/\/cronfa.swan.ac.uk\/Record\/cronfa43083 British Library, EThOS"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_35"},{"key":"e_1_2_1_26_1","volume-title":"Generic Haskell: Practice and Theory. In Generic Programming - Advanced Lectures","author":"Hinze Ralf","year":"2003","unstructured":"Ralf Hinze and Johan Jeuring . 2003 . Generic Haskell: Practice and Theory. In Generic Programming - Advanced Lectures , Roland Carl Backhouse and Jeremy Gibbons (Eds .) (Lecture Notes in Computer Science, Vol. 2793). Springer, 1\u2013 56 . isbn:3-540-20194-7 http:\/\/springerlink.metapress.com\/openurl.asp?genre=article&amp;issn=0302-9743&amp;volume=2793&amp;spage=1 Ralf Hinze and Johan Jeuring. 2003. Generic Haskell: Practice and Theory. In Generic Programming - Advanced Lectures, Roland Carl Backhouse and Jeremy Gibbons (Eds.) (Lecture Notes in Computer Science, Vol. 2793). Springer, 1\u201356. isbn:3-540-20194-7 http:\/\/springerlink.metapress.com\/openurl.asp?genre=article&amp;issn=0302-9743&amp;volume=2793&amp;spage=1"},{"key":"e_1_2_1_27_1","unstructured":"LLC Jane Street Group. 2018. ppxlib\u2019s user manual. https:\/\/github.com\/ocaml-ppx\/ppx_deriving \t\t\t\t  LLC Jane Street Group. 2018. ppxlib\u2019s user manual. https:\/\/github.com\/ocaml-ppx\/ppx_deriving"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263763"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00015-1"},{"key":"e_1_2_1_30_1","volume-title":"Haskell 98 language and libraries: the revised report","author":"Jones Simon Peyton","unstructured":"Simon Peyton Jones . 2003. Haskell 98 language and libraries: the revised report . Cambridge University Press . Simon Peyton Jones. 2003. Haskell 98 language and libraries: the revised report. Cambridge University Press."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_2_1_32_1","volume-title":"The Rust Programming Language (Covers Rust","author":"Klabnik Steve","year":"2018","unstructured":"Steve Klabnik and Carol Nichols . 2019. The Rust Programming Language (Covers Rust 2018 ). No Starch Press. Steve Klabnik and Carol Nichols. 2019. The Rust Programming Language (Covers Rust 2018). No Starch Press."},{"key":"e_1_2_1_33_1","volume-title":"Intuitionistic type theory (Studies in proof theory","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f . 1984. Intuitionistic type theory (Studies in proof theory , Vol. 1). Bibliopolis. isbn:978-88-7088-228- 5 Per Martin-L\u00f6f. 1984. Intuitionistic type theory (Studies in proof theory, Vol. 1). Bibliopolis. isbn:978-88-7088-228-5"},{"key":"e_1_2_1_34_1","unstructured":"Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs Paul Callaghan Zhaohui Luo James McKinna Robert Pollack and Robert Pollack (Eds.). \t\t\t\t  Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs Paul Callaghan Zhaohui Luo James McKinna Robert Pollack and Robert Pollack (Eds.)."},{"key":"e_1_2_1_35_1","unstructured":"Conor McBride. 2013. Dependently typed metaprogramming (in Agda). Lecture Notes. \t\t\t\t  Conor McBride. 2013. Dependently typed metaprogramming (in Agda). Lecture Notes."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_12"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"e_1_2_1_38_1","volume-title":"Constructing Universes for Generic Programming. Ph. D. Dissertation","author":"Morris Peter W. J.","year":"1940","unstructured":"Peter W. J. Morris . 2007. Constructing Universes for Generic Programming. Ph. D. Dissertation . University of Nottingham, UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.5 1940 5 British Library , EThOS Peter W. J. Morris. 2007. Constructing Universes for Generic Programming. Ph. D. Dissertation. University of Nottingham, UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.519405 British Library, EThOS"},{"key":"e_1_2_1_39_1","volume-title":"Programming in Martin-L\u00f6f\u2019s type theory. 200","author":"Nordstr\u00f6m Bengt","unstructured":"Bengt Nordstr\u00f6m , Kent Petersson , and Jan M Smith . 1990. Programming in Martin-L\u00f6f\u2019s type theory. 200 , Oxford University Press . Bengt Nordstr\u00f6m, Kent Petersson, and Jan M Smith. 1990. Programming in Martin-L\u00f6f\u2019s type theory. 200, Oxford University Press."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_1_41_1","unstructured":"Yorick Sijsling. 2016. Generic programming with ornaments and dependent types. Master\u2019s thesis. \t\t\t\t  Yorick Sijsling. 2016. Generic programming with ornaments and dependent types. Master\u2019s thesis."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707799"},{"key":"e_1_2_1_43_1","volume-title":"A cosmology of datatypes : reusability and dependent types. Ph. D. Dissertation","author":"Dagand Pierre \u00c9variste","unstructured":"Pierre \u00c9variste Dagand . 2013. A cosmology of datatypes : reusability and dependent types. Ph. D. Dissertation . University of Strathclyde, Glasgow, UK . http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.605921 British Library , EThOS Pierre \u00c9variste Dagand. 2013. A cosmology of datatypes : reusability and dependent types. Ph. D. Dissertation. University of Strathclyde, Glasgow, UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.605921 British Library, EThOS"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547644","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547644","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\/3547644"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":43,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547644"],"URL":"https:\/\/doi.org\/10.1145\/3547644","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"}}]}}