iBet uBet web content aggregator. Adding the entire web to your favor.

Link to original content: https://doi.org/10.1145/3485487

Relational nullable types with Boolean unification | Proceedings of the ACM on Programming Languages

research-article

Open access

Relational nullable types with Boolean unification

Authors:

Jaco van de PolAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue OOPSLA

Article No.: 110, Pages 1 - 28

https://doi.org/10.1145/3485487

Published: 15 October 2021 Publication History

Abstract

We present a simple, practical, and expressive relational nullable type system. A relational nullable type system captures whether an expression may evaluate to null based on its type, but also based on the type of other related expressions. The type system extends the Hindley-Milner type system with Boolean constraints, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support full Hindley-Milner style type inference with an extension of Algorithm W.

We conduct a preliminary study of open source projects showing that there is a need for relational nullable type systems across a wide range of programming languages. The most important findings from the study are: (i) programmers use programming patterns where the nullability of one expression depends on the nullability of other related expressions, (ii) such invariants are commonly enforced with run-time exceptions, and (iii) reasoning about these programming patterns requires not only knowledge of when an expression may evaluate to null, but also when it may evaluate to a non-null value. We incorporate these observations in the design of the proposed relational nullable type system.

Supplementary Material

Auxiliary Presentation Video (oopsla21main-p47-p-video.mp4)

This is a presentation of the work Relational Nullable Types with Boolean Unification by Magnus Madsen and Jaco van de Pol.

Download
86.18 MB

References

[1]

Nada Amin and Ross Tate. 2016. Java and Scala’s Type Systems are Unsound: the Existential Crisis of Null Pointers. Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).

Digital Library

[2]

Franz Baader. 1998. On the Complexity of Boolean Unification. Inform. Process. Lett.

Digital Library

[3]

Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. 2019. Nullaway: Practical Type-based Null Safety for Java. In Proc. Joint Symposium on European Software Engineering and the Foundations of Software Engineering (ESEC/FSE).

Digital Library

[4]

George Boole. 1847. The mathematical analysis of logic.

[5]

Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauß. 1989. Unification in Boolean Rings and Abelian Groups. Journal of Symbolic Computation.

Digital Library

[6]

Dan Brotherston, Werner Dietl, and Ondřej Lhoták. 2017. Granullar: Gradual Nullable Types for Java. In Proc. International Conference on Compiler Construction (CC).

Digital Library

[7]

Wolfram Buttner and Helmut Simonis. 1987. Embedding Boolean Expressions into Logic Programming. Journal of Symbolic Computation.

Digital Library

[8]

Patrice Chalin and Perry R James. 2007. Non-Null References by Default in Java: Alleviating the Nullity Annotation Burden. In Proc. European Conference on Object-Oriented Programming (ECOOP).

Digital Library

[9]

Olaf Chitil. 2001. Compositional explanation of types and algorithmic debugging of type errors. In Proc. International Conference on Functional Programming (ICFP).

Digital Library

[10]

Luis Damas. 1984. Type Assignment in Programming Languages. Ph. D. Dissertation. The University of Edinburgh.

[11]

Manuel Fähndrich and K Rustan M Leino. 2003. Declaring and Checking Non-Null Types in an Object-Oriented Language. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).

Digital Library

[12]

Manuel Fähndrich and Songtao Xia. 2007. Establishing Object Invariants with Delayed Types. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).

Digital Library

[13]

Roger Hindley. 1969. The Principal Type-scheme of an Object in Combinatory Logic. Transactions of the American Mathematical Society (AMS).

[14]

Laurent Hubert, Thomas Jensen, and David Pichardie. 2008. Semantic Foundations and Inference of Non-Null Annotations. In International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS).

Digital Library

[15]

Mark P Jones. 2003. Qualified Types: Theory and Practice. Cambridge University Press.

Digital Library

[16]

Leopold Löwenheim. 1908. Über das Auflösungsproblem im logischen Klassenkalkul.

[17]

Magnus Madsen and Ondřej Lhoták. 2018. Safe and Sound Program Analysis with Flix. In Proc. International Symposium on Software Testing and Analysis (ISSTA).

Digital Library

[18]

Magnus Madsen and Ondřej Lhoták. 2020. Fixpoints for the Masses: Programming with first-class Datalog Constraints. Proc. of the ACM on Programming Languages, 4, OOPSLA (2020).

Digital Library

[19]

Magnus Madsen and Jaco van de Pol. 2020. Polymorphic Types and Effects with Boolean Unification. Proc. of the ACM on Programming Languages, 4, OOPSLA (2020).

Digital Library

[20]

Magnus Madsen, Ming-Ho Yee, and Ondrej Lhoták. 2016. From Datalog to Flix: A Declarative Language for Fixed Points on Lattices. In Proc. Programming Language Design and Implementation (PLDI).

Digital Library

[21]

Chris Male, David J Pearce, Alex Potanin, and Constantine Dymnikov. 2008. Java Bytecode Verification for NonNull Types. In Proc. International Conference on Compiler Construction (CC).

Digital Library

[22]

Alberto Martelli and Ugo Montanari. 1982. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS).

Digital Library

[23]

Urusula Martin and Tobias Nipkow. 1989. Boolean Unification - The Story So Far. Journal of Symbolic Computation.

Digital Library

[24]

Robin Milner. 1978. A Theory of Type Polymorphism in Programming. J. Comput. System Sci.

[25]

Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. 2020. Blame for Null. In Proc. European Conference on Object-Oriented Programming (ECOOP 2020).

[26]

Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, and Justin Pu. 2020. Scala with Explicit Nulls. In Proc. European Conference on Object-Oriented Programming (ECOOP 2020).

[27]

Benjamin C Pierce and David N Turner. 2000. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS).

Digital Library

[28]

Xin Qi and Andrew C Myers. 2009. Masked Types for Sound Object Initialization. In Proc. Principles of Programming Languages (POPL).

Digital Library

[29]

Patrick M Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types. In Proc. Programming Language Design and Implementation (PLDI).

Digital Library

[30]

Sergiu Rudeanu. 1974. Boolean Functions and Equations.

[31]

Fausto Spoto. 2008. Nullness Analysis in Boolean Form. In Proc. International Conference on Software Engineering and Formal Methods (SEFM).

Digital Library

[32]

Alexander J Summers and Peter Müller. 2011. Freedom Before Commitment: A Lightweight Type System for Object Initialisation. In Proc. Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).

Digital Library

[33]

Sam Tobin-Hochstadt and Matthias Felleisen. 2010. Logical types for untyped languages. In Proc. International Conference on Functional Programming (ICFP).

Digital Library

[34]

Mads Tofte and Jean-Pierre Talpin. 1997. Region-based Memory Management. Information and Computation.

Digital Library

[35]

Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. In Proc. International Conference on Functional Programming (ICFP).

Digital Library

[36]

Philip Wadler and Stephen Blott. 1989. How to make ad-hoc polymorphism less ad hoc. In Proc. Symposium on Principles of Programming Languages (POPL).

Digital Library

[37]

Andrew K Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation.

Digital Library

Cited By

Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Madsen Mvan de Pol JHenriksen T(2023)Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect SystemsProceedings of the ACM on Programming Languages10.1145/36228167:OOPSLA2(516-543)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622816
Lutze MMadsen MSchuster PBrachthäuser J(2023)With or Without You: Programming with Effect ExclusionProceedings of the ACM on Programming Languages10.1145/36078467:ICFP(448-475)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607846

Index Terms

Relational nullable types with Boolean unification
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Polymorphic types and effects with Boolean unification

We present a simple, practical, and expressive type and effect system based on Boolean constraints. The effect system extends the Hindley-Milner type system, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We ...
Boxy types: inference for higher-rank types and impredicativity
ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming

Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the ...
Gradual typing with unification-based inference
DLS '08: Proceedings of the 2008 symposium on Dynamic languages

Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence ...

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue OOPSLA

October 2021

2001 pages

EISSN:2475-1421

DOI:10.1145/3492349

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 October 2021

Published in PACMPL Volume 5, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
517
Total Downloads

Downloads (Last 12 months)211
Downloads (Last 6 weeks)67

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Madsen Mvan de Pol JHenriksen T(2023)Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect SystemsProceedings of the ACM on Programming Languages10.1145/36228167:OOPSLA2(516-543)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622816
Lutze MMadsen MSchuster PBrachthäuser J(2023)With or Without You: Programming with Effect ExclusionProceedings of the ACM on Programming Languages10.1145/36078467:ICFP(448-475)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607846

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents