John Peter Campora
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Gradual typing provides a methodology to integrate static and dynamic typing, harmonizing their often conflicting advantages in a single language. When a user wants to enjoy the advantages of static typing, most gradual languages require that they add type annotations. Many nontrivial tasks must be undertaken while adding type annotations, including understanding program behaviors and invariants. Unfortunately, if this is done incorrectly then the added type annotations can be wrong–leading to inconsistencies between the program and the type annotations. Gradual typing implementations detect such inconsistencies at runtime, raise cast errors, and generate messages. However, solely relying on such error messages for understanding and fixing inconsistencies and their resulting cast errors is often insufficient for multiple reasons. One reason is that while such messages cover inconsistencies in one execution path, fixing them often requires reconciling information from multiple paths. Another is that users may add many wrong type annotations that they later find difficult to identify and fix, when considering all added annotations.
Recent studies provide evidence that type annotations added during program migration are often wrong and that many programmers prefer compile-time warnings about wrong annotations. Motivated by these results, we develop exploratory typing to help with the static detection, understanding, and fixing of inconsistencies. The key idea of exploratory typing is that it systematically removes dynamic types and explores alternative types for static type annotations that can remedy inconsistencies. To demonstrate the feasibility of exploratory typing, we have implemented it in PyHound, which targets programs written in Reticulated Python, a gradual variant of Python. We have evaluated PyHound on a set of Python programs, and the evaluation results demonstrate that our idea can effectively detect inconsistencies in 98% of the tested programs and fix 93% of inconsistencies, significantly outperforming pytype, a widely used Python tool for enforcing type annotations.
Supplemental Material
- 2020. Pytype. https://github.com/google/pytype Last accessed on April 27th, 2020.Google Scholar
- Martín Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. 1991. Dynamic Typing in a Statically Typed Language. ACM Trans. Program. Lang. Syst. 13, 2 (April 1991 ), 237-268. https://doi.org/10.1145/103135.103138 Google ScholarDigital Library
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. SIGPLAN Not. 46, 1 (Jan. 2011 ), 201-214. https://doi.org/10.1145/1925844.1926409 Google ScholarDigital Library
- Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. 2017. Theorems for Free for Free: Parametricity, with and Without Types. Proc. ACM Program. Lang. 1, ICFP, Article 39 ( Aug. 2017 ), 28 pages. https://doi.org/10.1145/3110283 Google ScholarDigital Library
- Alex Aiken and Brian Murphy. 1991. Static Type Inference in a Dynamically Typed Language. In Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '91). ACM, New York, NY, USA, 279-290. https://doi.org/10.1145/99583.99621 Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A Theory of Gradual Efect Systems. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14). ACM, New York, NY, USA, 283-295. https://doi.org/10.1145/2628136.2628149 Google ScholarDigital Library
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2016. Gradual type-and-efect systems. Journal of Functional Programming 26 ( 2016 ), e19. https://doi.org/10.1017/S0956796816000162 Google ScholarCross Ref
- Johannes Bader, Jonathan Aldrich, and Éric Tanter. 2018. Gradual Program Verification. In Verification, Model Checking, and Abstract Interpretation, Isil Dillig and Jens Palsberg (Eds.). Springer International Publishing, Cham, 25-46.Google Scholar
- Bernd Braßel. 2004. TypeHope: There is hope for your type errors. In Int. Workshop on Implementation of Functional Languages.Google Scholar
- John Campora, Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2018b. Migrating Gradual Types. In Proceedings of the 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '18). ACM, New York, NY, USA.Google ScholarDigital Library
- John Peter Campora, Sheng Chen, and Eric Walkingshaw. 2018a. Casts and Costs: Harmonizing Safety and Performance in Gradual Typing. Proc. ACM Program. Lang. 2, ICFP, Article 98 ( July 2018 ), 30 pages. https://doi.org/10.1145/3236793 Google ScholarDigital Library
- Robert Cartwright and Mike Fagan. 1991. Soft Typing. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation (PLDI '91). ACM, New York, NY, USA, 278-292. https://doi.org/10.1145/113445. 113469 Google ScholarDigital Library
- Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2017 ). To appear.Google Scholar
- Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. 2017. Fast and Precise Type Checking for JavaScript. Proc. ACM Program. Lang. 1, OOPSLA, Article 48 (Oct. 2017 ), 30 pages. https://doi.org/10.1145/3133872 Google ScholarDigital Library
- S. Chen, M. Erwig, and E. Walkingshaw. 2012a. An Error-Tolerant Type System for Variational Lambda Calculus. In ACM Int. Conf. on Functional Programming. 29-40.Google Scholar
- Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2012b. An Error-tolerant Type System for Variational Lambda Calculus. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming (ICFP '12). ACM, New York, NY, USA, 29-40. https://doi.org/10.1145/2364527.2364535 Google ScholarDigital Library
- S. Chen, M. Erwig, and E. Walkingshaw. 2014a. Extending Type Inference to Variational Programs. ACM Trans. on Programming Languages and Systems 36, 1, Article 1 ( 2014 ), 54 pages.Google ScholarDigital Library
- Sheng Chen, Martin Erwig, and Eric Walkingshaw. 2014b. Extending Type Inference to Variational Programs. ACM Trans. Program. Lang. Syst. 36, 1, Article 1 (March 2014 ), 54 pages. https://doi.org/10.1145/2518190 Google ScholarDigital Library
- Tim Disney and Cormac Flanagan. 2011. Gradual Information Flow Typing. In International Workshop on Scripts to Programs.Google Scholar
- Oli Evans and Alan Shaw. 2018. asciify. https://github.com/olizilla/asciifyGoogle Scholar
- Asger Feldthaus and Anders Møller. 2014. Checking Correctness of TypeScript Interfaces for JavaScript Libraries. SIGPLAN Not. 49, 10 (Oct. 2014 ), 1-16. https://doi.org/10.1145/2714064.2660215 Google ScholarDigital Library
- Luminous Fennell and Peter Thiemann. 2013. Gradual Security Typing with References. In Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium (CSF '13). IEEE Computer Society, Washington, DC, USA, 224-239. https://doi.org/10.1109/CSF. 2013.22 Google ScholarDigital Library
- Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). ACM, New York, NY, USA, 303-315. https://doi.org/10.1145/2676726.2676992 Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). ACM, New York, NY, USA, 429-442. https://doi.org/10.1145/2837614.2837670 Google ScholarDigital Library
- Ronald Garcia, Éric Tanter, Roger Wolf, and Jonathan Aldrich. 2014. Foundations of Typestate-Oriented Programming. ACM Trans. Program. Lang. Syst. 36, 4, Article 12 (Oct. 2014 ), 44 pages. https://doi.org/10.1145/2629609 Google ScholarDigital Library
- Fritz Henglein. 1994. Dynamic Typing: Syntax and Proof Theory. In Selected Papers of the Symposium on Fourth European Symposium on Programming (ESOP'92). Elsevier Science Publishers B. V., Amsterdam, The Netherlands, The Netherlands, 197-230. http://dl.acm.org/citation.cfm?id= 197475. 190867Google Scholar
- David Herman, Aaron Tomb, and Cormac Flanagan. 2010. Space-eficient Gradual Typing. Higher Order Symbol. Comput. 23, 2 ( June 2010 ), 167-189. https://doi.org/10.1007/s10990-011-9066-z Google ScholarDigital Library
- Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, and Philip Wadler. 2017b. Gradual Session Types. In ACM SIGPLAN International Conference on Functional Programming (ICFP 2017 ). To appear.Google Scholar
- Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017a. On Polymorphic Gradual Typing. Proc. ACM Program. Lang. 1, ICFP, Article 40 ( Aug. 2017 ), 29 pages. https://doi.org/10.1145/3110284 Google ScholarDigital Library
- Lintaro Ina and Atsushi Igarashi. 2011. Gradual Typing for Generics. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA '11). ACM, New York, NY, USA, 609-624. https://doi.org/10.1145/2048066.2048114 Google ScholarDigital Library
- Khurram A. Jafery and Joshua Dunfield. 2017. Sums of Uncertainty: Refinements Go Gradual. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017 ). ACM, New York, NY, USA, 804-817. https://doi.org/10.1145/3009837.3009865 Google ScholarDigital Library
- Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. 2016. Occurrence Typing Modulo Theories. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '16). ACM, New York, NY, USA, 296-309. https://doi.org/10.1145/2908080.2908091 Google ScholarDigital Library
- Kenneth Knowles and Cormac Flanagan. 2010. Hybrid Type Checking. ACM Trans. Program. Lang. Syst. 32, 2, Article 6 ( Feb. 2010 ), 34 pages. https://doi.org/10.1145/1667048.1667051 Google ScholarDigital Library
- Erik Krogh Kristensen and Anders Møller. 2017a. Inference and Evolution of TypeScript Declaration Files. In Fundamental Approaches to Software Engineering, Marieke Huisman and Julia Rubin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 99-115.Google Scholar
- Erik Krogh Kristensen and Anders Møller. 2017b. Type Test Scripts for TypeScript Testing. Proc. ACM Program. Lang. 1, OOPSLA, Article 90 (Oct. 2017 ), 25 pages. https://doi.org/10.1145/3133914 Google ScholarDigital Library
- Nico Lehmann and Éric Tanter. 2017. Gradual Refinement Types. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017 ). ACM, New York, NY, USA, 775-788. https://doi.org/10.1145/3009837. 3009856 Google ScholarDigital Library
- Phúc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. 2014. Soft Contract Verification. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP '14). ACM, New York, NY, USA, 139-152. https://doi.org/10.1145/2628136.2628156 Google ScholarDigital Library
- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. 2007. Practical Type Inference for Arbitraryrank Types. J. Funct. Program. 17, 1 (Jan. 2007 ), 1-82.Google ScholarDigital Library
- Ilya Sergey and Dave Clarke. 2012. Gradual Ownership Types. In Proceedings of the 21st European Conference on Programming Languages and Systems (ESOP'12). Springer-Verlag, Berlin, Heidelberg, 579-599. https://doi.org/10.1007/978-3-642-28869-2_29 Google ScholarDigital Library
- Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects. In Proceedings of the 21st European Conference on ECOOP 2007 : Object-Oriented Programming ( ECOOP '07). Springer-Verlag, Berlin, Heidelberg, 2-27. https://doi.org/10.1007/978-3-540-73589-2_2 Google ScholarDigital Library
- Jeremy Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Eficient Gradual Typing. https://doi.org/10.1007/978-3-662-46669-8_18 Google ScholarDigital Library
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In IN SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP. 81-92.Google Scholar
- Jeremy G. Siek and Manish Vachharajani. 2008. Gradual Typing with Unification-based Inference. In Proceedings of the 2008 Symposium on Dynamic Languages (DLS '08). ACM, New York, NY, USA, Article 7, 12 pages. https://doi.org/10.1145/ 1408681.1408688 Google ScholarDigital Library
- Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.Google Scholar
- Vincent St-Amour and Neil Toronto. 2013. Experience Report: Applying Random Testing to a Base Type Environment. In ACM Int. Conf. on Functional Programming. 351-356.Google ScholarDigital Library
- Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead?. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). ACM, New York, NY, USA, 456-468. https://doi.org/10.1145/2837614.2837630 Google ScholarDigital Library
- Satish Thatte. 1988. Type inference with partial types. In Automata, Languages and Programming, Timo Lepistö and Arto Salomaa (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 615-629.Google Scholar
- Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs. In Companion to the 21st ACM SIGPLAN Symposium on Object-oriented Programming Systems, Languages, and Applications (OOPSLA '06). ACM, New York, NY, USA, 964-974. https://doi.org/10.1145/1176617.1176755 Google ScholarDigital Library
- Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '08). ACM, New York, NY, USA, 395-406. https://doi.org/10.1145/1328438.1328486 Google ScholarDigital Library
- Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa. 2017. Migratory Typing: Ten Years Later. In 2nd Summit on Advances in Programming Languages (SNAPL 2017 ) (Leibniz International Proceedings in Informatics (LIPIcs)), Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi (Eds.), Vol. 71. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 17 : 1-17 : 17. https://doi.org/10.4230/LIPIcs.SNAPL. 2017.17 Google ScholarCross Ref
- Matías Toro, Elizabeth Labrada, and Éric Tanter. 2019. Gradual Parametricity, Revisited. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '19). To appear.Google Scholar
- Matías Toro and Éric Tanter. 2017. A Gradual Interpretation of Union Types. In SAS.Google Scholar
- Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. 2018. The Behavior of Gradual Types: A User Study. In Proceedings of the 14th ACM SIGPLAN International Symposium on Dynamic Languages (DLS 2018 ). ACM, New York, NY, USA, 1-12. https://doi.org/10.1145/3276945.3276947 Google ScholarDigital Library
- Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for Python. ( 2014 ), 45-56.Google Scholar
- Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. 2017. Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017 ). ACM, New York, NY, USA, 762-774. https://doi.org/10.1145/3009837.3009849 Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can't Be Blamed. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009 (ESOP '09). Springer-Verlag, Berlin, Heidelberg, 1-16. https://doi.org/10.1007/978-3-642-00590-9_1 Google ScholarDigital Library
- Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. 2017. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In 31st European Conference on Object-Oriented Programming (ECOOP 2017 ) (Leibniz International Proceedings in Informatics (LIPIcs)), Peter Müller (Ed.), Vol. 74. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 28 : 1-28 : 29. https://doi.org/10.4230/LIPIcs.ECOOP. 2017.28 Google ScholarCross Ref
- Roger Wolf, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual Typestate. In Proceedings of the 25th European Conference on Object-oriented Programming (ECOOP'11). Springer-Verlag, Berlin, Heidelberg, 459-483. http://dl.acm.org/citation.cfm?id= 2032497. 2032529Google Scholar
- Baijun Wu and Sheng Chen. 2017. How Type Errors Were Fixed and What Students Did? Proc. ACM Program. Lang. 1, OOPSLA, Article 105 (Oct. 2017 ), 27 pages. https://doi.org/10.1145/3133929 Google ScholarDigital Library
- Ningning Xie, Xuan Bi, and Bruno C. d. S. Oliveira. 2018. Consistent Subtyping for All. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 3-30.Google Scholar
Index Terms
- Taming type annotations in gradual typing
Recommendations
Gradual typing: a new perspective
We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type ...
Migrating gradual types
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 ...
On polymorphic gradual typing
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically ...
Comments