{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T16:44:35Z","timestamp":1785602675598,"version":"3.56.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T00:00:00Z","timestamp":1574294400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Research Foundation - Flanders"},{"name":"Hong Kong Research Grant Council","award":["17210617,17258816"],"award-info":[{"award-number":["17210617,17258816"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,3,31]]},"abstract":"<jats:p>Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by\u00a0Siek and Taha serves as a guideline for designing gradual type systems with subtyping. Polymorphic types \u00e0 la System F also induce a subtyping relation that relates polymorphic types to their instantiations. However, Siek and Taha\u2019s definition is not adequate for polymorphic subtyping. The first goal of this article is to propose a generalization of consistent subtyping that is adequate for polymorphic subtyping and subsumes the original definition by\u00a0Siek and Taha. The new definition of consistent subtyping provides novel insights with respect to previous polymorphic gradual type systems, which did not employ consistent subtyping. The second goal of this article is to present a gradually typed calculus for implicit (higher-rank) polymorphism that uses our new notion of consistent subtyping. We develop both declarative and (bidirectional) algorithmic versions for the type system. The algorithmic version employs techniques developed by\u00a0Dunfield and Krishnaswami for higher-rank polymorphism to deal with instantiation. We prove that the new calculus satisfies all static aspects of the refined criteria for gradual typing. We also study an extension of the type system with static and gradual type parameters, in an attempt to support a variant of the dynamic criterion for gradual typing. Assuming a coherence conjecture for the extended calculus, we show that the dynamic gradual guarantee of our source language can be reduced to that of \u03bb B, which, at the time of writing, is still an open question. Most of the metatheory of this article, except some manual proofs for the algorithmic type system and extensions, has been mechanically formalized using the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3310339","type":"journal-article","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T13:35:22Z","timestamp":1574343322000},"page":"1-79","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Consistent Subtyping for All"],"prefix":"10.1145","volume":"42","author":[{"given":"Ningning","family":"Xie","sequence":"first","affiliation":[{"name":"The University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuan","family":"Bi","sequence":"additional","affiliation":[{"name":"The University of Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno C. D. S.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"The University of Hong Kong, Hong Kong, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom","family":"Schrijvers","sequence":"additional","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000126X"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926409"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 19th International Conference on Functional Programming.","author":"Schwerter Felipe Ba\u00f1ados","year":"2014","unstructured":"Felipe Ba\u00f1ados Schwerter, Ronald Garcia, and \u00c9ric Tanter. 2014. A theory of gradual effect systems. In Proceedings of the 19th International Conference on Functional Programming."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming.","author":"Bierman Gavin","year":"2010","unstructured":"Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding dynamic types to C#. In Proceedings of the European Conference on Object-Oriented Programming."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Ambrose Bonnaire-Sergeant Rowan Davies and Sam Tobin-Hochstadt. 2016. Practical optional types for clojure. In Programming Languages and Systems.","DOI":"10.1007\/978-3-662-49498-1_4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"e_1_2_1_10_1","volume-title":"The Calculi of Lambda-conversion. Number 6","author":"Church Alonzo","unstructured":"Alonzo Church. 1941. The Calculi of Lambda-conversion. Number 6. Princeton University Press."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 43rd Symposium on Principles of Programming Languages.","author":"Cimini Matteo","unstructured":"Matteo Cimini and Jeremy G. Siek. 2016. The gradualizer: A methodology and algorithm for generating gradual type systems. In Proceedings of the 43rd Symposium on Principles of Programming Languages."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 44th Symposium on Principles of Programming Languages.","author":"Cimini Matteo","unstructured":"Matteo Cimini and Jeremy G. Siek. 2017. Automatically generating the dynamic semantics of gradually typed languages. In Proceedings of the 44th Symposium on Principles of Programming Languages."},{"key":"e_1_2_1_13_1","volume-title":"Seldin","author":"Curry Haskell Brooks","year":"1958","unstructured":"Haskell Brooks Curry, Robert Feys, William Craig, J. Roger Hindley, and Jonathan P. Seldin. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351259"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the International Conference on Functional Programming. https:\/\/arxiv.org\/abs\/1306","author":"Dunfield Joshua","unstructured":"Joshua Dunfield and Neelakantan R. Krishnaswami. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proceedings of the International Conference on Functional Programming. https:\/\/arxiv.org\/abs\/1306.6032."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop.","author":"Gronski Jessica","year":"2006","unstructured":"Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. Sage: Hybrid checking for flexible specifications. In Proceedings of the Scheme and Functional Programming Workshop."},{"key":"e_1_2_1_21_1","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley J. Roger","year":"1969","unstructured":"J. Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29--60.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 44th Symposium on Principles of Programming Languages. 14","author":"Khurram","unstructured":"Khurram A. Jafery and Joshua Dunfield. 2017. Sums of uncertainty: Refinements go gradual. In Proceedings of the 44th Symposium on Principles of Programming Languages. 14."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_15"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Haskell Workshop","volume":"1997","author":"Jones Simon Peyton","year":"1997","unstructured":"Simon Peyton Jones, Mark Jones, and Erik Meijer. 1997. Type classes: Exploring the design space. In Proceedings of the Haskell Workshop, Vol. 1997."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944709"},{"key":"e_1_2_1_28_1","first-page":"726","article-title":"Recasting MLF. Info","volume":"207","author":"Botlan Didier Le","year":"2009","unstructured":"Didier Le Botlan and Didier R\u00e9my. 2009. Recasting MLF. Info. Comput. 207, 6 (2009), 726--785.","journal-title":"Comput."},{"key":"e_1_2_1_29_1","unstructured":"Jukka Lehtosalo et al. 2006. Mypy. Retrieved from http:\/\/www.mypy-lang.org\/."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480891"},{"key":"e_1_2_1_31_1","volume-title":"Parametric polymorphism through run-time sealing or, theorems for low, low prices&excl","author":"Matthews Jacob","unstructured":"Jacob Matthews and Amal Ahmed. 2008. Parametric polymorphism through run-time sealing or, theorems for low, low prices&excl; In Proceedings of the European Symposium on Programming. Springer, 16--31."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004355"},{"key":"e_1_2_1_33_1","volume-title":"Logical Foundations of Functional Programming","author":"Mitchell John C.","unstructured":"John C. Mitchell. 1990. Polymorphic type inference and containment. In Logical Foundations of Functional Programming. Addison-Wesley, Boston, MA."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512938"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596572"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90042-E"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_2_1_40_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411216"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress.","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In Proceedings of the IFIP 9th World Computer Congress."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670915"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_2"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the Scheme and Functional Programming Workshop.","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming.","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2007. Gradual typing for objects. In Proceedings of the European Conference on Object-Oriented Programming."},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the Symposium on Dynamic Languages.","author":"Jeremy","unstructured":"Jeremy G. Siek and Manish Vachharajani. 2008. Gradual typing with unification-based inference. In Proceedings of the Symposium on Dynamic Languages."},{"key":"e_1_2_1_48_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics.","author":"Siek Jeremy G.","year":"2015","unstructured":"Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics."},{"key":"e_1_2_1_49_1","volume-title":"Siek and Philip Wadler","author":"Jeremy","year":"2016","unstructured":"Jeremy G. Siek and Philip Wadler. 2016. The Key to Blame: Gradual Typing Meets Cryptography (draft)."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of Commercial Users of Functional Programming.","author":"Verlaguet Julien","year":"2013","unstructured":"Julien Verlaguet. 2013. Facebook: Analyzing PHP statically. In Proceedings of Commercial Users of Functional Programming."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661101"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00047-5"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the European Symposium on Programming. 3--30","author":"Xie Ningning","unstructured":"Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent subtyping for all. In Proceedings of the European Symposium on Programming. 3--30."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310339","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310339","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:37Z","timestamp":1750204417000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310339"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,21]]},"references-count":53,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3,31]]}},"alternative-id":["10.1145\/3310339"],"URL":"https:\/\/doi.org\/10.1145\/3310339","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,21]]},"assertion":[{"value":"2018-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}