Skip to Main content Skip to Navigation
New interface
Conference papers

Unboxing Mutually Recursive Type Definitions in OCaml

Simon Colin 1 Rodolphe Lepigre 2 Gabriel Scherer 3 
2 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
3 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Scherer Gabriel Connect in order to contact the contributor
Submitted on : Wednesday, November 21, 2018 - 11:33:13 AM
Last modification on : Wednesday, February 2, 2022 - 3:55:15 PM
Long-term archiving on: : Friday, February 22, 2019 - 1:32:31 PM


Files produced by the author(s)


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


Simon Colin, Rodolphe Lepigre, Gabriel Scherer. Unboxing Mutually Recursive Type Definitions in OCaml. JFLA 2019 - 30 èmes journées francophones des langages applicatifs, Jan 2019, Les Rousses, France. ⟨hal-01929508⟩



Record views


Files downloads