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.
"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.
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.
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.
- Categories, duality, functors
- Natural transformations, adjunctions
- Universality, limits, co-limits
- Monads, algebras, co-monads, co-algebras
- Examples, examples, examples; from computer science and mathematics
- Introduction to Haskell
- Advanced constructions in Haskell
- Monads in functional programming
For the category theory part of the course, we will use the following as a basic textbook:
We will also make use of material from the following sources:
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:
We will additionally make use of the following sources:
- First day programme
- Second day programme
- Third day programme
- Fourth day programme
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.
- Closely related is the more advanced notion of monoidal categories, which are categories with an extra "tensor" product. These are covered in Mac Lane Chapter 7; especially interesting for computer scientists is Mac Lane Section 7.7.
- 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
- 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
- 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