Relational nullable types with Boolean unification

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference articleResearchpeer-review

41 Downloads (Pure)

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 languageEnglish
Article number110
JournalProceedings of the ACM on Programming Languages
Volume5
IssueOOPSLA
Pages (from-to)1-28
Number of pages28
ISSN2475-1421
DOIs
Publication statusPublished - Oct 2021
EventSPLASH 2021 - Chicago, United States
Duration: 17 Oct 202122 Nov 2021
https://2021.splashcon.org/

Conference

ConferenceSPLASH 2021
Country/TerritoryUnited States
CityChicago
Period17/10/202122/11/2021
Internet address

Keywords

  • Algorithm W
  • Boolean unification
  • choose construct
  • relational nullable type system
  • relational pattern matching
  • successive variable elimination algorithm
  • type inference

Fingerprint

Dive into the research topics of 'Relational nullable types with Boolean unification'. Together they form a unique fingerprint.

Cite this