Types, Sets and Categories

Question

I am learning Category Theory and at first I just pictured a category like a class in object oriented programming: type definition + methods (morphisms). However the author I am reading uses maps like A --f--> B and doesn't tell you if f is going from category A to category B, or if A and B are in the same category. He also uses sets, which is more troublesome if you care for the the meaning of what you are doing.

Questions

How are categories different from sets? And why doesn't every body just use types in the first place?

Note: The second question is a teaser, I study Mathematical Engineering but am also a Developer. In programming languages the notion of type is very well understood, and one of these types is the Set and there is nothing special to it. In math however, the concepts its not only incredibly dominant, it had/has mayor flaws (paradoxes).

Answer 1

Categories are different from sets in many respects. One answer would be that sets are $0$-dimensional and categories are $1$-dimensional. To see that, note that a set only has elements in it which can be thought of as point-like entities. If you were to draw a picture of the set $\{1,2,3,4\}$ you would draw four points and mark them accordingly. If you were to draw a picture of the set $\{dog, cat, alligator, piano\}$, then you will again draw four points and label them accordingly. In that sense sets are $0$ dimensional. Now a category consists of a set (or a class) of objects, which can again be thought of as point-like entities, but then there are also the morphisms, or arrows. An arrow, or morphism, in a category can be drawn as an arrow from some object to another. In that sense, categories are $1$-dimensional.

The analogy between classes in OOP and categories in mathematics is not a very strong one. There are certainly some things in common, but it is not a good idea to thing of the two notions as very much related. In OOP a class consists of data and methods. The methods use and act on the data. When you define a category there is no such divide. A category specifies the objects and the morphisms, but it is incorrect to view the objects as data and the morphisms as using or acting on the data. In fact, it is well-known that the objects can be completely dispensed with, while in a class in OOP, the data certainly is not redundant. In a category, each morphism is tied to a domain and codomain. It does not necessarily act on its domain. In fact, the domain can be anything at all, not necessarily a set, so there may be nothing to act on.

The confusion you mention with $f:A\to B$ (or whatever notation is used) should not exist. In the context of categories, $f:A\to B$ always means that $f$ is a morphism in some category (understood from the context) and the domain of $f$ is $A$, while the codomain is $B$. It is possible that $A$ and $B$ are themselves categories, and $f$ is then also known as a functor. This is in line with the above since there is a category of categories and functors.

Type theory is not the same as category theory. Type theory is much more related to classes in OOP than categories are. The programming paradigm that is most categorical is functional programming, where type theory is prominent as well. In OOP one can also adopt functional programming ideas, and in fact functors and monads (which can be modeled in any OOP language using classes that behave in a certain way, and in most functional languages are supported directly) are present in programming.

As for flaws with sets, there aren't really any, at least none that we know of. The prominence of sets in mathematics is simply due to the fact that it provides a very convenient and basic language to speak of practically all of maths. After all, what is more fundamental that a set, just a bunch of things collected together? So, anything at all (almost) can be expected to be: a set with.....

Answer 2

If you want to better understand category theory with computer science in mind, I suggest you read:

Asperti and Longo:

Categories, Types and structures: An Introduction to Category Theory for the working computer scientist

which should be freely available online

or

Pierce: Basic category theory for computer scientists

or

Barr/Wells: Category theory for computing science

Anyway , if you just want to understand what is a category and get more than a feeling for the theory, I suggest you look in Wikipedia

Answer 3

For start sets are rather different objects from categories in that they are structureless data type, from type theoretic view point sets are just data type with an equality relation.

Categories are a completely different sort of objects, for start they consist of two type of objects (objects and morphisms/arrows) and they have much more structure: there are various operations that relate them.

Of course you can treat categories from a type theoretic perspective, and in such perspective you can reguard a category just as an instance of a specification for an abstract data type.

There are different specifications for a category, one is the following one.

A category $\mathbf C$ is given by:

• a type $\mathbf C_0$ whose terms are called objects;
• a type $\mathbf C_1$ whose terms are called morphisms;
• two operations $s,t \colon \mathbf C_1 \to \mathbf C_0$ which are called source and target respectively;
• one operation $i \colon \mathbf C_0 \to \mathbf C_1$ called identity
• one partial operation $\circ \colon \mathbf C_1 \times \mathbf C_1 \to \mathbf C_1$ called composition

this data are required to satisfy the following properties:

• for every $f,g \in \mathbf C_1$ the composite $\circ(g,f)$ is defined iff and only if $t(f)=s(g)$;
• whenevery $f,g,h \in \mathbf C_1$ are morphisms such that $s(h)=t(g)$ and $s(g)=t(f)$ then $h \circ (g \circ f)=(h \circ g) \circ f$ (note that this composite are defined because the previous property);
• for every $X \in \mathbf C_0$ and every $f,g \in \mathbf C_1$ such that $s(f)=X$ and $t(g)=X$ you have that $f \circ i(X)=f$ and $i(X) \circ g=g$.

This specification can be seen from a computer science point of view as an abstract data type, a category is simply an instance of this abstract data type.

Hope this helps.

Answer 4

The three concepts are different but in subtle ways. A category is a class, which is why we can have the category of all sets, but we cannot have the set of all sets. Even when a category is small (that is, just a set) it has more structure then a simple set. Any category $C$ is a pair $(Obj_C, Homs_C)$, while a set simply has elements.

As for types, we can think of types as sets. A type has elements and functions from one type to another simply send one element to another. From a categorical point of view, they're very similar. However, they differ in subtle ways, which are difficult to understand for people familiar exclusively with set theory, which is most people. Sets can contain elements of different sets, but types cannot. A type might be said to have an "image" of another type, but certainly we cannot say that a type contains other types. We do not have a set type in type theory, otherwise you would have the type of all types, which doesn't work.

The three $Cat, Set, Type$ are related in the sense that they are all Cartesian Closed. Any category that models computations must be such. They're also all (symmetric) monoidal. To be slightly pedantic, there are different type theories which are all slightly different. There's also different set theories, but we usually use first-order logic together with ZFA. We can also exclude 3 axioms from ZFA, which give the category $FinSet$ of finite sets. All are Cartesian Closed Symmetric Monoidal.