{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:42Z","timestamp":1775790702587,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003816","name":"Huawei Technologies","doi-asserted-by":"publisher","award":["TC20230508031"],"award-info":[{"award-number":["TC20230508031"]}],"id":[{"id":"10.13039\/501100003816","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002920","name":"Research Grants Council, University Grants Committee","doi-asserted-by":"publisher","award":["17209821"],"award-info":[{"award-number":["17209821"]}],"id":[{"id":"10.13039\/501100002920","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Modern mainstream programming languages, such as TypeScript, Flow, and Scala, have polymorphic type systems enriched with intersection and union types. These languages implement variants of\n                    <jats:italic toggle=\"yes\">bidirectional higher-rank polymorphic<\/jats:italic>\n                    type inference, which was previously studied mostly in the context of functional programming. However, existing type inference implementations lack solid theoretical foundations when dealing with non-structural subtyping and intersection and union types, which were not studied before.\n                  <\/jats:p>\n                  <jats:p>In this paper, we study bidirectional higher-rank polymorphic type inference with explicit type applications, and intersection and union types and demonstrate that these features have non-trivial interactions. We first present a type system, described by a bidirectional specification, with good theoretical properties and a sound, complete, and decidable algorithm. This is helpful to identify a class of types that can always be inferred. We also explore variants incorporating practical features, such as handling records and inferring a larger class of types, which align better with real-world implementations. Though some variants no longer have a complete algorithm, they still enhance the expressiveness of the type system. To ensure rigor, all results are formalized in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3704907","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2118-2148","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Bidirectional Higher-Rank Polymorphism with Intersection and Union Types"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4443-0753","authenticated-orcid":false,"given":"Shengyi","family":"Jiang","sequence":"first","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8351-2679","authenticated-orcid":false,"given":"Chen","family":"Cui","sequence":"additional","affiliation":[{"name":"University of Hong Kong, Hong Kong, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Jan Bessai Boris D\u00fcdder Andrej Dudenhefner Tzu-Chun Chen and Ugo de\u2019Liguoro. 2014. Typing Classes and Mixins with Intersection Types. In Proceedings Seventh Workshop on Intersection Types and Related Systems ITRS 2014 Vienna Austria 18 July 2014 (EPTCS Vol. 177) Jakob Rehof (Ed.). 79\u201393. https:\/\/doi.org\/10.4204\/EPTCS.177.7 10.4204\/EPTCS.177.7","DOI":"10.4204\/EPTCS.177.7"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_3"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1033"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632882"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055784"},{"key":"e_1_3_2_13_1","unstructured":"Julien Cretin. 2014. Erasable coercions: a unified approach to type systems. (Coercions effa\u00e7ables : une approche unifi\u00e9e des syst\u00e8mes de types). Ph. D. Dissertation. Paris Diderot University France. https:\/\/tel.archives-ouvertes.fr\/tel-00940511"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622871"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2016.19"},{"key":"e_1_3_2_18_1","doi-asserted-by":"crossref","unstructured":"Jana Dunfield. 2009. Greedy Bidirectional Polymorphism. In ML Workshop (ML \u201809). 15\u201326. http:\/\/www.cs.queensu.ca\/~jana\/papers\/poly\/.","DOI":"10.1145\/1596627.1596631"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000270"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"issue":"5","key":"e_1_3_2_21_1","first-page":"38","article-title":"Bidirectional Typing","volume":"54","author":"Dunfield Jana","year":"2021","unstructured":"Jana Dunfield and Neelakantan R. Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54, 5, Article 98 (May 2021), 38 pages.","journal-title":"ACM Comput. Surv."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386003"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995158"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000186"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Shengyi Jiang Chen Cui and Bruno C. d. S. Oliveira. 2024. Bidirectional Higher-Rank Polymorphism with Intersection and Union Types (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13922447 10.5281\/zenodo.13922447","DOI":"10.5281\/zenodo.13922447"},{"key":"e_1_3_2_29_1","first-page":"323","volume-title":"ICALP Workshops 2000, Proceedings of the Satelite Workshops of the 27th International Colloquium on Automata, Languages and Programming, Geneva, Switzerland, July 9-15, 2000","author":"Jim Trevor","year":"2000","unstructured":"Trevor Jim. 2000. A Polar Type System. In ICALP Workshops 2000, Proceedings of the Satelite Workshops of the 27th International Colloquium on Automata, Languages and Programming, Geneva, Switzerland, July 9-15, 2000, Jos\u00e9 D. P. Rolim, Andrei Z. Broder, Andrea Corradini, Roberto Gorrieri, Reiko Heckel, Juraj Hromkovic, Ugo Vaccaro, and J. B. Wells (Eds.). Carleton Scientific, Waterloo, Ontario, Canada, 323\u2013338."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944709"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Daan Leijen. 2008. HMF: Simple Type Inference for First-class Polymorphism. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming. ICFP 283\u2013294. https:\/\/doi.org\/10.1145\/1411204.1411245 10.1145\/1411204.1411245","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276483"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360207"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632890"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796806006034"},{"key":"e_1_3_2_41_1","unstructured":"Benjamin Crawford Pierce. 1992. Programming with intersection types and bounded polymorphism. Ph. D. Dissertation. USA. UMI Order No. GAX92-16028."},{"key":"e_1_3_2_42_1","unstructured":"Benjamin Crawford Pierce. 1992. Programming with intersection types and bounded polymorphism. Ph. D. Dissertation. USA. UMI Order No. GAX92-16028."},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_44_1","unstructured":"John C Reynolds. 1983. Types Abstraction and Parametric Polymorphism. Information Processing (1983) 513\u2013523."},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Nick Rioux Xuejing Huang Bruno C. d. S. Oliveira and Steve Zdancewic. 2023. A Bowtie for a Beast: Overloading Eta Expansion and Extensible Data Types in F\u22b2\u22b3. Proc. ACM Program. Lang. 7 POPL Article 18 (jan 2023) 29 pages. https:\/\/doi.org\/10.1145\/3571211 10.1145\/3571211","DOI":"10.1145\/3571211"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984008"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/72551.72555"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503292"},{"key":"e_1_3_2_51_1","article-title":"The subtyping problem for second-order types is undecidable","author":"Tiuryn Jerzy","year":"1996","unstructured":"Jerzy Tiuryn and Pawel Urzyczyn. 1996. The subtyping problem for second-order types is undecidable. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science.","journal-title":"Proceedings 11th Annual IEEE Symposium on Logic in Computer Science"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328486"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3310339"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.2"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341716"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704907","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704907","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:05Z","timestamp":1770200225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704907"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704907"],"URL":"https:\/\/doi.org\/10.1145\/3704907","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}