Relational nullable types with Boolean unification

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avisKonferenceartikelForskningpeer review

40 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.

OriginalsprogEngelsk
Artikelnummer110
TidsskriftProceedings of the ACM on Programming Languages
Vol/bind5
NummerOOPSLA
Sider (fra-til)1-28
Antal sider28
ISSN2475-1421
DOI
StatusUdgivet - okt. 2021
BegivenhedSPLASH 2021 - Chicago, USA
Varighed: 17 okt. 202122 nov. 2021
https://2021.splashcon.org/

Konference

KonferenceSPLASH 2021
Land/OmrådeUSA
ByChicago
Periode17/10/202122/11/2021
Internetadresse

Fingeraftryk

Dyk ned i forskningsemnerne om 'Relational nullable types with Boolean unification'. Sammen danner de et unikt fingeraftryk.

Citationsformater