{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:17:20Z","timestamp":1760044640684,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["MR\/T043830\/1"],"award-info":[{"award-number":["MR\/T043830\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"name":"European Research Council","award":["682315"],"award-info":[{"award-number":["682315"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature.<\/jats:p>\n          <jats:p>In this paper, we systematically study the relative expressive power of structural subtyping and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subtyping for variant and record types. We base our study on various Church-style \u03bb-calculi extended with records and variants, different forms of structural subtyping, and row and presence polymorphism.<\/jats:p>\n          <jats:p>We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subtyping cannot be encoded via polymorphism, but we show that several restricted forms of subtyping can be encoded via particular forms of polymorphism.<\/jats:p>","DOI":"10.1145\/3622836","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1093-1121","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Structural Subtyping as Parametric Polymorphism"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6589-3821","authenticated-orcid":false,"given":"Wenhao","family":"Tang","sequence":"first","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4730-9315","authenticated-orcid":false,"given":"Daniel","family":"Hillerstr\u00f6m","sequence":"additional","affiliation":[{"name":"Huawei Zurich Research Center, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6745-2560","authenticated-orcid":false,"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"Techinsche Universit\u00e4t Berlin, Berlin, Germany \/ University of Edinburgh, Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9927-7875","authenticated-orcid":false,"given":"Ornela","family":"Dardha","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6966-4037","authenticated-orcid":false,"given":"Rongxiao","family":"Fu","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1360-4714","authenticated-orcid":false,"given":"Sam","family":"Lindley","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_1"},{"volume-title":"FRG)","author":"Birtwistle Graham M.","key":"e_1_2_2_2_1","unstructured":"Graham M. Birtwistle , Ole-Johan Dahl , Bjorn Myhrhaug , and Kristen Nygaard . 1979. Simula Begin . Studentlitteratur ( Lund , Sweden) , Bratt Institut fuer nues Lernen (Goch , FRG) , Charwell-Bratt Ltd (Kent , England ). Graham M. Birtwistle, Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. 1979. Simula Begin. Studentlitteratur (Lund, Sweden), Bratt Institut fuer nues Lernen (Goch, FRG), Charwell-Bratt Ltd (Kent, England)."},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Matthias Blume Umut A. Acar and Wonseok Chae. 2006. Extensible programming with first-class cases. In ICFP. ACM 239\u2013250. \t\t\t\t  Matthias Blume Umut A. Acar and Wonseok Chae. 2006. Extensible programming with first-class cases. In ICFP. ACM 239\u2013250.","DOI":"10.1145\/1160074.1159836"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91590"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_2"},{"volume-title":"Structural Subtyping and the Notion of Power Type","author":"Cardelli Luca","key":"e_1_2_2_7_1","unstructured":"Luca Cardelli . 1988. Structural Subtyping and the Notion of Power Type . In POPL. ACM Press , 70\u201379. Luca Cardelli. 1988. Structural Subtyping and the Notion of Power Type. In POPL. ACM Press, 70\u201379."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000049"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951945"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"volume-title":"Computer Laboratory","author":"Dolan Stephen","key":"e_1_2_2_14_1","unstructured":"Stephen Dolan . 2016. Algebraic Subtyping . Ph. D. Dissertation . Computer Laboratory . University of Cambridge , United Kingdom . Stephen Dolan. 2016. Algebraic Subtyping. Ph. D. Dissertation. Computer Laboratory. University of Cambridge, United Kingdom."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In POPL. ACM 60\u201372. \t\t\t\t  Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In POPL. ACM 60\u201372.","DOI":"10.1145\/3093333.3009882"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000270"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386003"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90036-W"},{"volume-title":"variants and qualified types. Ph. D. Dissertation","author":"Gaster Benedict R","key":"e_1_2_2_19_1","unstructured":"Benedict R Gaster . 1998. Records , variants and qualified types. Ph. D. Dissertation . University of Nottingham. Benedict R Gaster. 1998. Records, variants and qualified types. Ph. D. Dissertation. University of Nottingham."},{"key":"e_1_2_2_21_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris 7. France. \t\t\t\t  Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Ph. D. Dissertation. Universit\u00e9 Paris 7. France."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1184\/R1\/6605507.v1"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe@ICFP. ACM 15\u201327. \t\t\t\t  Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In TyDe@ICFP. ACM 15\u201327.","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_2_24_1","volume-title":"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) , Tallinn, Estonia. https:\/\/www.microsoft.com\/en-us\/research\/publication\/extensible-records-with-scoped-labels\/ Daan Leijen. 2005. Extensible records with scoped labels. In Proceedings of the 2005 Symposium on Trends in Functional Programming (TFP\u201905), Tallinn, Estonia. https:\/\/www.microsoft.com\/en-us\/research\/publication\/extensible-records-with-scoped-labels\/"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_26_1","volume-title":"Proc. ACM Program. Lang., 3, POPL","author":"Garrett Morris J.","year":"2019","unstructured":"J. Garrett Morris and James McKinna . 2019 . Abstracting extensible data types: or, rows by any other name . Proc. ACM Program. Lang., 3, POPL (2019), 12:1\u201312:28. J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name. Proc. ACM Program. Lang., 3, POPL (2019), 12:1\u201312:28."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C.","key":"e_1_2_2_28_1","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press . isbn:978-0-262-16209-8 Benjamin C. Pierce. 2002. Types and programming languages. MIT Press. isbn:978-0-262-16209-8"},{"key":"e_1_2_2_29_1","unstructured":"Fran\u00e7ois Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. INRIA. https:\/\/hal.inria.fr\/inria-00073205 \t\t\t\t  Fran\u00e7ois Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. INRIA. https:\/\/hal.inria.fr\/inria-00073205"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2963"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1104.003.0016"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75284"},{"volume-title":"Type Inference for Records in Natural Extension of ML","author":"R\u00e9my Didier","key":"e_1_2_2_33_1","unstructured":"Didier R\u00e9my . 1994. Type Inference for Records in Natural Extension of ML . MIT Press , Cambridge, MA, USA . 67\u201395. Didier R\u00e9my. 1994. Type Inference for Records in Natural Extension of ML. MIT Press, Cambridge, MA, USA. 67\u201395."},{"key":"e_1_2_2_34_1","volume-title":"Symposium on Programming (LNCS","volume":"423","author":"Reynolds John C.","year":"1974","unstructured":"John C. Reynolds . 1974 . Towards a theory of type structure . In Symposium on Programming (LNCS , Vol. 19). Springer, 408\u2013 423 . John C. Reynolds. 1974. Towards a theory of type structure. In Symposium on Programming (LNCS, Vol. 19). Springer, 408\u2013423."},{"key":"e_1_2_2_35_1","volume-title":"Semantics-Directed Compiler Generation (Lecture Notes in Computer Science","volume":"258","author":"Reynolds John C.","year":"1980","unstructured":"John C. Reynolds . 1980 . Using category theory to design implicit conversions and generic operators . In Semantics-Directed Compiler Generation (Lecture Notes in Computer Science , Vol. 94). Springer, 211\u2013 258 . John C. Reynolds. 1980. Using category theory to design implicit conversions and generic operators. In Semantics-Directed Compiler Generation (Lecture Notes in Computer Science, Vol. 94). Springer, 211\u2013258."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_52"},{"volume-title":"Complete Type Inference for Simple Objects","author":"Wand Mitchell","key":"e_1_2_2_37_1","unstructured":"Mitchell Wand . 1987. Complete Type Inference for Simple Objects . In LICS. IEEE Computer Society , 37\u201344. Mitchell Wand. 1987. Complete Type Inference for Simple Objects. In LICS. IEEE Computer Society, 37\u201344."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.27"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571224"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622836","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622836","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622836"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":38,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622836"],"URL":"https:\/\/doi.org\/10.1145\/3622836","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}