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.
| Original language | English |
|---|---|
| Article number | 110 |
| Journal | Proceedings of the ACM on Programming Languages |
| Volume | 5 |
| Issue | OOPSLA |
| Pages (from-to) | 1-28 |
| Number of pages | 28 |
| ISSN | 2475-1421 |
| DOIs | |
| Publication status | Published - Oct 2021 |
| Event | SPLASH 2021 - Chicago, United States Duration: 17 Oct 2021 → 22 Nov 2021 https://2021.splashcon.org/ |
Conference
| Conference | SPLASH 2021 |
|---|---|
| Country/Territory | United States |
| City | Chicago |
| Period | 17/10/2021 → 22/11/2021 |
| Internet address |
Keywords
- Algorithm W
- Boolean unification
- choose construct
- relational nullable type system
- relational pattern matching
- successive variable elimination algorithm
- type inference