Category Class Set Type

[Pete, you're asking several rather enormous questions (e.g. what is CategoryTheory?), and the lack of answers over the last year indicates to me that some kind of rephrasing to allow a short answer, rather than book-length answer, would be in order. -- DougMerritt]

Asking a question out of confusion in the context of mathematics: What's the difference between these things?

As far as I can tell from my naive reading of sources like MathWorld, a Class is a Set sexed up with one of a number of restrictions that force it to relate to other Classes in some kind of lattice structure. Which is to say, no StrangeLoops allowed.

A Type seems to be some kind of attribute of rank in this Class lattice.

And a Category seems to be some kind of arbitrary grouping of objects with the same Type. Morphically speaking.

I am obviously not getting this - can someone with a good math head please spell it out in little words?

CategoryTheoryForSoftwareEngineers? (or just for the lowly programmers in the well-known hierarchy), InteractionDesigners? need not apply:

CategoryTheory is ExtremeRefactoring and OnceAndOnlyOnce pushed to the limits, in Mathematics.

We start by looking at sets and functions that map from one set to another. And consider a set as just things (objects); you don't care whether the sets have elements nor what is the meaning of the sets. And because a function is from a set to another set, again, you do not care that it's a function or what that function means, you simply call it arrow (or "morphism"). We see that these thingies and arrows have some compositional properties, like lego pieces: if there's an arrow A -> B and another arrow B -> C then we can make an arrow from A to C by composing the two arrows. For every thingie A there's an identity arrow, we'll call it id_A ("identity A", term used for this wiki page only) A -> A, such that when composed with another arrow going out of A or coming into A, we get the same arrow, just like 0 is the identity for addition or 1 is the identity for multiplication.

Now we move to another universe: sets and relations. And we do the same with binary relations that we did with functions; they are between sets. So you call the set things as before, but now the arrows are the relations. So we have generalized from set+function to set+relation.

And yet another universe: Integers and "<=". We call integers the thingies and "<=" the arrow, for every i <= j that really is true (note it's not the global <=, but each instantiation that holds true. And we note that if we have both i <= j and j <= k then we also have i <= k, so we kind of have composition as well. Please note that while in the "universe" of set and functions, there's a handful (and on occasions an infinite number) of arrows between two thingies; in the ordered universe of integers and <=, there's always at most 1 arrow between two thingies.

Then we can similarly look at vector spaces and their isomorphisms and, as before, we find other thingies and arrows.

And so on, so forth. Many subjects of mathematics revolve around things and arrows. So a bunch of algebraists looked at theorems about sets and functions, and theorems about lattices, about ordered sets, about groups, vectorial spaces, and so on so forth. And they noticed that some of the theorems had the same structure. So they asked: are we not repeating ourselves from one universe to another ? So they went on ReFactoring, they abstracted in the extreme and they talked only about things and arrows. Surprisingly, a great deal of things can be proven without actual detailed knowledge about what the things and arrow are, just about their rules of composition. So in CategoryTheory they prove all kinds of theorems about things and arrows.

For example, if your arrows have this extra feature, then this theorem holds. And then a mathematician in a particular universe (say vector spaces with morphisms) just needs to prove that his things and his arrow match the concepts described abstractly in Category Theory. Then he can say that the theorem in category theory applies to that particular universe, because it is "the same" in terms of arrow relationships and thingies, as some previous result. So it's all about OnceAndOnlyOnce.

So to get it technical: the "universes" described above are called categories, the things are called "objects", and the arrows are called, well, just arrows, or morphisms. When you go deeper you discover that you can draw some correspondences between universes. For example, because every function between 2 sets is also a relation between the 2 sets, there's a "natural" correspondence between the universe of (sets + functions) and the universe of (sets + binary relations) that maps a set to the same set, and a function to the binary relation that is that function (more exactly to itself, viewed as a relation). So these second-level correspondences are called functors and themselves have arrow-like properties.

And there are theorems that allow some properties discovered in one particular universe of thingies and arrows to be applied to other universes with different thingies and arrows, provided you can find functors (second-level arrows) that make this correspondence between the thingies and arrows of the two universes.

Now coming to types in programming language, those can be viewed as thingies. And the function that takes as input a value of type A, and computes a value of type B, is an arrow. The fun thing here is that the arrow itself has a type, so the collection of all the arrows from A to B can be viewed as a thing. So the types are thingies, and the programs (function) are arrows, therefore this is one particular category (a special kind of universe that follows the rules for thingies and arrows).

Studying category theory is on occasion extremely boring. Because category theory is very dry and abstract, there's no inherent specific meaning behind the thingies and the arrows. So the theorems go like this: if the thingies and the arrows have some extra set of properties, which does not apply to all the thingies and arrows in general, then we can show that some certain "important" property holds. So that theorem was created by a bright mathematician, who knew what examples of concrete things and concrete arrows would have that property, so he had an intuition behind it. And he knows why the property that is the conclusion of the theorem is important (he would know where to apply that).

But the poor reader doesn't. The natural intuition is to associate thingies with sets and arrows with functions, so you check the abstract theorem for sets and functions to see if it holds. But many times it doesn't, because sets were not the kind of things that guy had in mind when he was talking in the abstract. So the reader is confined to a meaningless manipulation of symbols according to seemingly arbitrary rules. Only when, and if, you study another pileload of mathematics (domain theory, type theory, etc) then you can make sense of that special kind of thingies and arrows that the category theory was talking about.

Actually I think a wiki would help, because you can name the particular situations (the thingies and arrows with extra properties) and you can link to concrete instances and where they apply. Then the reader can look at 2 or 3 concrete situations and what you're after, and then spot the similarities and then go the abstract route with things, arrows and functors.

Does this help, Pete?

[Light editing was intended to be constructive, forgive me if I failed in that intention. Wiki diff is mildly confused about this edit in its synchronization, so I should mention that I did not do large scale changes like swapping/deleting/completely rewriting paragraphs, fyi.]