Theme: Subtyping and Computational Monads
Saarland University
Informatics
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
Context
Computational effects, ranging from possible divergence (loops, recursion)
over I/O operations (read, write,file handling), control operators (jumps, exceptions,
continuations) and nondeterminism 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 adhoc 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 objectoriented 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.
 The calculus of Moggi (1991) should be formulated using a smallstep 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 wellknown example is the value restriction
in ML's HindleyMilner polymorphism. This problem is somewhat orthogonal to
subtyping, see Wright (1995) for discussion.
References
 Nick Benton & John Hughes & Eugenio Moggi. Monads and effects. Pages 42122 of
Advanced lectures from int. summer school on applied semantics. LNCS vol. 2395, Springer,
2002.
 Eugenio Moggi. Notions of computation and monads. Information and Computation, 93,
5592, 1991.
 Benjamin Pierce. Types and Programming Languages. MIT Press, 2002.
 PierreLouis Curien & Giorgio Ghelli. Coherence of subsumption, minimum subtyping and
typechecking F_{&le}. Mathematical structures in computer science, 2, 5591, 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), 3894, 1994.
 Andrew Wright. Simple Imperative Polymorphism. LISP and Symbolic Computation, 8(4),
343355, 1995.
Downloads
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.