{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:58Z","timestamp":1779836758254,"version":"3.53.1"},"reference-count":78,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2022,10,6]],"date-time":"2022-10-06T00:00:00Z","timestamp":1665014400000},"content-version":"unspecified","delay-in-days":278,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically typed to more statically typed or vice versa, gradual typing itself does not provide a way to facilitate this migration. This places the burden on programmers who have to manually add or remove type annotations. Besides the general challenge of adding type annotations to dynamically typed code, there are subtle interactions between these annotations in gradually typed code that exacerbate the situation. For example, to migrate a program to be as static as possible, in general, all possible combinations of adding or removing type annotations from parameters must be tried out and compared. In this paper, we address this problem by developing\n                    <jats:italic>migrational typing<\/jats:italic>\n                    , which efficiently types all possible ways of replacing dynamic types with fully static types for a gradually typed program. The typing result supports automatically migrating a program to be as static as possible or introducing the least number of dynamic types necessary to remove a type error. The approach can be extended to support user-defined criteria about which annotations to modify. We have implemented migrational typing and evaluated it on large programs. The results show that migrational typing scales linearly with the size of the program and takes only 2\u20134 times longer than plain gradual typing.\n                  <\/jats:p>","DOI":"10.1017\/s0956796822000089","type":"journal-article","created":{"date-parts":[[2022,10,6]],"date-time":"2022-10-06T08:35:45Z","timestamp":1665045345000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":1,"title":["Migrating gradual types"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5301-9552","authenticated-orcid":false,"suffix":"III","given":"JOHN PETER","family":"CAMPORA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1735-0704","authenticated-orcid":false,"given":"SHENG","family":"CHEN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"MARTIN","family":"ERWIG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ERIC","family":"WALKINGSHAW","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,10,6]]},"reference":[{"key":"S0956796822000089_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35992-7_2"},{"key":"S0956796822000089_ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_21"},{"key":"S0956796822000089_ref57","unstructured":"Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Workshop on Scheme and Functional Programming, pp. 81\u201392."},{"key":"S0956796822000089_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009865"},{"key":"S0956796822000089_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46014-4_27"},{"key":"S0956796822000089_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103714"},{"key":"S0956796822000089_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3426422.3426985"},{"key":"S0956796822000089_ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ICSME.2016.88"},{"key":"S0956796822000089_ref61","doi-asserted-by":"publisher","DOI":"10.1145\/3141848.3141852"},{"key":"S0956796822000089_ref9","doi-asserted-by":"crossref","unstructured":"Campora, J. , Chen, S. , Erwig, M. & Walkingshaw, E. (2022) Migrating Gradual Types. Tech. rept. University of Louisiana at Lafayette. Available at: https:\/\/people.cmix.louisiana.edu\/schen\/ws\/techreport\/MGT-With-Proofs.pdf.","DOI":"10.1017\/S0956796822000089"},{"key":"S0956796822000089_ref67","author":"Tobin-Hochstadt","year":"2017"},{"key":"S0956796822000089_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009863"},{"key":"S0956796822000089_ref65","doi-asserted-by":"publisher","DOI":"10.1145\/2580950"},{"key":"S0956796822000089_ref68","doi-asserted-by":"publisher","DOI":"10.1145\/3290330"},{"key":"S0956796822000089_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_14"},{"key":"S0956796822000089_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314627"},{"key":"S0956796822000089_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_19"},{"key":"S0956796822000089_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3110283"},{"key":"S0956796822000089_ref70","unstructured":"van Keeken, P. (2006) Analyzing Helium Programs Obtained through Logging\u2013the Process of Mining Novice Haskell Programs. M.Phil. thesis, Department of Information and Computing Sciences, Utrecht University."},{"key":"S0956796822000089_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"S0956796822000089_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"S0956796822000089_ref32","doi-asserted-by":"crossref","unstructured":"Henglein, F. & Rehof, J. (1995) Safe polymorphic type inference for a dynamically typed language: Translating scheme to ml. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture. FPCA\u201995. New York, NY, USA: Association for Computing Machinery, pp. 192\u2013203.","DOI":"10.1145\/224164.224203"},{"key":"S0956796822000089_ref20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2518190","article-title":"Extending type inference to variational programs","volume":"36","author":"Chen","year":"2014","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"S0956796822000089_ref19","doi-asserted-by":"crossref","unstructured":"Chen, S. , Erwig, M. & Walkingshaw, E. (2012) An error-tolerant type system for variational lambda calculus. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. ICFP\u201912. New York, NY, USA: ACM, pp. 29\u201340.","DOI":"10.1145\/2364527.2364535"},{"key":"S0956796822000089_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837665"},{"key":"S0956796822000089_ref4","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1145\/2714064.2660222","article-title":"Confined gradual typing","volume":"49","author":"Allende","year":"2014","journal-title":"Sigplan Not."},{"key":"S0956796822000089_ref43","doi-asserted-by":"crossref","unstructured":"Migeed, Z. & Palsberg, J. (2019) What is decidable about gradual types? Proc. ACM Program. Lang. 4(POPL), 1\u201329.","DOI":"10.1145\/3371097"},{"key":"S0956796822000089_ref76","doi-asserted-by":"crossref","unstructured":"Walkingshaw, E. , K\u00e4stner, C. , Erwig, M. , Apel, S. & Bodden, E. (2014) Variational data structures: Exploring tradeoffs in computing with variability. In Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. Onward! 2014. New York, NY, USA: ACM, pp. 213\u2013226.","DOI":"10.1145\/2661136.2661143"},{"key":"S0956796822000089_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3158103"},{"key":"S0956796822000089_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3428259"},{"key":"S0956796822000089_ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1978.1675141"},{"key":"S0956796822000089_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3290329"},{"key":"S0956796822000089_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3485483"},{"key":"S0956796822000089_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568300"},{"key":"S0956796822000089_ref64","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449788"},{"key":"S0956796822000089_ref75","doi-asserted-by":"crossref","unstructured":"Walkingshaw, E. & Ostermann, K. (2014) Projectional editing of variational software. In ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE). ACM, pp. 29\u201338.","DOI":"10.1145\/2775053.2658766"},{"key":"S0956796822000089_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2063239.2063245"},{"key":"S0956796822000089_ref59","doi-asserted-by":"crossref","unstructured":"Siek, J. G. , & Vachharajani, M. (2008). Gradual typing with unification-based inference. In Proceedings of the 2008 Symposium on Dynamic Languages. DLS\u201908. New York, NY, USA: ACM, pp. 7:1\u20137:12.","DOI":"10.1145\/1408681.1408688"},{"key":"S0956796822000089_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535863"},{"key":"S0956796822000089_ref15","first-page":"2:1","author":"Chen","year":"2019"},{"key":"S0956796822000089_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1953163.1953308"},{"key":"S0956796822000089_ref33","doi-asserted-by":"crossref","unstructured":"Igarashi, A. , Thiemann, P. , Vasconcelos, V. T. & Wadler, P. (2017). Gradual session types. Proc. ACM Program. Lang. 1(ICFP), 38:1\u201338:28.","DOI":"10.1145\/3110282"},{"key":"S0956796822000089_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"S0956796822000089_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3290331"},{"key":"S0956796822000089_ref63","doi-asserted-by":"crossref","unstructured":"Takikawa, A. , Feltey, D. , Greenman, B. , New, M. S. , Vitek, J. & Felleisen, M. (2016) Is sound gradual typing dead? In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL\u201916. New York, NY, USA: ACM, pp. 456\u2013468.","DOI":"10.1145\/2837614.2837630"},{"key":"S0956796822000089_ref5","volume-title":"Feature-Oriented Software Product Lines","author":"Apel","year":"2016"},{"key":"S0956796822000089_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"S0956796822000089_ref73","doi-asserted-by":"crossref","unstructured":"Wadler, P. & Findler, R. B. (2007) Well-typed programs can\u2019t be blamed. In Proceedings of the 2007 Workshop on Scheme and Functional Programming, pp. 1\u201313.","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"S0956796822000089_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3110285"},{"key":"S0956796822000089_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985864"},{"key":"S0956796822000089_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"S0956796822000089_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/3133872"},{"key":"S0956796822000089_ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2048237.2048241"},{"key":"S0956796822000089_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2489804.2489810"},{"key":"S0956796822000089_ref66","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S. & Felleisen, M. (2006) Interlanguage migration: From scripts to programs. In Companion to the 21st ACM SIGPLAN Symposium on Object-Oriented Programming Systems, Languages, and Applications. OOPSLA\u201906. New York, NY, USA: Association for Computing Machinery, pp. 964\u2013974.","DOI":"10.1145\/1176617.1176755"},{"key":"S0956796822000089_ref72","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1017\/S0956796811000098","article-title":"Outsidein(x) modular type inference with local assumptions","volume":"21","author":"Vytiniotis","year":"2011","journal-title":"J. Funct. Program."},{"key":"S0956796822000089_ref77","unstructured":"Wei, J. , Goyal, M. , Durrett, G. & Dillig, I. (2020) Lambdanet: Probabilistic type inference using graph neural networks. In International Conference on Learning Representations."},{"key":"S0956796822000089_ref60","unstructured":"Siek, J. G. , Vitousek, M. M. , Cimini, M. & Boyland, J. T. (2015) Refined Criteria for Gradual Typing. LIPIcs-Leibniz International Proceedings in Informatics, vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0956796822000089_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_29"},{"key":"S0956796822000089_ref45","first-page":"53","article-title":"Analyzing novice programmers\u2019 response to compiler error messages","volume":"31","author":"Munson","year":"2016","journal-title":"J. Comput. Sci. Colleges"},{"key":"S0956796822000089_ref17","doi-asserted-by":"crossref","unstructured":"Chen, S. & Erwig, M. (2014b) Guided type debugging. In International Symposium on Functional and Logic Programming. LNCS, vol. 8475, pp. 35\u201351.","DOI":"10.1007\/978-3-319-07151-0_3"},{"key":"S0956796822000089_ref71","doi-asserted-by":"crossref","unstructured":"Vytiniotis, D. , Peyton Jones, S. & Magalh\u00e3es, J. (2012) Equality proofs and deferred type errors: A compiler pearl. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming. ICFP\u201912, pp. 341\u2013352.","DOI":"10.1145\/2364527.2364554"},{"key":"S0956796822000089_ref21","unstructured":"Chen, S. , Erwig, M. & Walkingshaw, E. (2016) A calculus for variational programming. In European Conference on Object-Oriented Programming (ECOOP), pp. 6:1\u20136:26."},{"key":"S0956796822000089_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983994"},{"key":"S0956796822000089_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660230"},{"key":"S0956796822000089_ref47","doi-asserted-by":"crossref","unstructured":"New, M. S. , Jamner, D. & Ahmed, A. (2019) Graduality and parametricity: Together again for the first time. Proc. ACM Program. Lang. 4(POPL), 1\u201332.","DOI":"10.1145\/3371114"},{"key":"S0956796822000089_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"S0956796822000089_ref78","doi-asserted-by":"publisher","DOI":"10.1145\/3276504"},{"key":"S0956796822000089_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3236793"},{"key":"S0956796822000089_ref1","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/1925844.1926409","article-title":"Blame for all","volume":"46","author":"Ahmed","year":"2011","journal-title":"Sigplan Not."},{"key":"S0956796822000089_ref53","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"S0956796822000089_ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_2"},{"key":"S0956796822000089_ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3485488"},{"key":"S0956796822000089_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"S0956796822000089_ref22","doi-asserted-by":"crossref","unstructured":"Chugh, R. , Rondon, P. M. & Jhala, R. (2012) Nested refinements: A logic for duck typing. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL\u201912. New York, NY, USA: Association for Computing Machinery, pp. 231\u2013244.","DOI":"10.1145\/2103656.2103686"},{"key":"S0956796822000089_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3023956.3023966"},{"key":"S0956796822000089_ref55","first-page":"672","author":"Serrano","year":"2016"},{"key":"S0956796822000089_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/136035.136043"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796822000089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:53Z","timestamp":1779835013000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796822000089\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":78,"alternative-id":["S0956796822000089"],"URL":"https:\/\/doi.org\/10.1017\/s0956796822000089","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e14"}}