Unboxing Mutually Recursive Type Definitions in OCaml

Abstract : In modern OCaml, single-argument datatype declarations (variants with a single con-structor, records with a single field) can sometimes be "unboxed". This means that their memory representation is the same as their single argument (omitting the variant or record constructor and an indirection), thus achieving better time and memory efficiency. However , in the case of generalized/guarded algebraic datatypes (GADTs), unboxing is not always possible due to a subtle assumption about the runtime representation of OCaml values. The current correctness check is incomplete, rejecting many valid definitions, in particular those involving mutually-recursive datatype declarations. In this paper, we explain the notion of separability as a semantic for the unboxing criterion, and propose a set of inference rules to check separability. From these inference rules, we derive a new implementation of the unboxing check that properly supports mutually-recursive definitions.
Type de document :
Communication dans un congrès
JFLA 2019, Jan 2019, Les Rousses, France
Liste complète des métadonnées

https://hal.inria.fr/hal-01929508
Contributeur : Scherer Gabriel <>
Soumis le : mercredi 21 novembre 2018 - 11:33:13
Dernière modification le : vendredi 23 novembre 2018 - 01:13:25

Fichier

1811.02300.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01929508, version 1
  • ARXIV : 1811.02300

Citation

Simon Colin, Rodolphe Lepigre, Gabriel Scherer. Unboxing Mutually Recursive Type Definitions in OCaml. JFLA 2019, Jan 2019, Les Rousses, France. 〈hal-01929508〉

Partager

Métriques

Consultations de la notice

64

Téléchargements de fichiers

5