{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:55:09Z","timestamp":1790927709254,"version":"4.1.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["FA8655-13-1-3006"],"award-info":[{"award-number":["FA8655-13-1-3006"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We present a novel typed language for extensible data types, generalizing and abstracting existing systems of row types and row polymorphism. Extensible data types are a powerful addition to traditional functional programming languages, capturing ideas from OOP-like record extension and polymorphism to modular compositional interpreters. We introduce row theories, a monoidal generalization of row types, giving a general account of record concatenation and projection (dually, variant injection and branching). We realize them via qualified types, abstracting the interpretation of records and variants over different row theories. Our approach naturally types terms untypable in other systems of extensible data types, while maintaining strong metatheoretic properties, such as coherence and principal types. Evidence for type qualifiers has computational content, determining the implementation of record and variant operations; we demonstrate this in giving a modular translation from our calculus, instantiated with various row theories, to polymorphic \u03bb-calculus.<\/jats:p>","DOI":"10.1145\/3290325","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T08:33:51Z","timestamp":1546590831000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Abstracting extensible data types: or, rows by any other name"],"prefix":"10.1145","volume":"3","author":[{"given":"J. Garrett","family":"Morris","sequence":"first","affiliation":[{"name":"University of Kansas, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633628.2633635"},{"key":"e_1_2_2_2_1","volume-title":"Workshop on types for program analysis","author":"Berthomieu B.","year":"1995","unstructured":"B. Berthomieu and C. le Moni\u00e8s de Sagazan. A calculus of tagged types, with applications to process languages . In Workshop on types for program analysis , Aarhus , 1995 . B. Berthomieu and C. le Moni\u00e8s de Sagazan. A calculus of tagged types, with applications to process languages. In Workshop on types for program analysis , Aarhus, 1995."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159836"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236779"},{"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\/2364527.2364534"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_2_2_8_1","volume-title":"ML Workshop. ACM","author":"Garrigue J.","year":"1998","unstructured":"J. Garrigue . Programming with polymorphic variants . In ML Workshop. ACM , 1998 . J. Garrigue. Programming with polymorphic variants. In ML Workshop. ACM, 1998."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99603"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676989"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926428"},{"key":"e_1_2_2_15_1","volume-title":"Theory and Practice","author":"Jones M. P.","year":"1994","unstructured":"M. P. Jones . Qualified Types : Theory and Practice . Cambridge University Press , 1994 . M. P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, 1994."},{"key":"e_1_2_2_16_1","series-title":"Lecture Notes in Computer Science","first-page":"244","volume-title":"Programming Languages and Systems, 9th European Symposium on Programming, ESOP","author":"Jones M. P.","year":"2000","unstructured":"M. P. Jones . Type classes with functional dependencies. In G. Smolka, editor, Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000 , Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings , volume 1782 of Lecture Notes in Computer Science , pages 230\u2013 244 . Springer, 2000. M. P. Jones. Type classes with functional dependencies. In G. Smolka, editor, Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings , volume 1782 of Lecture Notes in Computer Science , pages 230\u2013244. Springer, 2000."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_2_18_1","volume-title":"The lens package, version 4.16","author":"Kmett E.","year":"2018","unstructured":"E. Kmett . The lens package, version 4.16 , 2018 . E. Kmett. The lens package, version 4.16, 2018."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291892"},{"key":"e_1_2_2_20_1","first-page":"179","article-title":"Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn","volume":"23","author":"Leijen D.","year":"2005","unstructured":"D. Leijen . Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn , Estonia , 23-24 September 2005 . , pages 179 \u2013 194 , 2005. D. Leijen. Extensible records with scoped labels. In Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005. , pages 179\u2013194, 2005.","journal-title":"Estonia"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_2_2_25_1","volume-title":"Behavioural Types: from Theory to Tools","author":"Lindley S.","year":"2017","unstructured":"S. Lindley and J. G. Morris . Lightweight functional session types . In S. Gay and A. Ravara, editors, Behavioural Types: from Theory to Tools . River Publishers , 2017 . S. Lindley and J. G. Morris. Lightweight functional session types. In S. Gay and A. Ravara, editors, Behavioural Types: from Theory to Tools . River Publishers, 2017."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086386"},{"key":"e_1_2_2_28_1","series-title":"CEUR Workshop Proceedings","first-page":"94","volume-title":"Bx@ETAPS","author":"McKinna J.","unstructured":"J. McKinna . Complements witness consistency . In Bx@ETAPS , volume 1571 of CEUR Workshop Proceedings , pages 90\u2013 94 . CEUR-WS.org, 2016. J. McKinna. Complements witness consistency. In Bx@ETAPS, volume 1571 of CEUR Workshop Proceedings, pages 90\u201394. CEUR-WS.org, 2016."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633364"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804320"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804315"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951945"},{"key":"e_1_2_2_34_1","volume-title":"Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming , 1(2)","author":"Pickering M.","year":"2017","unstructured":"M. Pickering , J. Gibbons , and N. Wu . Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming , 1(2) , 2017 . Article 7. M. Pickering, J. Gibbons, and N. Wu. Profunctor Optics: Modular Data Accessors. The Art, Science, and Engineering of Programming , 1(2), 2017. Article 7."},{"key":"e_1_2_2_35_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pottier F.","year":"2005","unstructured":"F. Pottier and D. R\u00e9my . The essence of ML type inference . In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages . The MIT Press , 2005 . F. Pottier and D. R\u00e9my. The essence of ML type inference. In B. C. Pierce, editor, Advanced Topics in Types and Programming Languages . The MIT Press, 2005."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75284"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680300488X"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_39_1","unstructured":"P. Wadler. The expression problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt 1998.  P. Wadler. The expression problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt 1998."},{"key":"e_1_2_2_40_1","first-page":"44","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201987)","author":"Wand M.","year":"1987","unstructured":"M. Wand . Complete type inference for simple objects . In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987) , Ithaca, New York, USA , June 22-25, 1987 , pages 37\u2013 44 . IEEE Computer Society, 1987. M. Wand. Complete type inference for simple objects. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987 , pages 37\u201344. IEEE Computer Society, 1987."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90050-C"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290325","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:02:07Z","timestamp":1750194127000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290325"],"URL":"https:\/\/doi.org\/10.1145\/3290325","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}