Theme: Subtyping and Computational Monads

Saarland University
Programming Systems
Dieter Brunotte

Bachelor Thesis

If you can read this, your browser provides insufficient support for style sheets. The visual presentation of this document will suffer.
Author: Dieter Brunotte
Time frame: April 06 -September/Oktober 06
Advisor: Jan Schwinghammer
Responsible Professor: 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 applications.

Task description

The thesis shall develop the basics of a theory of subtyping based on Moggi's computational metalanguage. This involves the following tasks.

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

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

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



The slides from my introductory talk (pdf, ppt).
The thesis paper, Effectful Computation in Moggi's Calculus with Records and Subtyping, is also available here.