Resource Polymorphism

Guillaume Munch-Maccagnoni 1, 2
1 GALLINETTE - GALLINETTE
LS2N - Laboratoire des Sciences du Numérique de Nantes, Inria Rennes – Bretagne Atlantique
Abstract : 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). In particular, it proposes to identify the types of GCed values with types with trivial destructor: from this definition it deduces a model in which GC is the default allocation mode, and where GCed values can be used without restriction both in owning and borrowing contexts. 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.
Type de document :
Pré-publication, Document de travail
2018
Liste complète des métadonnées

Littérature citée [67 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01724997
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : mercredi 7 mars 2018 - 13:01:35
Dernière modification le : jeudi 19 avril 2018 - 11:46:06
Document(s) archivé(s) le : vendredi 8 juin 2018 - 12:23:39

Fichier

ocaml-raii.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01724997, version 1

Collections

Citation

Guillaume Munch-Maccagnoni. Resource Polymorphism. 2018. 〈hal-01724997〉

Partager

Métriques

Consultations de la notice

2282

Téléchargements de fichiers

4836