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

The second day in the course takes place Wednesday 7 October from 9:00 to 15:00 at SLV300-0.2.13

The programme for the second day of the course is as follows (a superscript "R" indicates a repetition from the last day):

9:00	CT2.1: Graphs; categories^R; transition systems; functors^R; natural transformations^R
9:40	Break
9:50	CT2.2: Adjoints; reflections; adjoint equivalences; Galois connections
10:40	Exercises
11:20	CT2.3: Transition systems, synchronization trees, and languages
12:00	Lunch
12:30	FP2: Type classes; constructor classes
15:00	Closing

For the new material, we shall use the following sources:

Pierce: Section 2.4
Rydeheard-Burstall: Section 6.3
Mac Lane: Sections 4.2 to 4.4
Winskel-Nielsen (Models): Sections 4 up to (and not including) 4.0.6, and 5 up to (and not including) "We can immediately observe some categorical constructions..."

The Mac Lane sections are available on-line here. We will not go through all this material, but leave some for self study.

Exercises marked with * are again available for student presentation. Exercises marked with + may require some extra mathematical pre-requisites.

Pierce 2.4.12.5
Mac Lane 1.4.3+ (p.18)
* Mac Lane 4.2.5 (p.90)
* Mac Lane 4.2.9 (p.90)
Mac Lane 4.3.4(a) (p.92)
Mac Lane 4.3.5 (p.92)
Mac Lane 4.4.3 (p.95)
* Mac Lane 4.4.4 (p.95)
Implement a version of set equality (for Set a) requiring only Eq a.
* Model categories (objects and morphisms) as an algebraic data type (i.e., using data)
1. Show how the category of (finite) Sets and functions is represented
2. Define a finite category as a data type and show how it is represented.
3. Discuss if/how your representation captures the axioms defining a category.
Model functors as a data type
1. Define two functors, e.g., between the categories defined in exercise 1, and show how they are represented.
Make a representation of the ninf-max semiring and make a (direct) instance of the semiring class.
Define a type class for groups
1. Make an instance of the group class for Int's
2. Can you make an instance for Num's?
* Model categories and functors again, this time using type clasess (note: the name Functor is already used)
1. Does your model of functors correspond to the pre-defined representation?
2. Re-do the representations from exercise 1.
Discuss pros and cons of the data type vs. type class representations.