Fabian Muehlboeck
Ross Tate
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Recent research has identified significant performance hurdles that sound gradual typing needs to overcome. These performance hurdles stem from the fact that the run-time checks gradual type systems insert into code can cause significant overhead. We propose that designing a type system for a gradually typed language hand in hand with its implementation from scratch is a possible way around these and several other hurdles on the way to efficient sound gradual typing. Such a design process also highlights the type-system restrictions required for efficient composition with gradual typing. We formalize the core of a nominal object-oriented language that fulfills a variety of desirable properties for gradually typed languages, and present evidence that an implementation of this language suffers minimal overhead even in adversarial benchmarks identified in earlier work.
Supplemental Material
Available for Download
- Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All . In POPL 2011. ACM, New York, NY, USA, 201–214. Google Scholar
Digital Library
- Wonsun Ahn, Jiho Choi, Thomas Shull, María J. Garzarán, and Josep Torrellas. 2014. Improving JavaScript Performance by Deconstructing the Type System . In PLDI 2014. ACM, New York, NY, USA, 496–507. Google ScholarDigital Library
- Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. 2014. Gradual Typing for Smalltalk . Science of Computer Programming 96 (2014), 52 – 69. Special issue on Advances in Smalltalk based Systems. Google ScholarDigital Library
- Esteban Allende, Johan Fabry, and Éric Tanter. 2013. Cast Insertion Strategies for Gradually-Typed Objects . In DLS 2013. ACM, New York, NY, USA, 27–36. Google ScholarDigital Library
- Nada Amin and Ross Tate. 2016. Java and Scala’s Type Systems are Unsound: The Existential Crisis of Null Pointers . In OOPSLA 2016. ACM, New York, NY, USA, 838–848. Google ScholarDigital Library
- Christopher Anderson and Sophia Drossopoulou. 2003. BabyJ: From Object Based to Class Based Programming via Types . In WOOD 2003. Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 53 – 81. Google ScholarCross Ref
- Gavin Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding Dynamic Types to C# . In ECOOP 2010. Springer Berlin Heidelberg, Berlin, Heidelberg, 76–100. Google ScholarCross Ref
- Gilad Bracha. 2004. Pluggable Type Systems . (2004). In Workshop on Revival of Dynamic Languages.Google Scholar
- Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems . In POPL 2016. ACM, New York, NY, USA, 443–455. Google ScholarDigital Library
- Alan Demers, Mark Weiser, Barry Hayes, Hans Boehm, Daniel Bobrow, and Scott Shenker. 1990. Combining Generational and Conservative Garbage Collection: Framework and Implementations . In POPL 1990. ACM, New York, NY, USA, 261–269. Google ScholarDigital Library
- L. Peter Deutsch and Allan M. Schiffman. 1984. Efficient Implementation of the Smalltalk-80 System . In POPL 1984. ACM, New York, NY, USA, 297–302. Google ScholarDigital Library
- Facebook, Inc. 2016. The Hack Language Specification, Version 1.1 . (April 2016).Google Scholar
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions . In ICFP 2002. ACM, New York, NY, USA, 48–59. Google ScholarDigital Library
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing . In POPL 2016. ACM, New York, NY, USA, 429–442. Google ScholarDigital Library
- Ben Greenman, Fabian Muehlboeck, and Ross Tate. 2014. Getting F-Bounded Polymorphism into Shape . In PLDI 2014. ACM, New York, NY, USA, 89–99. Google ScholarDigital Library
- Radu Grigore. 2017. Java Generics are Turing Complete . In POPL 2017. ACM, New York, NY, USA, 73–85. Google ScholarDigital Library
- Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. 2006. SAGE: Hybrid Checking for Flexible Specifications . Scheme and Functional Programming Workshop 6 (2006), 93–104.Google Scholar
- Fritz Henglein. 1994. Dynamic Typing: Syntax and Proof Theory . Science of Computer Programming 22, 3 (1994), 197 – 230. Google ScholarDigital Library
- Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. 2001. Featherweight Java: A Minimal Core Calculus for Java and GJ . TOPLAS 23, 3 (May 2001), 396–450. Google ScholarDigital Library
- Lintaro Ina and Atsushi Igarashi. 2011. Gradual Typing for Generics . In OOPSLA 2011. ACM, New York, NY, USA, 609–624. Google ScholarDigital Library
- Andrew Kennedy and Benjamin C. Pierce. 2007. On Decidability of Nominal Subtyping with Variance . In FOOL/WOOD 2007. Microsoft Research, Cambridge, UK, 1–12.Google Scholar
- Jacob Matthews and Robert Bruce Findler. 2007. Operational Semantics for Multi-Language Programs . In POPL 2007. ACM, New York, NY, USA, 3–10. Google ScholarDigital Library
- Microsoft. 2012. TypeScript . (Oct. 2012).Google Scholar
- The Python Development Team. 2008. Python Benchmarks . https://hg.python.org/benchmarks/ . (Dec. 2008).Google Scholar
- Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. 2015. Safe & Efficient Gradual Typing for TypeScript . In POPL 2015. ACM, New York, NY, USA, 167–180. Google ScholarDigital Library
- Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. 2015. Concrete Types for TypeScript . In ECOOP 2015, Vol. 37. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 76–100.Google Scholar
- Michel Schinz. 2005. Compiling Scala for the Java Virtual Machine . Ph.D. Dissertation. EPFL.Google Scholar
- Jeremy Siek, Ronald Garcia, and Walid Taha. 2009. Exploring the Design Space of Higher-Order Casts . In ESOP 2009. Springer-Verlag, Berlin, Heidelberg, 17–31. Google ScholarDigital Library
- Jeremy Siek and Walid Taha. 2007. Gradual Typing for Objects . In ECOOP 2007. Springer-Verlag, Berlin, Heidelberg, 2–27. Google ScholarDigital Library
- Jeremy G Siek and Walid Taha. 2006. Gradual Typing for Functional Languages . Scheme and Functional Programming Workshop 6 (2006), 81–92.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing . In SNAPL 2015, Vol. 32. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 274–293.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, Sam Tobin-Hochstadt, and Ronald Garcia. 2015b. Monotonic References for Efficient Gradual Typing . In ESOP 2015. Springer Berlin Heidelberg, Berlin, Heidelberg, 432–456. Google ScholarDigital Library
- Jeremy G. Siek and Philip Wadler. 2010. Threesomes, with and without Blame . In POPL 2010. ACM, New York, NY, USA, 365–376. Google ScholarDigital Library
- Daniel Smith and Robert Cartwright. 2008. Java Type Inference is Broken: Can We Fix It? . In OOPSLA 2008. ACM, New York, NY, USA, 505–524. Google ScholarDigital Library
- Nikhil Swamy, Cedric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin Bierman. 2014. Gradual Typing Embedded Securely in JavaScript . In POPL 2014. ACM, New York, NY, USA, 425–437. Google ScholarDigital Library
- Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. 2016. Is Sound Gradual Typing Dead? . In POPL 2016. ACM, New York, NY, USA, 456–468. Google ScholarDigital Library
- Sam Tobin-Hochstadt and Matthias Felleisen. 2006. Interlanguage Migration: From Scripts to Programs . In OOPSLA 2006. ACM, New York, NY, USA, 964–974. Google ScholarDigital Library
- Matías Toro and Éric Tanter. 2017. A Gradual Interpretation of Union Types . In SAS 2017. Springer International Publishing, Cham, 382–404. Google ScholarCross Ref
- Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. 2014. Design and Evaluation of Gradual Typing for Python . In DLS 2014. ACM, New York, NY, USA, 45–56. Google ScholarDigital Library
- 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 POPL 2017. ACM, New York, NY, USA, 762–774. Google ScholarDigital Library
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed . In ESOP 2009. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–16. Google ScholarDigital Library
- Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. 2010. Integrating Typed and Untyped Code in a Scripting Language . In POPL 2010. ACM, New York, NY, USA, 377–388. Google ScholarDigital Library
Index Terms
- Sound gradual typing is nominally alive and well
Recommendations
Toward efficient gradual typing for structural types via coercions
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationGradual typing combines static and dynamic typing in the same program. Siek et al. (2015) describe five criteria for gradually typed languages, including type soundness and the gradual guarantee. A significant number of languages have been developed in ...
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 ...
Is sound gradual typing dead?
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesProgrammers have come to embrace dynamically-typed languages for prototyping and delivering large and complex systems. When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. In response, ...
Comments