Nothing Special   »   [go: up one dir, main page]
Document Open Access Logo

Scala with Explicit Nulls

Authors Abel Nieto , Yaoyu Zhao, Ondřej Lhoták , Angela Chang, Justin Pu

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.25.pdf
  • Filesize: 0.73 MB
  • 26 pages

Document Identifiers

Author Details

Abel Nieto
  • University of Waterloo, Canada
Yaoyu Zhao
  • University of Waterloo, Canada
Ondřej Lhoták
  • University of Waterloo, Canada
Angela Chang
  • University of Waterloo, Canada
Justin Pu
  • University of Waterloo, Canada

Funding

This research was supported by the Natural Sciences and Engineering Research Council of Canada and by the Waterloo-Huawei Joint Innovation Lab.

Acknowledgements

We would like to thank Sébastien Doeraene, Fengyun Liu, Guillaume Martres, and Martin Odersky for their feedback on our explicit nulls design.

Cite AsGet BibTex

Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. Scala with Explicit Nulls. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 25:1-25:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.25

Abstract

The Scala programming language makes all reference types implicitly nullable. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors. In this paper, we present a modification to the Scala type system that makes nullability explicit in the types. Specifically, we make reference types non-nullable by default, while still allowing for nullable types via union types. We have implemented this design for explicit nulls as a fork of the Dotty (Scala 3) compiler. We evaluate our scheme by migrating a number of Scala libraries to use explicit nulls. Finally, we give a denotational semantics of type nullification, the interoperability layer between Java and Scala with explicit nulls. We show a soundness theorem stating that, for variants of System F_ω that model Java and Scala, nullification preserves values of types.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Theory of computation → Denotational semantics
  • Theory of computation → Type theory
  • Software and its engineering → Interoperability
Keywords
  • Scala
  • Java
  • nullability
  • language interoperability
  • type systems

Metrics

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

Supplementary Materials

References

  1. Edward Aftandilian, Raluca Sauciuc, Siddharth Priya, and Sundaresan Krishnan. Building Useful Program Analysis Tools Using an Extensible Java Compiler. In 2012 IEEE 12th International Working Conference on Source Code Analysis and Manipulation, pages 14-23. IEEE, 2012. Google Scholar
  2. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 249-272, 2016. Google Scholar
  3. Nada Amin and Ross Tate. Java and Scala’s Type Systems are Unsound: The Existential Crisis of Null Pointers. In Eelco Visser and Yannis Smaragdakis, editors, Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pages 838-848. ACM, 2016. URL: https://doi.org/10.1145/2983990.2984004.
  4. Apple Inc. About swift. [Online; accessed 5-November-2019]. URL: https://docs.swift.org/swift-book/.
  5. Apple Inc. Swift language guide. [Online; accessed 5-November-2019]. URL: https://docs.swift.org/swift-book/LanguageGuide/TheBasics.html.
  6. Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. Nullaway: Practical Type-Based Null Safety for Java. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 740-750. ACM, 2019. Google Scholar
  7. Dan Brotherston, Werner Dietl, and Ondřej Lhoták. Granullar: Gradual Nullable Types for Java. In Proceedings of the 26th International Conference on Compiler Construction, pages 87-97. ACM, 2017. Google Scholar
  8. Kim B Bruce, Albert R Meyer, and John C Mitchell. The Semantics of Second-Order Lambda Calculus. Information and Computation, 85(1):76-134, 1990. Google Scholar
  9. Werner Dietl, Stephanie Dietzel, Michael D Ernst, Kivanç Muşlu, and Todd W Schiller. Building and Using Pluggable Type-Checkers. In Proceedings of the 33rd International Conference on Software Engineering, pages 681-690. ACM, 2011. Google Scholar
  10. Manuel Fähndrich and K. Rustan M. Leino. Declaring and Checking Non-Null Types in an Object-Oriented Language. In Ron Crocker and Guy L. Steele Jr., editors, Proceedings of the 2003 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2003, October 26-30, 2003, Anaheim, CA, USA, pages 302-312. ACM, 2003. URL: https://doi.org/10.1145/949305.949332.
  11. Manuel Fähndrich and Songtao Xia. Establishing Object Invariants with Delayed Types. In Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr., editors, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pages 337-350. ACM, 2007. URL: https://doi.org/10.1145/1297027.1297052.
  12. Gavin King. The Ceylon Language. [Online; accessed 30-May-2020]. URL: https://ceylon-lang.org/.
  13. Gavin King. Using Java From Ceylon. [Online; accessed 30-May-2020]. URL: https://ceylon-lang.org/documentation/1.2/reference/interoperability/java-from-ceylon/.
  14. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  15. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. Typing Local Control and State Using Flow Analysis. In European Symposium on Programming, pages 256-275. Springer, 2011. Google Scholar
  16. 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):396-450, 2001. Google Scholar
  17. Kotlin Foundation. Kotlin programming language. [Online; accessed 5-November-2019]. URL: https://kotlinlang.org/.
  18. Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. The Java virtual machine specification. Pearson Education, 2014. Google Scholar
  19. Fengyun Liu, Aggelos Biboudis, and Martin Odersky. Initialization Patterns in Dotty. In Proceedings of the 9th ACM SIGPLAN International Symposium on Scala, pages 51-55. ACM, 2018. Google Scholar
  20. John C Mitchell. Foundations for Programming Languages, volume 1. MIT press Cambridge, 1996. Google Scholar
  21. MITRE. 2019 CWE Top 25 Most Dangerous Software Errors. [Online; accessed 17-November-2019]. URL: https://cwe.mitre.org/top25/archive/2019/2019_cwe_top25.html.
  22. Abel Nieto Rodriguez. Scala with explicit nulls. Master’s thesis, University of Waterloo, 2019. Google Scholar
  23. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical Pluggable Types for Java. In Proceedings of the 2008 international symposium on Software testing and analysis, pages 201-212. ACM, 2008. Google Scholar
  24. Xin Qi and Andrew C. Myers. Masked Types for Sound Object Initialization. In Zhong Shao and Benjamin C. Pierce, editors, Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 53-65. ACM, 2009. URL: https://doi.org/10.1145/1480881.1480890.
  25. Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. A simple soundness proof for dependent object types. PACMPL, 1(OOPSLA):46:1-46:27, 2017. Google Scholar
  26. John C Reynolds. Towards a Theory of Type Structure. In Programming Symposium, pages 408-425. Springer, 1974. Google Scholar
  27. Tiark Rompf and Nada Amin. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pages 624-641, 2016. Google Scholar
  28. Jeremy G Siek and Walid Taha. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop, volume 6, pages 81-92, 2006. Google Scholar
  29. Alexander J. Summers and Peter Müller. Freedom Before Commitment: a Lightweight Type System for Object Initialisation. In Cristina Videira Lopes and Kathleen Fisher, editors, Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011, pages 1013-1032. ACM, 2011. URL: https://doi.org/10.1145/2048066.2048142.
  30. Philip Wadler. Monads for Functional Programming. In International School on Advanced Functional Programming, pages 24-52. Springer, 1995. Google Scholar
  31. Yoav Zibin, David Cunningham, Igor Peshansky, and Vijay Saraswat. Object Initialization in X10. In European Conference on Object-Oriented Programming, pages 207-231. Springer, 2012. Google Scholar
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