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

                             JEUDI 31 mars, 10h30

                                 -----------
                                 Sam Lindley
                                 -----------

                           University of Edinburgh

                  =========================================
                  Liberating effects with rows and handlers
                    (joint work with Daniel Hillerström)
                  =========================================

Algebraic effects and effect handlers provide a modular abstraction
for effectful programming. They support user-defined effects, as in
Haskell, in conjunction with direct-style effectul programming, as in
ML. They also present a structured interface to programming with
delimited continuations.

In order to be modular, it is natural for an effect system to support
extensible effects. Row polymorphism is a natural abstraction for
modelling extensibility at the level of types. We argue that the
abstraction required to implement extensible effects and their
handlers is exactly row polymorphism.

We use the Links functional web programming language as a platform to
substantiate this claim. Links is a natural starting point as it uses
row polymorphism for polymorphic variants, records, and its built-in
effect types. It also has infrastructure for manipulating
continuations. Through a small extension to Links we smoothly add
support for effect handlers, making essential use of rows in the
frontend and first-class continuations in the backend.

We demonstrate our implementation through a number of examples which
illustrate how rows and handlers support modularity and smooth
composition of effectful computations. We present a core calculus of
row-polymorphic effects and handlers based on a variant of A-normal
form used in the intermediate representation of Links. We give an
operational semantics for the calculus and a novel generalisation of
the CEK machine that implements the operational semantics, and prove
that the two coincide.