Date: Wed 01 Sep
Time: 15.00
Place: Aula 214

Speaker: Eugenio Moggi
Title: Monadic Encapsulation of Effects: a Revised Approach

Abstract. Launchbury and Peyton-Jones came up with an ingenious idea for embedding regions of imperative programming in a pure functional language like Haskell. The key idea was based on a simple modification of Hindley-Milner's type system. Our first contribution is to propose a more natural encapsulation construct exploiting higher-order kinds, which achieves the same encapsulation effect, but avoids the "bogus" type parameter of the original proposal. The second contribution is a stronger type safety result, namely encapsulation of strict state in higher-order lambda-calculus. We formalise the intended implementation as a very simple big-step operational semantics on untyped terms, which captures interesting implementation details not captured by the reduction semantics proposed previously. (Joint work with F.Palumbo).

Speaker: Eugenio Moggi
Title: Monads, Shapely Functors and Traversals

Abstract. We demonstrates the potential for combining the polytypic and monadic programming styles, by introducing a new kind of combinator, called a traversal. The natural setting for defining traversals is the class of shapely data types. This result reinforces the view that shapely data types form a natural domain for polytypism: they include most of the data types of interest, while to exceed them would sacrifice a very smooth interaction between polytypic and monadic programming. (Joint work with G.Belle' and B.Jay).