Why does the category of language types have morphisms, not functors?

Question

I am probably not phrasing this question well, so please bear with me as I try to explain what I mean.

I am working on learning category theory, as applied to programming. So far, I understand that:

• Objects in a category are "unbroken"; you're not supposed to peer inside them to see their internal structure.
• Any Set is a category
• Programming language types can be thought of as sets. (Bool is the set True, False; Int is the set of all integers; etc.)
• Thus, all of the types in a language form a category of sets.
• Morphisms are arrows between objects.
• If those objects are themselves categories, then the morphisms get called functors.

Taken together, that would imply that a function from Int to Bool is a functor, because it's a map from the the set category Int to the set category Bool.

However, I have also read elsewhere (in particular https://www.johndcook.com/blog/2014/05/10/haskell-category-theory/), that thinking of it that way is wrong and we really shouldn't be talking about language types being a base category with "just" morphisms. But I don't see how that fits with my previous logic.

I therefore must conclude that my previous logic is faulty, but I'm unclear how or why. What is the right way to conceptualize this? Are Sets just extra special exceptions? Or is it really just an arbitrary matter of preference for how to view the problem space? Or am I just flat out wrong somewhere?

Answer 1

There are several ideas floating around here. You can look at a programming language through a categorical lens, and then types are objects, and they are indeed opaque. So Bool is not a set of True and False in this picture. It's an object that has two morphisms (injections) going into it, one corresponding to True, and one to False. In Haskell these are the two constructors of Bool. They take no arguments, but that is interpreted as being morphisms from the terminal object (the unit type). It all works out nicely.

Then there is the more traditional picture where types are just sets of values and morphisms are functions between sets. Sets and functions form a category Set. That picture works nicely as long as you don't talk about partial function (ones that loop forever).

Then there is the third idea that every individual set is a category in itself. It's a discrete category, meaning there are no morphisms (other than identity) between elements. In that case, functions between sets would indeed correspond to functors between discrete categories. But a functor between discrete categories is nothing but a function on objects (elements) which is trivial on morphisms, so it's not a very interesting point of view.