Document Open Access Logo

Blame for Null

Authors Abel Nieto , Marianna Rapoport, Gregor Richards , Ondřej Lhoták

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.3.pdf
  • Filesize: 0.72 MB
  • 28 pages

Document Identifiers

Author Details

Abel Nieto
  • University of Waterloo, Canada
Marianna Rapoport
  • University of Waterloo, Canada
Gregor Richards
  • University of Waterloo, Canada
Ondřej Lhoták
  • 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 the anonymous reviewers for their valuable feedback.

Cite As Get BibTex

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for Null. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.3

Abstract

Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this paper, we show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, we introduce a calculus, λ_null, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of λ_null, we then create a second calculus, λ_null^s, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. Our main result is a theorem that states that nullability errors in λ_null^s can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. We summarize our result with the slogan explicitly nullable programs can't be blamed. All our results are formalized in the Coq proof assistant.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Theory of computation → Type theory
  • Software and its engineering → Interoperability
  • Theory of computation → Operational semantics
Keywords
  • nullability
  • type systems
  • blame calculus
  • gradual typing

Metrics

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

Supplementary Materials

References

  1. Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for all. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 201-214. ACM, 2011. Google Scholar
  2. Brian Aydemir and Stephanie Weirich. LNgen: Tool support for locally nameless representations. Technical Report MS-CIS-10-24, Computer and Information Science, University of Pennsylvania, 2010. Google Scholar
  3. 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
  4. 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
  5. Arthur Charguéraud. The locally nameless representation. Journal of automated reasoning, 49(3):363-408, 2012. Google Scholar
  6. Microsoft Corporation. Nullable reference types. [Online; accessed 5-November-2019]. URL: https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references.
  7. 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
  8. Dotty Team. Explicit nulls. [Online; accessed 9-January-2020]. URL: https://dotty.epfl.ch/docs/reference/other-new-features/explicit-nulls.html.
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 48-59. ACM, 2002. Google Scholar
  12. 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
  13. Apple Inc. Swift language guide. [Online; accessed 5-November-2019]. URL: https://docs.swift.org/swift-book/LanguageGuide/TheBasics.html.
  14. JetBrains. Calling Java code from Kotlin. [Online; accessed 9-January-2020]. URL: https://kotlinlang.org/docs/reference/java-interop.html.
  15. JetBrains. Kotlin programming language. [Online; accessed 5-November-2019]. URL: https://kotlinlang.org/.
  16. JetBrains. Null safety. [Online; accessed 5-November-2019]. URL: https://kotlinlang.org/docs/reference/null-safety.html.
  17. Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811-1841, 1994. Google Scholar
  18. Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348-375, 1978. Google Scholar
  19. Daniel Patterson and Amal Ahmed. Linking types for multi-language software: Have your cake and eat it too. In Benjamin S. Lerner, Rastislav Bodík, and Shriram Krishnamurthi, editors, 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, volume 71 of LIPIcs, pages 12:1-12:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  20. 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. Google Scholar
  21. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strnisa. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20(1):71-122, 2010. Google Scholar
  22. 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
  23. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA, volume 32 of LIPIcs, pages 274-293. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  24. 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. Google Scholar
  25. Sam Tobin-Hochstadt and Matthias Felleisen. Interlanguage migration: from scripts to programs. In OOPSLA Companion, pages 964-974. ACM, 2006. Google Scholar
  26. Philip Wadler. A complement to blame. In Thomas Ball, Rastislav Bodík, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA, volume 32 of LIPIcs, pages 309-320. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  27. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 1-16. Springer, 2009. Google Scholar
  28. Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Commun. ACM, 9(6):413-432, 1966. Google Scholar
  29. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. Google Scholar
  30. 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 About DROPS Imprint Privacy Contact