{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T17:05:48Z","timestamp":1781715948889,"version":"3.54.5"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["72068931"],"award-info":[{"award-number":["72068931"]}],"id":[{"id":"10.13039\/501100000038","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":[[2026,1,8]]},"abstract":"<jats:p>\n                    This paper proposes a novel language design that combines extensible data types, implemented through row types and row polymorphism, with ad-hoc polymorphism, implemented through type classes. Our design introduces several new constructs and constraints useful for generic operations over rows. We formalize our design in a source calculus \u03bb\n                    <jats:sub>\u03c1<\/jats:sub>\n                    <jats:sup>\u21d2<\/jats:sup>\n                    , which elaborates into a target calculus\n                    <jats:italic toggle=\"yes\">F<\/jats:italic>\n                    <jats:sub>\u03c9<\/jats:sub>\n                    <jats:sup>\u2297\u2295<\/jats:sup>\n                    . We prove that the target calculus is type-safe and that the elaboration is sound, thus establishing the soundness of \u03bb\n                    <jats:sub>\u03c1<\/jats:sub>\n                    <jats:sup>\u21d2<\/jats:sup>\n                    . All proofs are mechanized in the Lean 4 proof assistant. Furthermore, we evaluate our type system using the Brown Benchmark for Table Types, demonstrating the utility of extensible rows with type classes for table types.\n                  <\/jats:p>","DOI":"10.1145\/3776662","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"568-596","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Extensible Data Types with Ad-Hoc Polymorphism"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2253-7193","authenticated-orcid":false,"given":"Matthew","family":"Toohey","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9608-0774","authenticated-orcid":false,"given":"Yanning","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4728-8100","authenticated-orcid":false,"given":"Ara","family":"Jamalzadeh","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5961-1493","authenticated-orcid":false,"given":"Ningning","family":"Xie","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Bernard Berthomieu and Camille Le Monies De Sagazan. 1995. A Calculus of Tagged Types with applications to process languages. Types for Program Analysis 1."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0040253"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806612"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633634"},{"key":"e_1_2_2_7_1","volume-title":"Programming with Polymorphic Variants. In ML workshop. 13","author":"Garrigue Jacques","year":"1998","unstructured":"Jacques Garrigue. 1998. Programming with Polymorphic Variants. In ML workshop. 13."},{"key":"e_1_2_2_8_1","volume-title":"Proofs and types","author":"Girard Jean-Yves","year":"1813","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Cambridge University Press, USA. isbn:0521371813"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99603"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607843"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086"},{"key":"e_1_2_2_13_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."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/640136.604179"},{"key":"e_1_2_2_15_1","unstructured":"Daan Leijen. 2004. First-class labels for extensible rows (technical report uu-cs-2004-51 ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/first-class-labels-for-extensible-rows\/ UTCS Technical Report"},{"key":"e_1_2_2_16_1","volume-title":"Proceedings of the 2005 Symposium on Trends in Functional Programming (TFP\u201905), Tallin, Estonia (proceedings of the 2005 symposium on trends in functional programming (tfp\u201905)","author":"Leijen Daan","year":"2005","unstructured":"Daan Leijen. 2005. Extensible records with scoped labels. In Proceedings of the 2005 Symposium on Trends in Functional Programming (TFP\u201905), Tallin, Estonia (proceedings of the 2005 symposium on trends in functional programming (tfp\u201905), tallin, estonia ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/extensible-records-with-scoped-labels\/"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_2_2_20_1","volume-title":"Lightweight functional session types. Behavioural Types: from Theory to Tools","author":"Lindley Sam","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers, 265\u2013286."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2022\/6\/8"},{"key":"e_1_2_2_22_1","unstructured":"Sarah Mameche. 2019. Strong Normalization of the \u03bb-calculus in Lean."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3609027.3609406"},{"key":"e_1_2_2_27_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","year":"2091","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press. isbn:0262162091","edition":"1"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75284"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143202"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360230"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Lau Skorstengaard. 2019. An Introduction to Logical Relations. arxiv:1907.11133. https:\/\/doi.org\/10.48550\/arXiv.1907.11133 10.48550\/arXiv.1907.11133","DOI":"10.48550\/arXiv.1907.11133"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","unstructured":"Matthew Toohey Yanning Chen Ara Jamalzadeh and Ningning Xie. 2025. Extensible Data Types with Ad-Hoc Polymorphism (Artifact). https:\/\/doi.org\/10.5281\/zenodo.17298033 10.5281\/zenodo.17298033","DOI":"10.5281\/zenodo.17298033"},{"key":"e_1_2_2_35_1","unstructured":"Sam van Kampen. 2025. Abstract Rewriting Formalized in Lean."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_37_1","volume-title":"Proc., IEEE Symposium on Logic in Computer Science. 37\u201344","author":"Wand Mitchell","year":"1987","unstructured":"Mitchell Wand. 1987. Type inference for simple objects. In Proc., IEEE Symposium on Logic in Computer Science. 37\u201344."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90050-C"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Robert Weingart Nicolas Wu and Cristian Cadar. 2024. Total Type Classes: Improving the ergonomics of type-level programming in Haskell.","DOI":"10.1145\/3759164.3759349"},{"key":"e_1_2_2_40_1","unstructured":"Robert Wright Michel Steuwer and Ohad Kammar. 2022. Idris2-Table: evaluating dependently-typed tables with the Brown Benchmark for Table Types."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776662","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T16:18:55Z","timestamp":1781713135000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776662"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776662"],"URL":"https:\/\/doi.org\/10.1145\/3776662","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}