APPSEM Summer School, Caminha, September 2000
Course on Monads and Effects
by N.Benton, J.Hughes and E.Moggi

Prerequisites

• typed lambda-calculi, e.g. [GLT88,Mit90,Mit96]
• type systems for programming languages, e.g. [Mit90,Mit96]
• operational and denotational semantics of programming languages, e.g. [Mit96,Ten91,Win93]
• interpretation of (simply) typed lambda-calculus in cartesian closed categories, e.g. [Mit90,Mit96,Pie91,Ten91]

Contents

1. PART I - Monads for denotational semantics (E.Moggi) OVERVIEW on monads in category theory and computer science.

   METALANGUAGES FOR COMPUTATIONAL MONADS (see [Mog91]). Simple examples of computational monads in the category of sets and cpos.

   MONADS AND DENOTATIONAL SEMANTICS (see [Mog97]). How to translate a programming language into a metalanguage for computational monads, why such translation helps in structuring the denotational semantics of a programming language. How to build complex monads: monad transformers [LH96,Mog97] and layered monads [Fil99].

2. PART II - Monads in Haskell programming (J.Hughes)

3. PART III - Effect systems and monads (N.Benton)

References

• [Fil99] A.Filinski. Representing layered monads. In POPL'99. ACM Press, 1999.
• [GLT88] J-Y.Girard, Y.Lafont, P.Taylor. Proofs and Types. Cambridge Tracts in TCS 7. CUP, 1988.
• [LHJ95] S.Liang, P.Hudak, M.Jones. Monad Transformers and Modular Interpreters. In POPL'95. ACM Press, 1995.
• [LH96] S.Liang, P.Hudak. Modular Denotational Semantics for Compiler Construction. In ESOP'96. LNCS, Springer, 1996.
• [Mit90] J.C.Mitchell. Type Systems for Programming Languages. In Handbook of Theoretical Computer Science (van Leeuwen ed). MIT Press, 1990.
• [Mit96] J.C.Mitchell. Foundations for Programming Languages. MIT Press, 1996.
• [Mog91] E.Moggi. Notions of Computation and Monads. Information and Computation, vol 93. 1991
• [Mog97] E.Moggi. Metalanguages and applications. In Semantics and Logics of Computation, A.M. Pitts, P. Dybjer (eds). CUP, 1997.
• [Pie91] B.C.Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991.
• [Ten91] R.D.Tennent. Semantics of Programming Languages. Prentice Hall International, 1991.
• [Win93] G.Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.