[pl-seminar] Talk on Monday @ 12pm in CS4310

[Calvin Smith <cjsmith@xxxxxxxxxxx>]

Howdy yâall,

Next Monday at 12pm in CS 4310, John is going to give another talk in his category theory for computer scientists series. This time, heâll wrap up natural transformations and (hopefully) discuss the classic functional programming tool, monads. If youâre unfamiliar with the concept of a monad, theyâre often described as burritos [1], boxes [2], or âa monoid in the category of endofunctorsâ [3]. By the end of the talk on Monday, hopefully weâll know what that means.

Johnâs original message is copied below.

- Calvin

[1] https://blog.plover.com/prog/burritos.html

[2] https://wiki.haskell.org/Monads_as_containers

[3] http://james-iry.blogspot.com/2009/05/brief-incomplete-and-mostly-wrong.html

------------------

Hi, all,

I'm gonna keep going with category theory. First I must finish up a few things about natural transformations before we move on. That is I need to talk about the two different notions of compositions of natural transformations. 

I hope this doesn't take too long, because in the same lecture I would like to switch gears a bit and start talking about Monads. Monads are very important to functional programming, and gives a real example of when a category theory idea was applied to a programming problem. Since monads are so important and often confusing to programmers, I will spend multiple lectures on monads. However, before we start using category theory to talk about monads, I want to make sure we have the same programming intuitions about what monads are. This means, for the most part, we are going to put our category theory hats off to the side for this lecture, and just approach monads as a design pattern for functional programming. If everything goes to plan we will then generalize and approach monads from a categorical perspective in subsequent lectures, eventually culminating in a dissection of the statement "a monad is simply a monoid in the category of endofunctors; whats the problem?"

I have also appended the notes from the previous email onto this one. I have also added some information about natural transformations at the bottom.

If anyone has any questions let me know.

John

Lecture 1 (Categories)

A category has

 - objects

 - morphisms

Morphisms compose, composition is associative, and each object has an identity morphism.

Many equations in category theory can be represented via commuting diagrams:

Nodes of the diagram are objects in the category, edges are morphisms. The property of a commuting diagram is that every directed path with the same source and ending object yield the same morphism.

We use category theory as a generalization of algebra. That is we understand mathematical objects as objects in a category and morphisms are structure preserving transformations of those objects. Even though it is possible to do so, we don't embed elements of a group, for example, as objects or morphisms in a category. Instead, we study groups through the category of all groups Grp, where objects are groups and morphisms are group homomorphisms. We then learn about groups not through the elements of a groups, which is opaque in the category, instead we understand groups relationships through the morphisms.

We briefly talked about a smalle list of some examples of categories

Set - Objects sets, morphisms total functions

Set_{\bottom} - Objects sets with bottom, morphisms are partial functions

Grp - Objects groups, morphism group homomorphisms

Partial order (P, <=) - Objects elements of P, morphism between a and b if a<=b.

Cat - Objects (small) categories, morphisms functors

We talked about small vs large categories.

Small categories are ones which objects and morphisms form a set as opposed to a proper class.

Large categories are not small.

I also mentioned locally small categories. A category is locally small if for every pair of objects the class of morphisms between them form a set.

For the above examples only the partial order is a small category. All the other categories are large.

I also want people to make the connection between category theory and functional programming. We talked about the category Hask (which may not be a real category due to some programming constructs). We want to think of objects in this category as types, and morphisms as functions between these types. We will try and use many examples from programming to understand category theory. We may see later how deep this connections goes.

To get in the spirit of category theory we then talked about some patterns of objects and morphisms. I will list them here

                           Initial object          Terminal Object                 Product                    Co-product

Set                           {}                          Singleton Set            Cartesian Product        Disjoint Union

Hask                     void                                ()                                    (,)                            Sum Type

Partial Order      \bottom                       \top                               meet                            join

Grp                 Singleton Group      Singleton Group             Group Product           Free Product

Lecture 2 (Functors)

In the next lecture we talked about functors. A functor is a structure preserving transformation.

A functor F : C -> D maps objects in C to objects in D, and morphisms f : c -> d of C to  morphisms F f : F c -> F d of D with

 - (unit) F (id_x) = id_{F x}

 - (composition) F (g . f) = F(g) . F(f) for morphisms g and f of C.

Intuitively, a functor embeds the category C in the category D. They can smash objects and morphisms together but they cannot break any connections. Functors also preserve commuting diagrams. 

The above definition defines a covariant functor. A contra-variant functor G : C -> D maps objects of C to objects of D and morphisms f : c -> d of C to a morphism G f : G d -> G c with

 - (unit) G (id_x) = id_{G x}

 - (composition) G (g . f) = (G f) . (G g)

A contravariant functor reverses the arrows of C. We can equivalently say a contravariant functor G is just a covariant functor G : C^{op} -> D, where C^{op} is the opposite category of C.

A functor F : C -> C is called an endo-functor.

In programming we only have one category, say Hask. Thus, all functors are endo-functors. In programming, functors are containers, such as Maybe, List, Stream, etc. These functors give a new type for any other type, such as [a] for a type a, and they also provide an fmap :: (a -> b) -> (f a -> f b) for functor f. fmap for lists is just map. A good intuition is that endo-functors are containers.

Finally, we talked about a particular functor in category theory the hom functor, denoted Hom( - , =) or C( - , -), which maps a locally small category C to Set. This functor is actually a bi-functor which maps pairs of objects in C to the set of morphisms between those objects. Remember a bi-functor is a functor from a product category C x D, where objects are pairs of objects and morphisms are pairs of morphisms. The hom functor is covariant in the second argument and contravariant in the first. Equivalently the hom functor is a functor C(-, -) : C^{op} x C -> Set.

Lecture 3 (Natural Transformations)

Natural transformations relate functors having the same domain and co-domain. Many later definitions in category theory rely on natural transformations. Saunders Mac Lane supposedly stated, "I didn't invent categories to study functors; I invented them to study natural transformations."

Suppose we have two categories C and D, and functors F : C -> D and G : C -> D. A natural transformation \alpha : F -> G is a family of morphisms such that

 - For each object a of C, \alpha picks a morphism of D \alpha_a : F a -> G a. \alpha_a is called the component of \alpha at object a.

 - For each morphism f : a -> b of C we have (G f) . alpha_a = alpha_b . (F f). This is called the naturality condition.

This last condition is usually represented as a commuting diagram.

Natural transformations have a specific connection to functional programming. In Haskell at least, as part of some theorems for free, we get the property that any parametrically polymorphic function with an appropriate type signature is a natural transformation.

That is suppose we have endofunctors F and G in our programming environment. A natural transformation is then a polymorphic function of type alpha : forall a . F a -> G a. That is if you plug in a type a, you get a component of the natural transformation. For alpha to be a natural transformation, naturality must be satisfied. That is suppose we have a function f from type a to type b. Then we must have

  (fmap f) . alpha = alpha . (fmap f)

This equation is a little confusing because in Haskell syntax we remove the function annotations. Let's annotate the parts of the equality:

  f : a -> b, for some a and b

  Left side of the equals

    fmap f : G a -> G b

    alpha : F a -> G a

    (fmap f). alpha : F a -> G b

  Right side of the equals

    alpha : F b -> G b

    fmap f : F a -> F b

    alpha . (fmap f) : F a -> G b

The point about theorems for free is that if alpha is parametrically polymorphic  then the naturality condition is automatically satisfied. In high-level terms a function is parametrically polymorphic if it is defined by one formula for all types. That is, the definition of alpha : forall a . F a -> G a, shouldn't depend on what type a is. Parametric polymorphism contrasts with ad-hoc polymorphism, which does allow multiple formulas depending on the input type. An example of ad-hoc polymorphism is an overloaded say add operator. The actual computation of the operator will depend on whether the input type is a complex or int or float or whatever.

An example of a parametric polymorphic function is 

  safeHead :: [a] -> Maybe a

  safeHead [] = Nothing

  safeHead (x : xs) = Just x

The definition of this function does not depend on what the type a is. As part of theorems for free safeHead is a natural transformation, though verifying naturality is a good exercise.

The intuition here is that endofunctors are containers, and a natural transformation is going from one container to another without modifying the contents during the transformation.