{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:41Z","timestamp":1747173461683,"version":"3.40.5"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"10","license":[{"start":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T00:00:00Z","timestamp":1724716800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Generalized Algebraic Data Types<\/jats:italic> (GADTs) are a syntactic generalization of the usual algebraic data types (ADTs), such as lists, trees, etc. ADTs\u2019 standard initial algebra semantics (IAS) in the category <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000161_inline1.png\"\/><jats:tex-math>\n$\\mathit{Set}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> of sets justify critical syntactic constructs \u2013 such as recursion, pattern matching, and fold \u2013 for programming with them. In this paper, we show that semantics for GADTs that specialize to the IAS for ADTs are necessarily unsatisfactory. First, we show that the functorial nature of such semantics for GADTs in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000161_inline2.png\"\/><jats:tex-math>\n$\\mathit{Set}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> introduces <jats:italic>ghost<\/jats:italic> elements, i.e., elements not writable in syntax. Next, we show how such ghost elements break parametricity. We observe that the situation for GADTs contrasts dramatically with that for ADTs, whose IAS coincides with the parametric model constructed via their Church encodings in System F. Our analysis reveals that the fundamental obstacle to giving a functorial IAS for GADTs is the inherently partial nature of their map functions. We show that this obstacle cannot be overcome by replacing <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000161_inline3.png\"\/><jats:tex-math>\n$\\mathit{Set}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> with other categories that account for this partiality.<\/jats:p>","DOI":"10.1017\/s0960129524000161","type":"journal-article","created":{"date-parts":[[2024,8,27]],"date-time":"2024-08-27T11:19:56Z","timestamp":1724757596000},"page":"1079-1102","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["GADTs are not (Even partial) functors"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3990-726X","authenticated-orcid":false,"given":"Pierre","family":"Cagne","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5983-6230","authenticated-orcid":false,"given":"Enrico","family":"Ghiorzi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8075-3904","authenticated-orcid":false,"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,8,27]]},"reference":[{"key":"S0960129524000161_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90023-0"},{"key":"S0960129524000161_ref47","unstructured":"Vytiniotis, D. and Weirich, S. (2006). Parametricity and GADTs. Available at https:\/\/www.cis.upenn.edu\/~sweirich\/talks\/param-gadt.pdf."},{"key":"S0960129524000161_ref25","doi-asserted-by":"crossref","unstructured":"Johann, P. , Ghiorzi, E. and Jeffries, D. (2021). Parametricity for primitive nested types. In: Foundations of Software Science and Computation Structures: 24th International Conference, FOSSACS 2021, Springer-Verlag. 324\u2013343.","DOI":"10.1007\/978-3-030-71995-1_17"},{"key":"S0960129524000161_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(02)00102-5"},{"key":"S0960129524000161_ref15","article-title":"The Church-Scott representation of inductive and coinductive data","author":"Geuvers","year":"2014","journal-title":"Unpublished"},{"key":"S0960129524000161_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-349-91518-7_12"},{"key":"S0960129524000161_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"volume-title":"Categories for the Working Mathematician","year":"1971","author":"MacLane","key":"S0960129524000161_ref29"},{"key":"S0960129524000161_ref33","unstructured":"Minsky, Y. (2015). Why GADTs matter for performance. Available at https:\/\/blog.janestreet.com\/why-gadts-matter-for-performance\/."},{"key":"S0960129524000161_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_7"},{"key":"S0960129524000161_ref9","first-page":"111","article-title":"Bicategories of partial maps","volume":"28","author":"Carboni","year":"1987","journal-title":"Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques"},{"key":"S0960129524000161_ref36","unstructured":"Norell, U. (2022). Russell\u2019s paradox in agda. Available at https:\/\/github.com\/agda\/agda\/blob\/master\/test\/Succeed\/Russell.agda."},{"key":"S0960129524000161_ref38","unstructured":"Penner, C. (2020). Simpler and safer API design using GADTs. Available at https:\/\/chrispenner.ca\/posts\/gadt-design."},{"key":"S0960129524000161_ref2","first-page":"340","volume-title":"Principles of Programming Languages","volume":"44","author":"Ahmed","year":"2009"},{"key":"S0960129524000161_ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022982420888"},{"key":"S0960129524000161_ref39","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S. L. , Vytiniotis, D. , Washburn, G. and Weirich, S. (2006). Simple unification-based type inference for GADTs. In: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, ICFP \u201906, Association for Computing Machinery, 50\u201361.","DOI":"10.1145\/1160074.1159811"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S0960129524000161_ref40"},{"key":"S0960129524000161_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111058"},{"key":"S0960129524000161_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2036918.2036927"},{"key":"S0960129524000161_ref42","first-page":"513","article-title":"Types, abstraction, and parametric polymorphism","volume":"83","author":"Reynolds","year":"1983","journal-title":"Information Processing"},{"key":"S0960129524000161_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328475"},{"key":"S0960129524000161_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4962-7"},{"key":"S0960129524000161_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00382-0"},{"key":"S0960129524000161_ref27","doi-asserted-by":"crossref","unstructured":"Johann, P. and Polonsky, A. (2020). Deep induction: Induction rules for (truly) nested types. In: Foundations of Software Science and Computation Structures: 23rd International Conference, FOSSACS 2020, Springer-Verlag. 339\u2013358.","DOI":"10.1007\/978-3-030-45231-5_18"},{"key":"S0960129524000161_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30175-2_8"},{"key":"S0960129524000161_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535852"},{"key":"S0960129524000161_ref10","unstructured":"Cheney, J. and Hinze, R. (2003). First-class phantom types , CUCIS TR2003-1901.Cornell University."},{"key":"S0960129524000161_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596599"},{"key":"S0960129524000161_ref26","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785657"},{"key":"S0960129524000161_ref46","first-page":"106","volume-title":"Workshop on Logical Frameworks and Meta-languages","author":"Sheard","year":"2004"},{"key":"S0960129524000161_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"S0960129524000161_ref19","first-page":"151","volume-title":". In: IV Higher Order Workshop, Banff 1990, Workshops in Computing","author":"Jay","year":"1991"},{"key":"S0960129524000161_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"S0960129524000161_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_16"},{"key":"S0960129524000161_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"S0960129524000161_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"S0960129524000161_ref48","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000079"},{"key":"S0960129524000161_ref5","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"103","author":"Barendregt","year":"1984"},{"key":"S0960129524000161_ref35","unstructured":"nLab, authors (2019). Transfinite construction of free algebras. Available at http:\/\/ncatlab.org\/nlab\/show\/transfinite+construction+of+free+algebras."},{"key":"S0960129524000161_ref32","unstructured":"McBride, C. (1999). Dependently typed programs and their proofs, PhD thesis, University of Edinburgh."},{"key":"S0960129524000161_ref43","unstructured":"Riehl, E. (2016). Category theory in context. Dover.."},{"key":"S0960129524000161_ref34","doi-asserted-by":"crossref","unstructured":"Morris, P. and Altenkirch, T. (2009). Indexed containers. In: 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009, 277\u2013285.","DOI":"10.1109\/LICS.2009.33"},{"key":"S0960129524000161_ref3","unstructured":"Atkey, R. (2012). Relational Parametricity for Higher Kinds. In: C\u00e9gielski, P. and Durand, A. , Leibniz International Proceedings in Informatics (LIPIcs), Computer Science Logic (CSL\u201912) - 26th International Workshop\/21st Annual Conference of the EACSL, Dagstuhl, Germany, vol. 16, 46\u201361, Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik."},{"key":"S0960129524000161_ref24","doi-asserted-by":"crossref","unstructured":"Johann, P. and Ghiorzi, E. (2022). (Deep) induction for GADTs. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, Association for Computing Machinery. 324\u2013337.","DOI":"10.1145\/3497775.3503680"},{"key":"S0960129524000161_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746330"},{"key":"S0960129524000161_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90034-X"},{"key":"S0960129524000161_ref49","doi-asserted-by":"crossref","unstructured":"Wadler, P. (1989). Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA, Association for Computing Machinery, vol. 89, 347\u2013359.","DOI":"10.1145\/99370.99404"},{"key":"S0960129524000161_ref30","article-title":"GADTs for the OCaml masses","author":"Mandelbaum","year":"2009","journal-title":"Unpublished"},{"key":"S0960129524000161_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(86)90010-9"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129524000161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T08:44:20Z","timestamp":1740991460000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129524000161\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,27]]},"references-count":49,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2024,11]]}},"alternative-id":["S0960129524000161"],"URL":"https:\/\/doi.org\/10.1017\/s0960129524000161","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2024,8,27]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}