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

TL;DR

This work investigates how to combine linearity, effects, and exceptions by modeling resources with an allocation monad and studying two calculi: an ordered, linear call-by-push-value language with new/delete, and an affine ordered extension with destructors and exceptions, incorporating a move operation to allow non-LIFO resource release. The authors develop a presheaf/categorical semantics around destructors via the slice category $\mathscr{C}_{/TI}$ and show resource-safety theorems: ordered programs release resources exactly once in reverse allocation order, while the linear setting permits permutation of release, with translations/interpretations between the ordered and linear systems. A rich semantic model is provided, including a presheaf model based on $\mathsf{Set}^{\mathbf{[R]}}$ and Day convolution, where destructors arise from resource-modality structures, and central types are resource-free. The study connects these theories to practical resource management (à la C++/Rust) and proposes a principled pathway to integrate first-class resources with linear and ordered logics, suggesting avenues for future work on borrowing, mixed modalities, and extended Curry–Howard frameworks for resources.

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 call-by-push-value language with two allocation effects $\mathit{new}$ and $\mathit{delete}$. The resource-safety properties follow from the linear (and even ordered) character of the typing rules. We then explain how to integrate exceptions on top of linearity and effects by adjoining default destruction actions to types, as inspired by C++/Rust destructors. We see destructors as objects $δ: A\rightarrow TI$ in the slice category over $TI$. This construction gives rise to a second calculus, an affine ordered call-by-push-value language with exceptions and destructors, in which the weakening rule performs a side-effect. As in C++/Rust, a ``move'' operation is necessary to allow random-order release of resources, as opposed to last-in-first-out order. Moving resources is modelled as an exchange rule that performs a side-effect.

Figures (8)

• Figure 1: Typing rules for $\mathrel{\boldsymbol{\mathcal{L}}}$
• Figure 2: Reduction rules
• Figure 3: Stack typing rules
• Figure 4: Typing rules of ordered expressions with resources
• Figure 5: Typing rules of ordered stacks and commands

Theorems & Definitions (27)

• theorem 1
• lemma 1: Substitution lemma (SL)
• theorem 2: Subject reduction
• theorem 3: Progress
• proposition 1
• lemma 2
• lemma 3
• theorem 4
• proof
• theorem 5