{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:10Z","timestamp":1751663410868,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC-CZ","award":["LL2325"],"award-info":[{"award-number":["LL2325"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1910850, CNS-1925644, CCF-2139612"],"award-info":[{"award-number":["CCF-1910850, CNS-1925644, CCF-2139612"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"GACR EXPRO","award":["23-07580X"],"award-info":[{"award-number":["23-07580X"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>Julia is a modern scientific-computing language that relies on multiple dispatch to implement generic libraries. While the language does not have a static type system, method declarations are decorated with expressive type annotations to determine when they are applicable. To find applicable methods, the implementation uses subtyping at run-time. We show that Julia\u2019s subtyping is undecidable, and we propose a restriction on types to recover decidability by stratifying types into method signatures over value types\u2014where the former can freely use bounded existential types but the latter are restricted to use-site variance. A corpus analysis suggests that nearly all Julia programs written in practice already conform to this restriction.<\/jats:p>","DOI":"10.1145\/3656421","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1091-1114","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Decidable Subtyping of Existential Types for Julia"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7490-8500","authenticated-orcid":false,"given":"Julia","family":"Belyakova","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9238-7334","authenticated-orcid":false,"given":"Benjamin","family":"Chung","sequence":"additional","affiliation":[{"name":"JuliaHub, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7608-4605","authenticated-orcid":false,"given":"Ross","family":"Tate","sequence":"additional","affiliation":[{"name":"Independent Consultant, Ithaka, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4052-3458","authenticated-orcid":false,"given":"Jan","family":"Vitek","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"},{"name":"Charles University, Prague, Czechia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Alexander Aiken and Edward L. Wimmers. 1993. Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture (FPCA). https:\/\/doi.org\/10.1145\/165180.165188 10.1145\/165180.165188","DOI":"10.1145\/165180.165188"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.17760\/D20581904"},{"key":"e_1_3_2_4_1","volume-title":"Ph. D. Dissertation","author":"Bezanson Jeff","year":"2015","unstructured":"Jeff Bezanson. 2015. Abstraction in technical computing. Ph. D. Dissertation. Massachusetts Institute of Technology. http:\/\/hdl.handle.net\/1721.1\/99811"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276490"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1137\/141000671"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Daniel G. Bobrow Kenneth Kahn Gregor Kiczales Larry Masinter Mark Stefik and Frank Zdybel. 1986. CommonLoops: Merging Lisp and Object-Oriented Programming. In Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/28697.28700 10.1145\/28697.28700","DOI":"10.1145\/28697.28700"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Francois Bourdoncle and Stephan Merz. 1997. Type checking higher-order polymorphic multi-methods. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/263699.263743 10.1145\/263699.263743","DOI":"10.1145\/263699.263743"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"Nicholas Cameron Sophia Drossopoulou and Erik Ernst. 2008. A Model for Java with Wildcards. In European Conference on Object-Oriented Programming (ECOOP). https:\/\/doi.org\/10.1007\/978-3-540-70592-5_2 10.1007\/978-3-540-70592-5_2","DOI":"10.1007\/978-3-540-70592-5_2"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Luca Cardelli Simone Martini John C. Mitchell and Andre Scedrov. 1991. An Extension of System F with Subtyping. In Theoretical Aspects of Computer Software (TACS). https:\/\/doi.org\/10.1007\/3-540-54415-1_73 10.1007\/3-540-54415-1_73","DOI":"10.1007\/3-540-54415-1_73"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Principles and Practice of Declarative Programming (PPDP). https:\/\/doi.org\/10.1145\/1069774.1069793 10.1145\/1069774.1069793","DOI":"10.1145\/1069774.1069793"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Giuseppe Castagna Kim Nguyen Zhiwu Xu and Pietro Abate. 2015. Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2676726.2676991 10.1145\/2676726.2676991","DOI":"10.1145\/2676726.2676991"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Satish Chandra Colin S. Gordon Jean-Baptiste Jeannin Cole Schlesinger Manu Sridharan Frank Tip and Youngil Choi. 2016. Type inference for static compilation of JavaScript. https:\/\/doi.org\/10.1145\/2983990.2984017 10.1145\/2983990.2984017","DOI":"10.1145\/2983990.2984017"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.17760\/D20531813"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Benjamin Chung Francesco Zappa Nardelli and Jan Vitek. 2019. Julia\u2019s Efficient Algorithm for Subtyping Unions and Covariant Tuples. In European Conference on Object-Oriented Programming (ECOOP). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2019.24 10.4230\/LIPIcs.ECOOP.2019.24","DOI":"10.4230\/LIPIcs.ECOOP.2019.24"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Pierre-Louis Curien and Giorgio Ghelli. 1990. Coherence of subsumption. In Colloquium on Trees in Algebra and Programming (CAAP). https:\/\/doi.org\/10.1007\/3-540-52590-4_45 10.1007\/3-540-52590-4_45","DOI":"10.1007\/3-540-52590-4_45"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/582153.582176 10.1145\/582153.582176","DOI":"10.1145\/582153.582176"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Ben Greenman Fabian Muehlboeck and Ross Tate. 2014. Getting F-Bounded Polymorphism into Shape. In Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/2594291.2594308 10.1145\/2594291.2594308","DOI":"10.1145\/2594291.2594308"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Radu Grigore. 2017. Java Generics Are Turing Complete. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3009837.3009871 10.1145\/3009837.3009871","DOI":"10.1145\/3009837.3009871"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Roger Hindley. 1969. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc. (1969). https:\/\/doi.org\/10.2307\/1995158 10.2307\/1995158","DOI":"10.2307\/1995158"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/574901"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371077"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Atsushi Igarashi and Mirko Viroli. 2002. On Variance-Based Subtyping for Parametric Types. In European Conference on Object-Oriented Programming (ECOOP). https:\/\/doi.org\/10.1007\/3-540-47993-7_19 10.1007\/3-540-47993-7_19","DOI":"10.1007\/3-540-47993-7_19"},{"key":"e_1_3_2_27_1","unstructured":"Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance. In Foundations and Developments of Object-Oriented Languages (FOOL). https:\/\/www.microsoft.com\/en-us\/research\/publication\/on-decidability-of-nominal-subtyping-with-variance\/"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Kresten Krab Thorup and Mads Torgersen. 1999. Unifying Genericity. In European Conference on Object-Oriented Programming (ECOOP). https:\/\/doi.org\/10.1007\/3-540-48743-3_9 10.1007\/3-540-48743-3_9","DOI":"10.1007\/3-540-48743-3_9"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371134"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","unstructured":"Julian Mackay Alex Potanin Jonathan Aldrich and Lindsay Groves. 2020. Syntactically Restricting Bounded Polymorphism for Decidable Subtyping. In Programming Languages and Systems (APLAS). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_7 10.1007\/978-3-030-64437-6_7","DOI":"10.1007\/978-3-030-64437-6_7"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Greg Morrisett David Walker Karl Crary and Neal Glew. 1998. From System F to Typed Assembly Language. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/268946.268954 10.1145\/268946.268954","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485527"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/143165.143228 10.1145\/143165.143228","DOI":"10.1145\/143165.143228"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","unstructured":"Franc ois Pottier. 1998. A framework for type inference with subtyping. In International Conference on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/289423.289448 10.1145\/289423.289448","DOI":"10.1145\/289423.289448"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","unstructured":"Daniel Smith and Robert Cartwright. 2008. Java Type Inference is Broken: Can We Fix It?. In Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1449764.1449804 10.1145\/1449764.1449804","DOI":"10.1145\/1449764.1449804"},{"key":"e_1_3_2_36_1","unstructured":"Ross Tate Juan Chen and Chris Hawblitzel. 2008. A Flexible Framework for Type Inference with Existential Quantification. Technical Report MSR-TR-2008-184. https:\/\/www.microsoft.com\/en-us\/research\/publication\/a-flexible-framework-for-type-inference-with-existential-quantification\/"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","unstructured":"Ross Tate Juan Chen and Chris Hawblitzel. 2010. Inferable object-oriented typed assembly language. In Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/1806596.1806644 10.1145\/1806596.1806644","DOI":"10.1145\/1806596.1806644"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Ross Tate Alan Leung and Sorin Lerner. 2011. Taming Wildcards in Java\u2019s Type System. In Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/1993498.1993570 10.1145\/1993498.1993570","DOI":"10.1145\/1993498.1993570"},{"key":"e_1_3_2_39_1","unstructured":"Mads Torgersen Erik Ernst and Christian Plesner Hansen. 2005. Wild FJ. In Foundations of Object-Oriented Languages (FOOL). https:\/\/homepages.inf.ed.ac.uk\/wadler\/fool\/program\/final\/14\/14_Paper.pdf"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Mads Torgersen Christian Plesner Hansen Erik Ernst Peter von der Ah\u00e9 Gilad Bracha and Neal Gafter. 2004. Adding Wildcards to the Java Programming Language. In Symposium on Applied Computing (SAC). https:\/\/doi.org\/10.1145\/967900.968162 10.1145\/967900.968162","DOI":"10.1145\/967900.968162"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Valery Trifonov and Scott Smith. 1996. Subtyping constrained types. In Static Analysis Symposium (SAS). https:\/\/doi.org\/10.1007\/3-540-61739-6_52 10.1007\/3-540-61739-6_52","DOI":"10.1007\/3-540-61739-6_52"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Stefan Wehr and Peter Thiemann. 2009. On the Decidability of Subtyping with Bounded Existential Types. In Programming Languages and Systems (ESOP). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_10 10.1007\/978-3-642-10672-9_10","DOI":"10.1007\/978-3-642-10672-9_10"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276483"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656421","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656421","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:26Z","timestamp":1751661806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656421"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":42,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656421"],"URL":"https:\/\/doi.org\/10.1145\/3656421","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}