A BRICS Mini-Course
October 24 and 27, 1997
Lectures by
Andrzej Filinski
LFCS (Laboratory for Foundations of Computer Science), University of Edinburgh, Scotland, UK
Over the last few years, the theory and practice of functional programming have been significantly influenced by the concept of computational monads. Perhaps most importantly, monads provide a uniform mathematical framework for defining the semantics of ``computational effects'' such as mutable state or exceptions in ML-like languages. Equally notable, monads can be used as a convenient structuring technique for expressing imperative concepts in purely functional languages such as Haskell. So far, however, these two application areas have seen little overlap; the main goal of this mini-course is therefore to explore some consequences of a cross-fertilisation.
The course will start with a general introduction to monads, their use in denotational semantics, and techniques for reasoning about languages defined in terms of monads. Most of these concepts and techniques generalise naturally to a more syntactic setting, allowing us to specify declaratively a wide range of new computational effects, such as nondeterministic choice, within a functional language itself. In particular, we will consider ``monadic reflection'', a generalisation of Wadler's monad comprehensions, which will allow us to write programs using the newly-defined effects, with the same conciseness and convenience as we expect from ``built-in'' effects in ML-like languages.
We will then see how a surprising semantic result-the existence of a ``universal'' monadic effect-allows us to uniformly implement monadic reflection in terms of two primitive effects: mutable state and first-class continuations, as found in Scheme or SML/NJ. This technique gives us the best of both worlds: uniform, declarative specifications of new computational effects, combined with the full programming environment and efficiency of an existing production-quality language implementation.
The course will be largely self-contained, requiring only familiarity with basic concepts of denotational semantics and a working knowledge of ML or Scheme.