Efficient Deconstruction with Typed Pointer Reversal (abstract)

Guillaume Munch-Maccagnoni (1, 2) , Rémi Douence (1, 3)

1 LS2N - équipe GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
2 LS2N - Laboratoire des Sciences du Numérique de Nantes
3 IMT Atlantique - IMT Atlantique

The resource-management model of C++ and Rust relies on compiler-generated destructors called predictably and reliably. In current implementations, the generated destructor consumes stack space proportionally to the depth of the structure it destructs. We describe a way to derive destructors for algebraic data types that consume a constant amount of stack and heap. We discuss applicability to C++ and Rust, and also some implication for anyone wishing to extend an ML-style language with first-class resources.

Domaines: Langage de programmation [cs.PL]; Logique en informatique [cs.LO]

Guillaume Munch-Maccagnoni, Rémi Douence. Efficient Deconstruction with Typed Pointer Reversal (abstract). ML 2019 Workshop, KC Sivaramakrishnan, Aug 2019, Berlin, Germany. ⟨hal-02177326v1⟩