18/09/2008 Francois Pottier (INRIA)

Pas vu pas pris – ou comment passer vos effets de bord sous silence.

La logique de séparation repose sur deux formes duales de modularité: le "raisonnement local" rend une partie de l'état invisible à l'intérieur d'une certaine portée statique, tandis que "l'état caché" rend au contraire une partie de l'état invisible à l'extérieur d'une portée statique. Dans la littérature récente, ces idiomes sont tous deux expliqués en termes d'une règle d'encadrement d'ordre supérieur ("higher-order frame rule"). J'argumenterai pourquoi cette explication de "l'état caché" impose un style par passage de continuations (CPS), et n'est pas satisfaisante en pratique. Pour résoudre ce problème, je propose une règle d'anti-encadrement d'ordre supérieur ("higher-order anti-frame rule"), qui permet de cacher un état local en style direct. Techniquement, je présenterai cette règle non pas dans le cadre de la logique de séparation, mais dans le cadre d'un système de types à capacités pour ML, développé par Arthur Charguéraud et moi-même. Afin d'illustrer l'emploi et l'expressivité de la règle, j'expliquerai comment elle permet de coder les références "non contrôlées" de ML ainsi que les suspensions ("lazy thunks").