Reference. Resource Polymorphism
We present a resource-management model for ML-style programming languages, designed to be compatible with the OCaml philosophy and runtime model. This is a proposal to extend the OCaml language with destructors, move semantics, and resource polymorphism, to improve its safety, efficiency, interoperability, and expressiveness. It builds on the ownership-and-borrowing models of systems programming languages (Cyclone, C++11, Rust) and on linear types in functional programming (Linear Lisp, Clean, Alms). It continues a synthesis of resources from systems programming and resources in linear logic initiated by Baker. It is a combination of many known and some new ideas. On the novel side, it highlights the good mathematical structure of Stroustrup’s “Resource acquisition is initialisation” (RAII) idiom for resource management based on destructors, a notion sometimes confused with finalizers, and builds on it a notion of resource polymorphism, inspired by polarisation in proof theory, that mixes C++‘s RAII and a tracing garbage collector (GC). The proposal targets a new spot in the design space, with an automatic and predictable resource-management model, at the same time based on lightweight and expressive language abstractions. It is backwards-compatible: current code is expected to run with the same performance, the new abstractions fully combine with the current ones, and it supports a resource-polymorphic extension of libraries. It does so with only a few additions to the runtime, and it integrates with the current GC implementation. It is also compatible with the upcoming multicore extension, and suggests that the Rust model for eliminating data-races applies. Interesting questions arise for a safe and practical type system, many of which have already been thoroughly investigated in the languages and prototypes Cyclone, Rust, and Alms.
Cite
Cited by (1)
Linear Effects, Exceptions, and Resource Safety: A Curry-Howard Correspondence for Destructors congard-2026-linear
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 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 and . 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 in the slice category over . 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.
Cites 68 works (4 here)
With notes (4)
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Formulae-as-types for an involutive negation munchmaccagnoni-2014-formulae
Call-By-Push-Value: A Functional/Imperative Synthesis levy-2003-callbypushvalue
Linear logic girard_linear_1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
External (64)
- Bounding data races in space and time (2018)
- RustBelt: securing the foundations of the rust programming language (2017)
- Linear Haskell: practical linearity in a higher-order polymorphic language (2017)
- Levity polymorphism (2017)
- ASAP: As Static As Possible memory management (2017)
- The Design and Formalization of Mezzo, a Permission-Based Programming Language (2016)
- Engineering the Servo Web Browser Engine Using Rust (2016)
- Effect-dependent transformations for concurrent programs (2016)
- Type Classes for Lightweight Substructural Types (2015)
- A brief introduction to C++'s model for type- and resource-safety (2015)
- C++ Core Guidelines (2015)
- Liveness-Based Garbage Collection (2014)
- A dissection of L (2014)
- Programming with permissions in Mezzo (2013)
- A linear type system for multicore programming in ATS (2013)
- Real World OCaml - Functional Programming for the Masses (2013)
- A mechanized semantics for C++ object construction and destruction, with applications to resource management (2012)
- Practical affine types (2011)
- Resource modalities in tensor logic (2010)
- Types are calling conventions (2009)
- CATEGORICAL SEMANTICS OF LINEAR LOGIC (2009)
- Quantified types in an imperative language (2006)
- Linear Regions Are All You Need (2006)
- Portable and high-level access to the stack with Continuation Marks (2006)
- Safe Programming with Pointers Through Stateful Views (2005)
- Substructural type systems (2005)
- CPS Transformation of Beta-Redexes ∗ (2005)
- A tail-recursive machine with stack inspection (2004)
- A unified theory of garbage collection (2004)
- External Uniqueness Is Unique Enough (2003)
- Cyclone: A Safe Dialect of C (2002)
- Adoption and focus: practical linear types for imperative programming (2002)
- Region-based memory management in cyclone (2002)
- A Proposal to Add Move Semantics Support to the C++ Language (2002)
- Exception Safety: Concepts and Techniques (2001)
- Linearly Used Continuations (2000)
- A Type System for Bounded Space and Functional In-Place Update (2000)
- Syntactic control of interference revisited (1999)
- Call-by-Push-Value: A Subsuming Paradigm (1999)
- Quasi-linear types (1999)
- Ownership types for flexible alias protection (1998)
- A Generalization of Jumps and Labels (1998)
- A region inference algorithm (1998)
- The Zipper (1997)
- A new deconstructive logic: linear logic (1997)
- Uniqueness typing for functional languages with graph rewriting semantics (1996)
- Towards Alias-Free Pointers (1996)
- Reference counting as a computational interpretation of linear logic (1996)
- Compiling with Types (1995)
- What is a Categorical Model of Intuitionistic Linear Logic? (1995)
- “Use-once” variables and linear objects: storage management, reflection and multi-threading (1995)
- Minimizing reference count updating with deferred and anchored pointers for functional data structures (1994)
- Linear logic and permutation stacks—the Forth shall be first (1994)
- Implementation of the typed call-by-value λ-calculus using a stack of regions (1994)
- The Design and Evolution of C (1994)
- Computational Interpretations of Linear Logic (1993)
- On the Unity of Logic (1993)
- A new constructive logic: classic logic (1991)
- The ZINC experiment : an economical implementation of the ML language (1990)
- A formulae-as-types notion of control (1990)
- Linear Types can Change the World! (1990)
- The Linear Abstract Machine (1988)
- Syntactic control of interference (1978)
- A Generalization of Jumps and Labels (Technical Report, UNIVAC) (1965)