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.