Skip to Content »

Michi’s blog » Soliciting advice

 Soliciting advice

  • July 22nd, 2009
  • 3:28 pm

Dear blogosphere,

come this fall, I shall be teaching. My first lecture course, ever.

The subject shall be on introducing Category Theory from the bottom up, in a manner digestible for Computer Science Undergraduates who have seen Haskell and been left wanting more from that contact.

And thus comes my question to you all: what would you like to see in such a course? Is there any advice you want to give me on how to make the course awesome?

The obvious bits are obvious. I shall have to discuss categories, functors, (co)products, (co)limits, monads, monoids, adjoints, natural transformations, the Curry-Howard isomorphism, the Hom-Tensor adjunction, categorical interpretation of data types. And all of it with explicit reference to how all these things influence Haskell, as well as plenty of mathematical examples.

But what ideas can you give me to make this greater than I’d make it on my own?

23 People had this to say...

Gravatar

What about writing course notes etc on the Haskell Wiki and asking for edits/suggestions/etc the way RWH and SPJ do/did their writing?

I know I’d like to learn these things, but I’ve never found any documentation that I considered accessible.

Gravatar
  • Derek Elkins
  • July 22nd, 2009
  • 17:31

(Re)Read this: Computational Category Theory. I particularly like the Curry-Howard-Lawvere-esque construction of a unification algorithm (or rather a compilation) from the proof that all finite limits can be constructed from a terminal object, products, and equalizers. You can then talk about unification in other categories, e.g. Poset which gives order sorted equational logic, which is the basis of the OBJ family of languages.

Many proofs in category theory are constructive and, thus, directly lead to algorithms. The CAM might also be worth talking about, and, if they are prepared for it, a bit of topos theory and its relation to higher order logic.

This video, Implementing Categorical Semantics, may also provide some ideas.

Gravatar

Start in your own notes with the definition of a topos. That’s your main goal. Then backtrack to the basic definitions of categorical concepts and work forward to topoi. Once you have topoi you can do other things like triples and monads from that base.

Gravatar

Incidentally, as I understand it what Haskell calls a monad is actually a triple. Yes, there’s a correspondence, but still the two are not the same thing.

Gravatar
  • Michi
  • July 22nd, 2009
  • 18:06

Shae: Sounds like a good plan. Thanks for the pointer!

Derek: I’ll make sure I’ll look into the links. Thank you. Right now, I’m reading through Barr&Wells and Lawvere&Schanuel to get a lay of the land before I dig into specifics.

John: That would make it all more challenging for me – since I must admit to still not having grokked what a topos is myself. Sounds like it would be a healthy approach, though.

Gravatar
  • Michi
  • July 22nd, 2009
  • 18:14

John: Also, what is the difference between a categorical monad and a triple? And what definitions are you using for them?

Is this about the Haskell definition using bind instead of join for the typeclass? i.e. not requiring the definition of a
join :: M M a -> M a
but rather a
bind :: (b -> M a) -> M b -> M a
?

Gravatar
  • jlouis
  • July 22nd, 2009
  • 20:50

Grab hold of:

Stephen Awodey, Category Theory (Oxford logics)

It introduces the basics and tends to use examples that a computer scientist understands. Monoids is a recurring structure for instance :). It is definitely easier to read than McLane for a first time reader.

Gravatar

Yes, that’s basically it. You can translate from one to the other, but the two are given by different data, and are semantically distinct. Similarly, the 1-torus and 1-sphere are not exactly the same thing.

A topos is basically a category with enough structure to give a model of set theory, so the category of sets is a topos. But so are categories of sheaves on sites, for instance. They have enough structure to mimic all the usual set-theoretic constructions, like unions and intersections. And when you think about how predicate logic and set theoretic constructions are related, you’ll realize how useful it is to have topoi around.

Gravatar
  • Damien Guichard
  • July 22nd, 2009
  • 22:44

From a down-to-earth point of view, monoids, functors, catamorphisms, paramorphisms, anamorphisms, (co-)monads and applicative functors are all programmer’s friends.

Plus they buy you the opportunity to play with Charity (a categorical programming language) which is fun because its recursion is so ‘primitive’.

However i agree that from a categorical point of view programming is much like a distraction.

Gravatar
  • Michi
  • July 22nd, 2009
  • 22:53

Damien: The modus operandi for the course is to connect up with the CS undergrads who have done Haskell, but not gotten enough connection to the underlying category theory, and give them the grounding they need to see the connections, and see the point of categories.

I could probably take a look at Charity – thank you for the suggestion – but it’s not going to be a major focus. I don’t want to teach a new programming language _too_ if I can avoid it. :-)

Gravatar

All of the above are good comments.

If I were trying to bridge the gap from Haskell to category theory I’d be sure to throw in all the goodies from recursion theory (cata-, ana-, hylo-, para-,…) as well as tricks like Swierstra’s Data Types a la Carte. Both of these focus a lot on functors which are still down-to-earth enough to be easily grasped, but abstract enough to see where you’re headed: the perfect gateway drug. (Be sure to cover the laws of the various recursions, not just the recursive pattern.)

I’d also spend some time doing an aside on deforestation, build/fold and unfold/destroy fusion, generalized Church encodings, why/how hylomorphisms are an optimization, and the like. These topics help to get into parametricity which leads to free theorems; and the focus on manipulating morphisms while “ignoring” the objects and their structure helps to break away from the thinking that’s so prevalent in set theory but antithetical to the category theoretic perspective.

There’s a lot of stuff out there on just the raw CT. The problem with most of it, IMO, is that it’s just CT. Basic CT is pretty easy, but seeing how to apply it to new tasks is a lot harder. Even though there are practical applications all over the place, there isn’t a really good resource for demonstrating the applicability of CT and charting out the overall geography of the field. I think the best thing for your course would be to try to give some of that geography so your students will have a better understanding for what areas of CT to continue exploring based on their interests.

Gravatar

wren: Thank you. My primary wish for the course is to make it a good gateway from the CS student who has heard categories mentioned in passing to someone who can start reading about the recursion theory things on their own; I certainly would like to include it in the course, but I don’t know whether I’ll have time for it.

John: One of my main intentions with the course is to be able to discuss the Hask category of Haskell types and computable functions between them. Is this a topos?

Gravatar

Well let’s see.. does it have

a) All finite limits?

b) All power objects?

Gravatar
  • Michi
  • July 27th, 2009
  • 14:53

It has all power objects: A^B is just the type B -> A.

As for finite limits, I’m less certain that it holds. Certainly, it has products and coproducts, but equational reasoning is often a matter of programming contracts more than of strict enforcement. However, I guess that one could argue that finite limits exist by virtue of having products, coproducts and a sensible QuickCheck suite verifying, Monte Carlo-style, any further relations.

The part I’m really iffy on is the subobject classifier (having read all of … five sentences of topoi that I understood by now…) – I don’t see how that fits.

Gravatar

Well, the nice thing is that if you have all finite limits and power objects you can *build* a subobject classifier!

Incidentally, what you’ve told me is that your category contains exponentials, not power objects. A power object is something like a power set. It turns out that when you’ve got a subobject classifier ? then the power object P(X) is the exponential ?^X. And a subobject classifier should be something like the Boolean type. It’s like the set of truth values in the category of sets!

Gravatar

Here is a pretty concise categorical definition of a power object.

Gravatar
  • Michi
  • July 27th, 2009
  • 17:16

John: Ooooooh, right.

I’d go with pointing at the List type as a potential power object. Hence, for the type T, the power object’d be [T].

Gravatar

Well let’s see.. actually I think that that post I linked to is slightly wrong. You need to specify the $latex \varepsilon$ monic instead of universally quantifying it. That is, you need to pick something like the “element of” relation.

So, what monic in the category of Haskell types mimics the “element of” relation, using [T] as power object?

I don’t have a copy myself, but I think the approach I found most sensible is in chapter IV of MacLane and Moerdijk. Reviewing my notes, they start with (binary) pullbacks, a terminal object, a subobject classifier, and a slightly different set of data to specify power objects. Since we know how power objects and exponentials will eventually relate, and that Hask has exponentials, we can use that to define the appropriate power objects once we have the subobject classifier.

Okay, so I still think that the classifying object will be the Boolean type. The terminal type should be what.. does Haskell have a type like C’s “void”? Then the (monic) computable function from void to Boolean should be “return True”.

The question (and I’m not a Haskell expert) would then be this: for every (monic) computable function $latex m:S\rightarrow B$, is there a unique computable function $latex B\rightarrow\mathbf{Bool}$ that returns “true” on instances of type B in the image of m and “false” on everything else?

Gravatar

Thanks, John, for clarifying the role of the subobject classifier.

There is an issue with all limits in Hask, though, it turns out. Having all limits is more than even the idealized Haskell category manages – and the keyword there seems to be Dependent Types.

Gravatar

I’m a bit late to this – sorry.

Ordinarily, I’d say you should get to adjunctions as quickly as possible, and then concentrate on the various theorems relating adjunctions and limits, and on the connections between monads and adjunctions. I don’t really think that topoi would be interesting to your proposed audience, but then I know very little about topos theory. BTW, Hask lacks equalisers, so it doesn’t have all finite limits (it’s an easy theorem that one can construct all finite limits if you have finite products and equalisers, or if you have binary pullbacks). Coproducts are, as the name suggests, colimits :-)

Jeff Egger recently taught what sounded like a really interesting basic CT course, which avoids all the tedious symbol-bashing by proving all the basics using string diagrams. It might be worth getting in touch with him to ask how it went.

I can perhaps explain the monad/triple thing. Among categorists, “triple” is a not-quite-abandoned name for “monad”, still used by a few of the older generation. There’s no semantic difference between the two. What Haskellers call a “monad” is called a “strong monad” by categorists, and that’s a slightly different notion. If John’s really saying that two concepts with different but totally equivalent definitions ought to be considered different, then I’m tempted to suggest that he hasn’t grokked the point of category theory at all – if two definitions give rise to equivalent categories of models and morphisms, one should really consider them the same.

Gravatar

pozorvlak, I’d say you haven’t grokked the point of higher category theory at all. If two definitions give rise to equivalent categories of models and morphisms, one should really consider them equivalent, not “the same”.

Gravatar

I am a retired economist turned marketing man. I am writing a book which will be concerned partly with an economic model which will address the chronic variability of the system, capitalist or otherwise. I am approaching it at three main levels: 1. Set-theoretic, where the main task undertaken will be to strictly define the Universe of Discourse as Arrow and Debreu did fairly successfully in regard to their now-famous model. Its a beautiful model but it just sits there, doing nothing, except maybe to suggest that if we gave it some impulsion (an old-fashioned shove) it would give us a clue to why, instead of a static or even a dynamic equilibrium we go through a centuries-long series of stops and starts in economic growth.
(2) In section two I am hoping that the conceptual field of Category Theory would enable us to give teeth to simple set-theoretic models of economic growth by providing the necessary one-to-one, one-to-many and many-to-one dynamic/kinetic relations which would allow and impel the damn thing to “go” or function.
(3) The third level would of course be the programming level which would provide the input to some enormous array of computers. This system would have room for built-in governors, not human ones but governors like those in the early steam engines. That’s where Category Theory would do its wonderful stuff.

However! Levels 1 and 3 I am fairly happy with. With Category Theory I have struggled manfully from fairly simple discussions to the beautiful output of a MacLane or a Lawvere. I need a simple example which shows me how to connect the three levels in a happy, functionning whole. How does one program an artificial child pedalling an artificial bicycle for, say, five minutes (No – ten seconds) using our three sets of tools? How do we build in the categories to make sure she does not fall off? Good luck John

programming level where we finally get down to business
#)

Gravatar
  • Michi
  • September 6th, 2009
  • 22:07

John: I’m not all that certain I see how Category Theory would make an easy interface between your levels. Of course, if you DO figure it out, it’ll be nice to see how you do it, but I remain cautiously pessimistic right now.

Want your say?

* Required fields. Your e-mail address will not be published on this site

You can use the following XHTML tags:
<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>