Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors

TL;DR

This paper explores the integration of linearity, effects, and exceptions in programming language models, introducing calculi that ensure resource safety through destructors and resource-aware effects.

Contribution

It presents new linear effectful calculi with resource-safety properties, incorporating destructors inspired by C++/Rust and analyzing their impact on resource management.

Findings

Resource-safety properties are established for the calculi.

Destructors modeled as objects enable resource release in non-LIFO order.

A new calculus integrates exceptions, destructors, and linear effects.

Abstract

We analyse the problem of combining linearity, effects, and exceptions, in abstract models of programming languages, as the issue of providing some kind of strength for a monad $T(- \oplus E)$ in a linear setting. We consider in particular for $T$ the allocation monad, which we introduce to model and study resource-safety properties. We apply these results to a series of two linear effectful calculi for which we establish their resource-safety properties. The first calculus is a linear (optionally ordered) call-by-push-value language with two allocation effects $\mathbf{new}$ and $\mathbf{delete}$. The resource-safety properties follow from the linear and ordered character of the typing rules. We then integrate exceptions with linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects $\delta : A\rightarrow TI$ in the slice category over $TI$. This construction gives rise to a second calculus, the resource call-by-push-value, featuring exceptions and destructors, and whose weakening and exchange rules perform side-effects. It is therefore affine at the level of types but ordered at the level of derivations. As in C++ and Rust, a ``move'' operation -- the side-effecting exchange rule -- is necessary for releasing resources in random order, as opposed to LIFO order.