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).