Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 28 janvier, 10h30 ----------- Simon Colin ----------- ===================================================== Unboxing Mutually Recursive Type Definitions in OCaml ===================================================== In modern OCaml, single-argument datatype declarations (variants with a single constructor, records with a single immutable field) can sometimes be "unboxed". This means that their memory representation is the same as their single argument, omitting an indirection through the variant or record constructor, thus achieving better 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 work, 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. This presentation will be given in JFLA format, so it should be a shorter talk than usual. This is joint work with Rodolphe Lepigre and Gabriel Scherer.