Document Open Access Logo

KafKa: Gradual Typing for Objects

Authors Benjamin Chung, Paley Li, Francesco Zappa Nardelli, Jan Vitek

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.12.pdf
  • Filesize: 3.66 MB
  • 25 pages

Document Identifiers

Author Details

Benjamin Chung
  • Northeastern University, Boston, MA, USA
Paley Li
  • Northeastern University, Boston, MA, USA
Francesco Zappa Nardelli
  • INRIA, Paris, France
Jan Vitek
  • Northeastern University, Boston, MA, USA

Funding

This work funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement 695412), the NSF (award 1544542) and (award 1518844) as well as ONR (award 503353).

Cite AsGet BibTex

Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ECOOP.2018.12

Abstract

A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems embody fundamentally different ideas of what it means to be well-typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. We present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
Keywords
  • Gradual typing
  • object-orientation
  • language design
  • type systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, and Marcus Denker. Gradual typing for Smalltalk. Science of Computer Programming, 96, 2014. URL: http://dx.doi.org/10.1016/j.scico.2013.06.006.
  2. Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy Siek, and Sam Tobin-Hochstadt. Sound gradual typing: Only mostly dead. Proc. ACM Program. Lang., 1(OOPSLA), 2017. URL: http://dx.doi.org/10.1145/3133878.
  3. Gavin Bierman, Martin Abadi, and Mads Torgersen. Understanding TypeScript. In European Conference on Object-Oriented Programming (ECOOP), 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_11.
  4. Gavin M. Bierman, Erik Meijer, and Mads Torgersen. Adding dynamic types to C#. In European Conference on Object-Oriented Programming (ECOOP), 2010. URL: http://dx.doi.org/10.1007/978-3-642-14107-2_5.
  5. Bard Bloom, John Field, Nathaniel Nystrom, Johan Östlund, Gregor Richards, Rok Strnisa, Jan Vitek, and Tobias Wrigstad. Thorn: Robust, concurrent, extensible scripting on the JVM. In Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 2009. URL: http://dx.doi.org/10.1145/1639950.1640016.
  6. Gilad Bracha. Pluggable type systems. In OOPSLA 2004 Workshop on Revival of Dynamic Languages, 2004. URL: http://dx.doi.org/10.1145/1167473.1167479.
  7. Gilad Bracha and David Griswold. Strongtalk: Typechecking Smalltalk in a production environment. In Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 1993. URL: http://dx.doi.org/10.1145/165854.165893.
  8. Luca Cardelli. Amber. In LITP Spring School on Theoretical Computer Science, pages 21-47. Springer, 1985. Google Scholar
  9. Gilles Dubochet and Martin Odersky. Compiling structural types on the JVM: A comparison of reflective and generative techniques from Scala’s perspective. In Workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems (ICOOLPS), 2009. URL: http://dx.doi.org/10.1145/1565824.1565829.
  10. Robert Findler and Matthias Felleisen. Contracts for higher-order functions. In Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2002. URL: http://dx.doi.org/10.1145/581478.581484.
  11. Robert Bruce Findler, Matthew Flatt, and Matthias Felleisen. Semantic casts: Contracts and structural subtyping in a nominal world. In European Conference on Object-Oriented Programming (ECOOP), 2004. URL: http://dx.doi.org/https://doi.org/10.1007/978-3-540-24851-4_17.
  12. Ben Greenman and Matthias Felleisen. A spectrum of soundness and performance. Proc. ACM PL (ICFP), to appear, 2018. Google Scholar
  13. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst., 23(3), 2001. URL: http://dx.doi.org/10.1145/503502.503505.
  14. Timothy Jones and David J. Pearce. A mechanical soundness proof for subtyping over recursive types. In Workshop on Formal Techniques for Java-like Programs (FTfJP), 2016. URL: http://dx.doi.org/10.1145/2955811.2955812.
  15. Fabian Muehlboeck and Ross Tate. Sound gradual typing is nominally alive and well. Proc. ACM Program. Lang., 1(OOPSLA), 2017. URL: http://dx.doi.org/10.1145/3133880.
  16. Benjamin C. Pierce and David N. Turner. Local type inference. In Symposium on Principles of Programming Languages (POPL), 1998. URL: http://dx.doi.org/10.1145/345099.345100.
  17. Gregor Richards, Ellen Arteca, and Alexi Turcotte. The VM already knew that: Leveraging compile-time knowledge to optimize gradual typing. Proc. ACM Program. Lang., 1(OOPSLA), 2017. URL: http://dx.doi.org/10.1145/3133879.
  18. Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete types for TypeScript. In European Conference on Object-Oriented Programming (ECOOP), 2015. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.76.
  19. Jeremy Siek. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006. URL: http://ecee.colorado.edu/~siek/pubs/pubs/2006/siek06_gradual.pdf.
  20. Jeremy Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming (ECOOP), 2007. URL: http://dx.doi.org/10.1007/978-3-540-73589-2_2.
  21. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In Summit on Advances in Programming Languages (SNAPL), 2015. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.274.
  22. Asumu Takikawa, Daniel Feltey, Ben Greenman, Max New, Jan Vitek, and Matthias Felleisen. Is sound gradual typing dead? In Symposium on Principles of Programming Languages (POPL), 2016. URL: http://dx.doi.org/10.1145/2837614.2837630.
  23. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 2012. URL: http://dx.doi.org/10.1145/2398857.2384674.
  24. The Dart Team. Dart programming language specification, 2016. URL: http://dartlang.org.
  25. The Facebook Hack Team. Hack, 2016. URL: http://hacklang.org.
  26. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In Symposium on Dynamic languages (DLS), 2006. URL: http://dx.doi.org/10.1145/1176617.1176755.
  27. Sam Tobin-Hochstadt and Matthias Felleisen. The design and implementation of typed Scheme. In Symposium on Principles of Programming Languages (POPL), 2008. URL: http://dx.doi.org/10.1145/1328438.1328486.
  28. Michael Vitousek, Andrew Kent, Jeremy Siek, and Jim Baker. Design and evaluation of gradual typing for Python. In Symposium on Dynamic languages (DLS), 2014. URL: http://dx.doi.org/10.1145/2661088.2661101.
  29. Michael M. Vitousek, Cameron Swords, and Jeremy G. Siek. Big types in little runtime: Open-world soundness and collaborative blame for gradual type systems. In Symposium on Principles of Programming Languages (POPL), 2017. URL: http://dx.doi.org/10.1145/3009837.3009849.
  30. Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek. Integrating typed and untyped code in a scripting language. In Symposium on Principles of Programming Languages (POPL), 2010. URL: http://dx.doi.org/10.1145/1706299.1706343.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact