{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T08:39:04Z","timestamp":1787560744318,"version":"build-2736575974"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"HKRGC","award":["17209821"],"award-info":[{"award-number":["17209821"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"\n Programming language mechanisms with a type-directed semantics are nowadays common and widely used. Such mechanisms include\n gradual typing, type classes, implicits<\/jats:italic>\n and intersection types with a\n merge operator<\/jats:italic>\n . While sharing common challenges in their design and having complementary strengths, type-directed mechanisms have been mostly independently studied.\n <\/jats:p>\n \n This paper studies a new calculus, called\n \n \n \n \u03bb<\/mml:mtext>\n \n M<\/mml:mtext>\n \u2605<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , which combines two type-directed mechanisms: gradual typing and a merge operator based on intersection types. Gradual typing enables a smooth transition between dynamically and statically typed code, and is available in languages such as TypeScript or Flow. The merge operator generalizes record concatenation to allow merges of values of any two types. Recent work has shown that the merge operator enables modelling expressive OOP features like\n first-class traits\/classes<\/jats:italic>\n and\n dynamic inheritance<\/jats:italic>\n with static type-checking. These features are not found in mainstream statically typed OOP languages, but they can be found in dynamically or gradually typed languages such as JavaScript or TypeScript. In\n \n \n \n \u03bb<\/mml:mtext>\n \n M<\/mml:mtext>\n \u2605<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n , by exploiting the complementary strengths of gradual typing and the merge operator, we obtain a foundation for modelling gradually typed languages with both first-class classes and dynamic inheritance. We study a static variant of\n \n \n \n \u03bb<\/mml:mtext>\n \n M<\/mml:mtext>\n \u2605<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n (called\n \n \n \n \u03bb<\/mml:mtext>\n M<\/mml:mtext>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n ); prove the type-soundness of\n \n \n \n \u03bb<\/mml:mtext>\n \n M<\/mml:mtext>\n \u2605<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n ; show that\n \n \n \n \u03bb<\/mml:mtext>\n \n M<\/mml:mtext>\n \u2605<\/mml:mo>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n can encode gradual rows and all well-typed terms in the\n \n \n \n \n \n GTFL<\/mml:mtext>\n <\/mml:mrow>\n \u2272<\/mml:mi>\n <\/mml:msub>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:inline-formula>\n typing criteria. The dynamic gradual guarantee (DGG) is challenging due to the possibility of ambiguity errors. We establish a variant of the DGG using a semantic notion of precision based on a step-indexed logical relation.\n <\/jats:p>","DOI":"10.1145\/3689734","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"648-676","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Merging Gradual Typing"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3968-6201","authenticated-orcid":false,"given":"Wenjia","family":"Ye","sequence":"first","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1846-7210","authenticated-orcid":false,"given":"Bruno C. d. S.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5315-0198","authenticated-orcid":false,"given":"Mat\u00edas","family":"Toro","sequence":"additional","affiliation":[{"name":"University of Chile, Santiago, Chile"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","unstructured":"Mart\u00edn Abadi and Luca Cardelli. 1996. A Theory of Objects. In Monographs in Computer Science.","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Jo\u00e3o Alpuim Bruno C. d. S. Oliveira and Zhiyuan Shi. 2017. Disjoint Polymorphism. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_1 10.1007\/978-3-662-54434-1_1","DOI":"10.1007\/978-3-662-54434-1_1"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434342"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Xuan Bi and Bruno C. d. S. Oliveira. 2018. Typed First-Class Traits. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2018.9 10.4230\/LIPIcs.ECOOP.2018.9","DOI":"10.4230\/LIPIcs.ECOOP.2018.9"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/97946.97982"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2829"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000049"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"William R. Cook and Jens Palsberg. 1989. A denotational semantics of inheritance and its correctness. In Object-Oriented Programming: Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/74878.74922 10.1145\/74878.74922","DOI":"10.1145\/74878.74922"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398856.2364534"},{"issue":"549","key":"e_1_3_1_16_1","article-title":"gbeta-a language with virtual attributes, Block Structure, and Propagating, Dynamic Inheritance","volume":"29","author":"Ernst Erik","year":"2000","unstructured":"Erik Ernst. 2000. gbeta-a language with virtual attributes, Block Structure, and Propagating, Dynamic Inheritance. DAIMI Report Series 29, 549 (2000).","journal-title":"DAIMI Report Series"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Matthew Flatt Robert Bruce Findler and Matthias Felleisen. 2006. Scheme with Classes Mixins and Traits. In APLAS. https:\/\/doi.org\/10.1007\/11924661_17 10.1007\/11924661_17","DOI":"10.1007\/11924661_17"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837670"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3589806.3600034"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000217"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.26"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000186"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.149"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314627"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Joseph Lee Jonathan Aldrich Troy Shaw and Alex Potanin. 2015. A Theory of Tagged Objects. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.174 10.4230\/LIPIcs.ECOOP.2015.174","DOI":"10.4230\/LIPIcs.ECOOP.2015.174"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133880"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485504"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371114"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Bruno C.d.S. Oliveira Adriaan Moors and Martin Odersky. 2010. Type Classes as Objects and Implicits. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA \u201910). 341\u2013360. https:\/\/doi.org\/10.1145\/1932682.1869489 10.1145\/1932682.1869489","DOI":"10.1145\/1932682.1869489"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951945"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"John C Reynolds. 1997. Design of the programming language Forsythe. In ALGOL-like languages. 173\u2013233.","DOI":"10.1007\/978-1-4612-4118-8_9"},{"key":"e_1_3_1_33_1","unstructured":"Taro Sekiyama and Atsushi Igarashi. 2019. Gradual Typing for Extensibility by Rows. ArXiv abs\/1910.08480 (2019)."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737968"},{"key":"e_1_3_1_35_1","first-page":"81","article-title":"Gradual typing for functional languages","volume":"6","author":"Siek Jeremy G.","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Vol. 6. 81\u201392.","journal-title":"Scheme and Functional Programming Workshop"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Jeremy G. Siek and Walid Taha. 2007. Gradual Typing for Objects. In ECOOP. https:\/\/doi.org\/10.1007\/978-3-540-73589-2_2 10.1007\/978-3-540-73589-2_2","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.274"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1570506.1570511"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837630"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384674"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage migration: from scripts to programs. https:\/\/doi.org\/10.1145\/1176617.1176755 10.1145\/1176617.1176755","DOI":"10.1145\/1176617.1176755"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102496"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"P. Wadler and S. Blott. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201989). https:\/\/doi.org\/10.1145\/75277.75283 10.1145\/75277.75283","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_3_1_45_1","unstructured":"Mitchell Wand. 1989. Type Inference for Record Concatenation and Multiple Inheritance. In Symposium on Logic in Computer Science (LICS)."},{"key":"e_1_3_1_46_1","unstructured":"Mitchell Wand. 1994. Type inference for objects with instance variables and inheritance."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310339"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_6"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.12"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Wenjia Ye Bruno C. d. S. Oliveira and Mat\u00edas Toro. 2024. Merging Gradual Typing (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13378311 10.5281\/zenodo.13378311","DOI":"10.5281\/zenodo.13378311"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460228"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689734","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689734","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:06:20Z","timestamp":1770195980000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689734"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":50,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689734"],"URL":"https:\/\/doi.org\/10.1145\/3689734","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-04","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}