Category Theory with Applications in Functional Programming: Ph.D. Course, October 2009

This course aims at giving you a solid introduction to category theory, and to apply concepts from category theory to gain insights in some advanced notions within functional programming.

This is a 2 ECTS Ph.D. course within the Computer Science and Engineering programme at the Doctoral School of Technology and Science at Aalborg University.

Organizers

Lecturers

"Why should I listen to you?"

Through this course you will gain insight in the basic concepts of category theory, an organizing paradigm increasingly used in many areas of computer science and mathematics. This will hopefully help you to be more structured in your research and to avoid pitfalls. You will also gain an understanding of modern functional programming and its relations to other fields.

Organization

The course will take place on the following four days in October 2009, each day from 9:00 to 15:00:

Thursday 1 October
Wednesday 7 October
Wednesday 21 October
Wednesday 28 October

The course will subsume four kinds of activity: lectures and exercises in category theory, and lectures and exercises in functional programming. In the beginning we will do more category theory, and in the end the functional programming part will have more weight.

Lectures and exercises in category theory will be given and supervised by Uli Fahrenberg; those in functional programming by Rene R. Hansen.

Evaluation

In order to pass the course, we will require you to present the solution of a selected exercise to the other course participants. More details on this during the first lecture.

Category theory:

Categories, duality, functors
Natural transformations, adjunctions
Universality, limits, co-limits
Monads, algebras, co-monads, co-algebras
Examples, examples, examples; from computer science and mathematics

Functional programming:

Introduction to Haskell
Advanced constructions in Haskell
Monads in functional programming

Literature

For the category theory part of the course, we will use the following as a basic textbook:

Benjamin C. Pierce: Basic category theory for computer scientists. MIT Press, 1991

We will also make use of material from the following sources:

David E. Rydeheard, Rod M. Burstall: Computational category theory. Prentice Hall, 1988. Available at http://www.cs.man.ac.uk/~david/categories/book/
Saunders Mac Lane: Categories for the working mathematician. Springer, 1998

We will make copies from these books available if needed. Also, for the numerous examples of categorical structures and constructions in the course we will read other material; more about this later.

For the functional programming part of the course, we will mainly use the following:

Bryan O'Sullivan, John Goerzen, Don Stewart: Real World Haskell. O'Reilly, 2008. Available at http://book.realworldhaskell.org/

Additional material

We will additionally make use of the following sources:

Glynn Winskel, Mogens Nielsen: Models for Concurrency. In S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum: Handbook of Logic in Computer Science, vol. 4. Oxford University Press, 1995. Also available at http://www.daimi.au.dk/PB/463/PB-463.pdf
Michael B. Smyth, Gordon D. Plotkin: The Category-Theoretic Solution of Recursive Domain Equations. SIAM Journal of Computing 11(4):761-783 (1982). Available at http://homepages.inf.ed.ac.uk/gdp/publications/Category_Theoretic_Solution.pdf
Mads Rosendahl: Introduktion til domæneteori (Danish). DIKU 1995. Available at http://akira.ruc.dk/~madsr/webpub/domaene.pdf

Lectures

Material for further study

Below follows a list of topics and material which can guide you further in exploring the land of categories and functional programming:

Cartesian closed categories. These are a special kind of categories which are important for applications in computer science. They are covered in Pierce Section 3.1 and Mac Lane Section 4.6.

Galois connections are a concept heavily used in static analysis, especially abstract interpretation. Essentially these are adjoint functors between preorder categories. They are introduced in Mac Lane Section 4.5.

Following up on Winskel-Nielsen's important work on the category of transition systems, the notion of open maps gives a categorical characterization of bisimulation. The standard reference on this is
André Joyal, Mogens Nielsen, Glynn Winskel: Bisimulation from Open Maps. Information and Computation 127(2):164-185 (1996). Available at http://www.brics.dk/RS/94/7/index.html.
Categorical formalisms and bisimulation-via-open-maps are useful for relating different formalisms. For timed automata for example, there is a notion of open maps in
- Mogens Nielsen, Thomas Hune: Bisimulation and Open Maps for Timed Transition Systems. Fundamenta Informaticae 38(1-2):61-77 (1999). Available at http://www.brics.dk/RS/98/4/index.html.
The notion of co-monads and co-algebras, dual to the one of monads and algebras, gives a different view on formal models. Essentially, a given formal model can be seen as a co-algebra for some functor, and bisimulation can be explained via co-induction to the final co-algebra. The standard reference is
- Jan Rutten: Universal coalgebra: A theory of systems. Theoretical Computer Science 249(1):3-80 (2000). Also available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.1958.