Wed 01 Sep
Monadic Encapsulation of Effects: a Revised Approach
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
(Joint work with F.Palumbo).
Monads, Shapely Functors and Traversals
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).