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 \({{\,\mathrm{\textbf{new}}\,}}\) and \({{\,\mathrm{\textbf{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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Linear Effects, Exceptions, and Resource Safety

  • Sidney Congard,
  • Guillaume Munch-Maccagnoni,
  • Rémi Douence

摘要

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 \({{\,\mathrm{\textbf{new}}\,}}\) and \({{\,\mathrm{\textbf{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.