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
VENDREDI 17 juin, 15h00
-----------
Ohad Kammar
-----------
University of Oxford
=================================================================
No value restriction is needed for algebraic effects and handlers
=================================================================
We present a straightforward, sound Hindley-Milner polymorphic type
system for algebraic effects and handlers in a call-by-value
calculus, which allows type variable generalisation of arbitrary
computations, not just values. This result is surprising. On the
one hand, the soundness of unrestricted call-by-value Hindley-Milner
polymorphism is known to fail in the presence of computational
effects such as reference cells and continuations. On the other
hand, many programming examples can be recast to use effect handlers
instead of these effects. Analysing the expressive power of effect
handlers with respect to state effects, we claim handlers cannot
express reference cells, and show they can simulate dynamically
scoped state. Time permitting, we will discuss the denotational
soundness theorem that led to this work.
Joint work with Sean Moss and Matija Pretnar.