ABSTRACT
Combining static and dynamic typing within the same language offers clear benefits to programmers. It provides dynamic typing in situations that require rapid prototyping, heterogeneous data structures, and reflection, while supporting static typing when safety, modularity, and efficiency are primary concerns. Siek and Taha (2006) introduced an approach to combining static and dynamic typing in a fine-grained manner through the notion of type consistency in the static semantics and run-time casts in the dynamic semantics. However, many open questions remain regarding the semantics of gradually typed languages.
In this paper we present Reticulated Python, a system for experimenting with gradual-typed dialects of Python. The dialects are syntactically identical to Python 3 but give static and dynamic semantics to the type annotations already present in Python 3. Reticulated Python consists of a typechecker and a source-to-source translator from Reticulated Python to Python 3. Using Reticulated Python, we evaluate a gradual type system and three approaches to the dynamic semantics of mutable objects: the traditional semantics based on Siek and Taha (2007) and Herman et al. (2007) and two new designs. We evaluate these designs in the context of several third-party Python programs.
- M. Abadi and L. Cardelli. phA Theory of Objects. Springer-Verlag, 1996. Google ScholarDigital Library
- M. Abadi, L. Cardelli, B. C. Pierce, and G. D. Plotkin. Dynamic typing in a statically-typed language. In phPOPL, pages 213--227, 1989. Google ScholarDigital Library
- A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In phPOPL '11: ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '11, pages 1--14, 2011. Google ScholarDigital Library
- Fabry, Tanter, and Denker}allende:2013gradualtalkE. Allende, O. Callaú, J. Fabry, E. Tanter, and M. Denker. Gradual typing for smalltalk. phScience of Computer Programming, August 2013.Google Scholar
- G. Bierman, E. Meijer, and M. Torgersen. Adding dynamic types to C\#. In phEuropean Conference on Object-Oriented Programming, ECOOP'10. Springer-Verlag, 2010. Google ScholarDigital Library
- B. Bloom, J. Field, N. Nystrom, J. Östlund, G. Richards, R. Strnisa, J. Vitek, and T. Wrigstad. Thorn: Robust, concurrent, extensible scripting on the jvm. phSIGPLAN Not., 44 (10): 117--136, Oct. 2009. ISSN 0362--1340. Google ScholarDigital Library
- G. Bracha and D. Griswold. Strongtalk: typechecking Smalltalk in a production environment. In phOOPSLA '93: Proceedings of the eighth annual conference on Object-oriented programming systems, languages, and applications, pages 215--230, New York, NY, USA, 1993. ACM Press. ISBN 0--89791--587--9. Google ScholarDigital Library
- C. Chambers and the Cecil Group. The Cecil language: Specification and rationale. Technical report, Department of Computer Science and Engineering, University of Washington, Seattle, Washington, 2004.Google Scholar
- T. V. Cutsem and M. S. Miller. Trustworthy proxies: virtualizing objects with invariants. In phProceedings of the 27th European Conference on Object-Oriented Programming, ECOOP'13, pages 154--178, Berlin, Heidelberg, 2013. Springer-Verlag. 10.1007/978--3--642--39038--8_7. Google ScholarDigital Library
- Facebook. Hack, 2011. URL http://hacklang.org.Google Scholar
- R. B. Findler and M. Felleisen. Contracts for higher-order functions. Technical Report NU-CCS-02-05, Northeastern University, 2002.Google ScholarDigital Library
- Google. Dart: structured web apps, 2011. URL http://dartlang.org.Google Scholar
- K. E. Gray, R. B. Findler, and M. Flatt. Fine-grained interoperability through mirrors and contracts. In phOOPSLA '05: Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming systems languages and applications, pages 231--245, New York, NY, USA, 2005. ACM Press. ISBN 1--59593-031-0. Google ScholarDigital Library
- J. Gronski, K. Knowles, A. Tomb, S. N. Freund, and C. Flanagan. Sage: Hybrid checking for flexible specifications. In phScheme and Functional Programming Workshop, pages 93--104, 2006.Google Scholar
- D. Herman, A. Tomb, and C. Flanagan. Space-efficient gradual typing. In phTrends in Functional Prog. (TFP), page XXVIII, April 2007.Google Scholar
- L. Ina and A. Igarashi. Gradual typing for generics. In phACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA '11, 2011. Google ScholarDigital Library
- G. A. Kildall. A unified approach to global program optimization. In phPOPL '73: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 194--206. ACM Press, 1973. Google ScholarDigital Library
- B. S. Lerner, J. G. Politz, A. Guha, and S. Krishnamurthi. Tejas: Retrofitting type systems for JavaScript. In phSymposium on Dynamic Languages, DLS '13, pages 1--16, 2013. Google ScholarDigital Library
- E. Meijer and P. Drayton. Static typing where possible, dynamic typing when needed: The end of the cold war between programming languages. In phOOPSLA'04 Workshop on Revival of Dynamic Languages, 2004.Google Scholar
- J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, and S. Krishnamurthi. Python: The full monty. In phACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '13, pages 217--232, 2013. Google ScholarDigital Library
- A. Rastogi, A. Chaudhuri, and B. Hosmer. The ins and outs of gradual type inference. In phACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, POPL '12, 2012. Google ScholarDigital Library
- B. M. Ren, J. Toman, T. S. Strickland, and J. S. Foster. The ruby type checker. In phSAC'13 (OOPS), 2013. Google ScholarDigital Library
- G. Richards, C. Hammer, B. Burg, and J. Vitek. The eval that men do: A large-scale study of the use of eval in javascript applications. In phEuropean Conference on Object-Oriented Programming, ECOOP'11, pages 52--78, Berlin, Heidelberg, 2011. Google ScholarDigital Library
- M. Serrano. phBigloo: a practical Scheme compiler. Inria-Rocquencourt, April 2002.Google Scholar
- J. G. Siek. Is typescript gradually typed? part 2, Oct. 2013. URL http://siek.blogspot.com/2012/10/is-typescript- gradually-typed-part-2.html.Google Scholar
- J. G. Siek and W. Taha. Gradual typing for functional languages. In phScheme and Functional Programming Workshop, pages 81--92, September 2006.Google Scholar
- J. G. Siek and W. Taha. Gradual typing for objects. In phECOOP 2007, volume 4609 of phLCNS, pages 2--27. Springer Verlag, August 2007. Google ScholarDigital Library
- J. G. Siek and P. Wadler. Threesomes, with and without blame. In phSymposium on Principles of Programming Languages, 2010. Google ScholarDigital Library
- J. G. Siek, R. Garcia, and W. Taha. Exploring the design space of higher-order casts. In phEuropean Symposium on Programming, March 2009. Google ScholarDigital Library
- A. Takikawa, T. S. Strickland, C. Dimoulas, S. Tobin-Hochstadt, and M. Felleisen. Gradual typing for first-class classes. In phConference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 793--810, 2012. Google ScholarDigital Library
- S. Thatte. Quasi-static typing. In phPOPL 1990, pages 367--381, New York, NY, USA, 1990. ACM Press. ISBN 0--89791--343--4. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In phOOPSLA'06 Companion, pages 964--974, NY, 2006. ACM. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In phPOPL '08: the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In phACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 117--128, 2010. Google ScholarDigital Library
- P. Wadler and R. B. Findler. Well-typed programs can't be blamed. In phEuropean Symposium on Programming, 2009. Google ScholarDigital Library
- R. Wolff, R. Garcia, E. Tanter, and J. Aldrich. Gradual typestate. In phEuropean Conference on Object-Oriented Programming, ECOOP'11. Springer-Verlag, 2011. Google ScholarDigital Library
- T. Wrigstad, F. Z. Nardelli, S. Lebresne, J. Östlund, and J. Vitek. Integrating typed and untyped code in a scripting language. In phSymposium on Principles of Programming Languages, 2010. Google ScholarDigital Library
Index Terms
Design and evaluation of gradual typing for python
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 ...
Design and evaluation of gradual typing for python
DLS '14Combining static and dynamic typing within the same language offers clear benefits to programmers. It provides dynamic typing in situations that require rapid prototyping, heterogeneous data structures, and reflection, while supporting static typing ...
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