Theme: Subtyping and Computational Monads
If you can read this, your browser provides
insufficient support for style sheets. The visual
presentation of this document will suffer.
April 06 -September/Oktober 06
Prof. Dr. Gert Smolka
Computational effects, ranging from possible divergence (loops, recursion)
over I/O operations (read, write,file handling), control operators (jumps, exceptions,
continuations) and non-determinism to state, are the heart and soul of real programming
languages. Yet much of the theoretical results are stated for the "pure" programs
of lambda calculus, or add computational ffects in an ad-hoc manner. With
his seminal work on computational monads, Moggi presented an abstract framework
that captures a wide range of effectful computations uniformly. These ideas also had
a significant impact on programming practice; monadic types are the main structuring
device in the Haskell language.
Subtyping is a relation between the types of the system and allows to use values of
a subtype in any context expecting values of the supertype. The interaction of subtyping
and effects can be subtle, as seen for instance in the combination of subtyping and
state. Nevertheless, many object-oriented concepts rely on exactly this combination.
It is hoped that the investigation of subtyping in the framework of Moggi's computational
monads allows for a more direct transfer of theoretical results to practical
The thesis shall develop the basics of a theory of subtyping based
on Moggi's computational metalanguage. This involves the following tasks.
- The calculus of Moggi (1991) should be formulated using a small-step operational
semantics, ideally without any assumptions about a particular evaluation order.
The notion of (structural) subtyping from lambda calculus (Pierce 2002) shall be
extended to the monadic types of Moggi's calculus, and a standard soundness
property (preservation and progress) be proved.
The next task will be to consider the problem of type checking for this calculus.
As usual, this requires the reformulation to an "algorithmic" inference system to
derive minimum types.
In a third phase we want to investigate whether the combination of subtyping
and computational monads can be extended to the polymorphic types of secondorder
lambda calculus (System F&le). It is likely that a restriction of System F&le is
required to obtain type soundness. A well-known example is the value restriction
in ML's Hindley-Milner polymorphism. This problem is somewhat orthogonal to
subtyping, see Wright (1995) for discussion.
- Nick Benton & John Hughes & Eugenio Moggi. Monads and effects. Pages 42-122 of
Advanced lectures from int. summer school on applied semantics. LNCS vol. 2395, Springer,
- Eugenio Moggi. Notions of computation and monads. Information and Computation, 93,
- Benjamin Pierce. Types and Programming Languages. MIT Press, 2002.
- Pierre-Louis Curien & Giorgio Ghelli. Coherence of subsumption, minimum subtyping and
type-checking F&le. Mathematical structures in computer science, 2, 55-91, 1992.
- Phil Wadler. The essence of functional programming. Proc. 19'th symposium on principles
of programming languages. ACM Press, 1992.
- Andrew Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Infor-
mation and Computation, 115(1), 38-94, 1994.
- Andrew Wright. Simple Imperative Polymorphism. LISP and Symbolic Computation, 8(4),
The slides from my introductory talk
The thesis paper,
Effectful Computation in Moggi's Calculus with Records and Subtyping,
is also available here.