{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:11:50Z","timestamp":1760033510102,"version":"build-2065373602"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"MathInGreaterParis Fellowship Programme","award":["H2020-MSCA-COFUND2020"],"award-info":[{"award-number":["H2020-MSCA-COFUND2020"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n            The merge operator is a powerful construct in programming languages, enabling flexible composition of various components such as functions, records, or classes. Unfortunately, its application often leads to ambiguity and non-determinism, especially when dealing with overlapping types. To prevent ambiguity, approaches such as disjoint intersection types have been proposed. However, disjointness imposes strict constraints to ensure determinism, at the cost of limiting expressiveness, particularly for function overloading. This paper introduces a novel concept called\n            <jats:italic toggle=\"yes\">type apartness<\/jats:italic>\n            , which relaxes the strict disjointness constraints, while maintaining type safety and determinism. Type apartness allows some overlap for overloaded functions as long as the calling contexts of those functions can be used to disambiguate upcasts in function calls. By incorporating the notion of guarded subtyping to prevent ambiguity when upcasting, our approach is the first to support\n            <jats:italic toggle=\"yes\">function overloading<\/jats:italic>\n            ,\n            <jats:italic toggle=\"yes\">return type overloading<\/jats:italic>\n            ,\n            <jats:italic toggle=\"yes\">extensible records<\/jats:italic>\n            , and\n            <jats:italic toggle=\"yes\">nested composition<\/jats:italic>\n            in a single calculus while preserving determinism. We formalize our calculi and proofs using Coq and prove their type soundness and determinism. Additionally, we demonstrate how type normalization and type difference provide more convenience and help resolve conflicts, enhancing the flexibility and expressiveness of the merge operator.\n          <\/jats:p>","DOI":"10.1145\/3763057","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"193-219","update-policy":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Liberating Merges via Apartness and Guarded Subtyping"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/orcid.org\/0000-0002-2548-6866","authenticated-orcid":false,"given":"Han","family":"Xu","sequence":"first","affiliation":[{"name":"Princeton University, Princeton, USA"}]},{"ORCID":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/orcid.org\/0000-0002-8496-491X","authenticated-orcid":false,"given":"Xuejing","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"},{"name":"IRIF - Universit\u00e9 Paris Cit\u00e9, Paris, France"}]},{"ORCID":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/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"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/937563.937567"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.22"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/97945.97982"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1033"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676991"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535840"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034788"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/232629.232654"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_17"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.18"},{"key":"e_1_2_1_18_1","volume-title":"Electronic proceedings of FOOL.","author":"Fisher Kathleen","year":"2004","unstructured":"Kathleen Fisher and John Reppy. 2004. A typed calculus of traits. In Electronic proceedings of FOOL. 2004."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268961"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"e_1_2_1_21_1","volume-title":"The 34th European Conference on Object-Oriented Programming (ECOOP","author":"Huang Xuejing","year":"2020","unstructured":"Xuejing Huang and Bruno C. d. S. Oliveira. 2020. A type-directed operational semantics for a calculus with a merge operator. In The 34th European Conference on Object-Oriented Programming (ECOOP 2020."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000186"},{"key":"e_1_2_1_23_1","unstructured":"Daan Leijen. 2004. First-class labels for extensible rows (technical report uu-cs-2004-51 ed.). https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/www.microsoft.com\/en-us\/research\/publication\/first-class-labels-for-extensible-rows\/ UTCS Technical Report"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.1.105"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428274"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951945"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"volume-title":"Preliminary design of the programming language Forsythe","author":"Reynolds John C","key":"e_1_2_1_29_1","unstructured":"John C Reynolds. 1988. Preliminary design of the programming language Forsythe. Carnegie Mellon University."},{"key":"e_1_2_1_30_1","series-title":"Lecture Notes in Computer Science (LNCS)","volume-title":"The coherence of languages with intersection types","author":"Reynolds John C.","unstructured":"John C. Reynolds. 1991. The coherence of languages with intersection types. In Lecture Notes in Computer Science (LNCS). Springer Berlin Heidelberg, 675\u2013700."},{"key":"e_1_2_1_31_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"},{"volume-title":"Theories of programming languages","author":"Reynolds John C","key":"e_1_2_1_32_1","unstructured":"John C Reynolds. 1998. Theories of programming languages. Cambridge University Press."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571211"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_12"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"e_1_2_1_36_1","volume-title":"Dependent Merges and First-Class Environments. In 37th European Conference on Object-Oriented Programming (ECOOP","author":"Tan Jinhao","year":"2023","unstructured":"Jinhao Tan and Bruno C d S Oliveira. 2023. Dependent Merges and First-Class Environments. In 37th European Conference on Object-Oriented Programming (ECOOP 2023)."},{"key":"e_1_2_1_37_1","unstructured":"Philip Wadler. 1998. The expression problem. Java-genericity mailing list."},{"key":"e_1_2_1_38_1","volume-title":"European Symposium on Programming. 1\u201316","author":"Wadler Philip","year":"2009","unstructured":"Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can\u2019t be blamed. In European Symposium on Programming. 1\u201316."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.20"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571224"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16921686"},{"key":"e_1_2_1_42_1","volume-title":"d. S. Oliveira, and Ningning Xie","author":"Xue Xu","year":"2022","unstructured":"Xu Xue, Bruno C. d. S. Oliveira, and Ningning Xie. 2022. Applicative Intersection Types. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer Nature Switzerland, Cham. 155\u2013174. isbn:978-3-031-21037-2"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689782"},{"key":"e_1_2_1_44_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:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/dl.acm.org\/doi\/pdf\/10.1145\/3763057","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:08Z","timestamp":1760031668000},"score":1,"resource":{"primary":{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/dl.acm.org\/doi\/10.1145\/3763057"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":44,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763057"],"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1145\/3763057","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2024-10-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}