Theme: Subtyping and Computational Monads

Saarland University
Informatics
Programming Systems
Dieter Brunotte


Bachelor Thesis

Context

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.

References

• 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, 2002.
• Eugenio Moggi. Notions of computation and monads. Information and Computation, 93, 55-92, 1991.
• 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), 343-355, 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.