CoursePlan

Category Theory and Functional Programming

7.5hp, PhD level course, Spring 2010

Examiner: Patrik Jansson

Course Description

Category theory, with an origin in algebra and topology, has found use in recent decades for computer science and logic applications. This can be clearly seen in the design of the pure functional programming languages like Haskell and Agda - where the categorical paradigm has influenced the language design, and given rise to several of the language elements (functions, functors, monads, arrows, ...).

In this course, we will learn category theory starting from first principles with an eye towards its applications to and correspondences with Haskell and the theory of functional programming. We expect students to previously have taken courses on Programming languages, Functional programming and Logic and to have some level of mathematical maturity. (The courses "Types for Programs and Proofs" or "Advanced Functional Programming" are also recommended.) We also expect students to have had contact with linear algebra and discrete mathematics in order to follow the motivating examples behind the theory expounded.

Overview

This course aims to give an introduction to Category Theory from first principles, with a close view to its role in functional programming theory, in programming language design, and in the design and structure of Haskell.

Learning objectives

After the course is completed, I expect a participating student to be able to

Follow and perform category theoretical arguments and diagram chases.
Argue categorically about Haskell code constructs.
Draw parallells between Haskell constructions, categorical standard constructions and propositional logic.
Read, understand, present and review material relevant to the CTFP course.

Examinatinon

Each student should

A: (10h) do a literature search to identify five suitable research papers connecting "Category Theory and Functional Programming (CTFP)" to his or her own research / application interests. Deliverable (by week 13): a BibTeX-file with the citations + a memo citing them including a one-paragraph-per-paper explanation of the connection.
B: (10h) identify one (of the above) papers as a suitable read for the whole group. Deliverable (by week 13): A one-page summary connecting the paper to the CTFP theme.
C: (80h) work through the Awodey book and identified "suitable reads" papers. Deliverable: active participation in the seminar discussions.
D: (20h) host one of the weekly seminars. Deliverable (by "your" week): a tutorial-style .pdf-slideshow of (some of) the material in the part of the course (lecture or paper) scheduled for that seminar. Presentation time, 45 min.
E: (70h) perform a case-study or implementation project. Deliverable (by week 19): a "workshop paper" (5-10 pages) or well documented source code.
F: (10h) review the case-study / project of one other participant. Deliverable (by week 20): a one-page review of the strengths and weaknesses of the deliverable E from the other participant.

Literature

See separate literature list.