{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T15:05:34Z","timestamp":1768835134641,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1910522, CCF-1816837, CCF-1453796"],"award-info":[{"award-number":["CCF-1910522, CCF-1816837, CCF-1453796"]}],"id":[{"id":"10.13039\/100000001","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":[[2020,1]]},"abstract":"<jats:p>Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.<\/jats:p>\n          <jats:p>We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.<\/jats:p>","DOI":"10.1145\/3371114","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Graduality and parametricity: together again for the first time"],"prefix":"10.1145","volume":"4","author":[{"given":"Max S.","family":"New","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dustin","family":"Jamner","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"State-Dependent Representation Independence. In ACM Symposium on Principles of Programming Languages (POPL)","author":"Ahmed Amal","year":"2009"},{"key":"e_1_2_2_2_1","volume-title":"Blame for All. In ACM Symposium on Principles of Programming Languages (POPL)","author":"Ahmed Amal","year":"2011"},{"key":"e_1_2_2_3_1","volume-title":"With and Without Types. In International Conference on Functional Programming (ICFP)","author":"Ahmed Amal","year":"2017"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628149"},{"key":"e_1_2_2_5_1","volume-title":"21st Workshop on Foundations of Object-Oriented Languages.","author":"Boyland John","year":"2014"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_2_7_1","volume-title":"Gradual Information Flow Typing. In Workshop on Script-to-Program Evolution (STOP).","author":"Disney Tim","year":"2011"},{"key":"e_1_2_2_9_1","volume-title":"On the expressive power of programming languages. ESOP\u201990","author":"Felleisen Matthias","year":"1990"},{"key":"e_1_2_2_10_1","volume-title":"Gradual Security Typing with References","author":"Fennell Luminous"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs (POPL \u201915).  Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs (POPL \u201915).","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_12_1","volume-title":"Abstracting Gradual Typing. In ACM Symposium on Principles of Programming Languages (POPL).","author":"Garcia Ronald","year":"2016"},{"key":"e_1_2_2_13_1","volume-title":"Gradual Session Types. In International Conference on Functional Programming (ICFP).","author":"Igarashi Atsushi","year":"2017"},{"key":"e_1_2_2_14_1","volume-title":"On Polymorphic Gradual Typing. In International Conference on Functional Programming (ICFP)","author":"Igarashi Yuu","year":"2017"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048114"},{"key":"e_1_2_2_16_1","volume-title":"Gradual Refinement Types. In ACM Symposium on Principles of Programming Languages (POPL).","author":"Nico"},{"key":"e_1_2_2_17_1","volume-title":"A Functional\/Imperative Synthesis","author":"Levy Paul Blain"},{"key":"e_1_2_2_18_1","volume-title":"7th International Conference","author":"Ma QingMing"},{"key":"e_1_2_2_19_1","volume-title":"ACM Symposium on Principles of Programming Languages (POPL)","author":"John"},{"key":"e_1_2_2_20_1","volume-title":"Non-Parametric Parametricity. In International Conference on Functional Programming (ICFP). 135\u2013148","author":"Neis Georg","year":"2009"},{"key":"e_1_2_2_21_1","volume-title":"International Conference on Functional Programming (ICFP), St","author":"Max"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Max S. New Dustin Jamner and Amal Ahmed. 2020. Technical Appendix to Graduality and Parametricity: Together Again for the First Time. http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/gradparam- tr.pdf  Max S. New Dustin Jamner and Amal Ahmed. 2020. Technical Appendix to Graduality and Parametricity: Together Again for the First Time. http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/gradparam- tr.pdf","DOI":"10.1145\/3371114"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Max S. New Daniel R. Licata and Amal Ahmed. 2019. Gradual Type Theory (POPL \u201919).  Max S. New Daniel R. Licata and Amal Ahmed. 2019. Gradual Type Theory (POPL \u201919).","DOI":"10.1145\/3290328"},{"key":"e_1_2_2_24_1","volume-title":"A logic for parametric polymorphism. Typed Lambda Calculi and Applications","author":"Plotkin Gordon","year":"1993"},{"key":"e_1_2_2_25_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress","author":"Reynolds John C.","year":"1983"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_2_27_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Sergey Ilya"},{"key":"e_1_2_2_28_1","volume-title":"1st Summit on Advances in Programming Languages.","author":"Siek Jeremy"},{"key":"e_1_2_2_29_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81\u201392","author":"Jeremy"},{"key":"e_1_2_2_30_1","volume-title":"Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP).","author":"Jeremy"},{"key":"e_1_2_2_31_1","volume-title":"ACM Symposium on Principles of Programming Languages (POPL)","author":"Sumii Eijiro"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Asumu Takikawa T. Stephen Strickland Christos Dimoulas Sam Tobin-Hochstadt and Matthias Felleisen. 2012. Gradual typing for first-class classes (ACM Symposium on Object Oriented Programming: Systems Languages and Applications (OOPSLA)).  Asumu Takikawa T. Stephen Strickland Christos Dimoulas Sam Tobin-Hochstadt and Matthias Felleisen. 2012. Gradual typing for first-class classes (ACM Symposium on Object Oriented Programming: Systems Languages and Applications (OOPSLA)).","DOI":"10.1145\/2384616.2384674"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_2_2_34_1","volume-title":"The Design and Implementation of Typed Scheme. In ACM Symposium on Principles of Programming Languages (POPL)","author":"Tobin-Hochstadt Sam","year":"2008"},{"key":"e_1_2_2_35_1","unstructured":"Sam Tobin-Hochstadt Vincent St-Amour Eric Dobson and Asumu Takikawa. [n. d.]. Typed Racket Reference. https: \/\/docs.racket- lang.org\/ts- reference\/Typed_Units.html Accessed: 2019-10-30.  Sam Tobin-Hochstadt Vincent St-Amour Eric Dobson and Asumu Takikawa. [n. d.]. Typed Racket Reference. https: \/\/docs.racket- lang.org\/ts- reference\/Typed_Units.html Accessed: 2019-10-30."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229061"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"e_1_2_2_38_1","volume-title":"Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP\u201911)","author":"Wolff Roger","year":"2011"},{"key":"e_1_2_2_39_1","volume-title":"d. S. Oliveira","author":"Xie Ningning","year":"2018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371114","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371114","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371114","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371114"],"URL":"https:\/\/doi.org\/10.1145\/3371114","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}