20220202 - Déboîter les constructeurs

ATTENTION : coupure de son de 21'45 à 36'12 (mille excuses pour l'orateur)

Date : 02 février 2022 à 14h - IRILL (site Jussieu 15-16 101)

Orateur : Gabriel Scherer (Partout / Inria Saclay & LIX)

Titre : Déboîter les constructeurs

abstract :

Dans le langage OCaml, les constructeurs de types algébriques sont représentés par des pointeurs vers des blocs mémoire. Cette représentation uniforme a de nombreux avantage, mais les utilisateurs aimeraient parfois des représentations plus compactes.

Dans ce travail, en collaboration avec Nicolas Chataing et Stephen Dolan, nous étudions la possibilité de "déboîter" certains constructeurs -- si l'utilisateur le demande au moment de leur définition -- c'est-à-dire de ne pas les représenter en mémoire du tout. Dans certains cas, effacer les constructeurs introduirait des confusions entre valeurs différentes, et il faut donc rejeter la demande. Nous avons donc conçu une analyse statique pour détecter ces confusions; la question de la terminaison de cette analyse est intéressante.

type exemple_accepté = | Short of int [@unboxed] | Long of Gmp.t

type exemple_rejeté = | I of int [@unboxed] | B of bool [@unboxed]