haskell - Where do values fit in Category of Hask?

Question

So we have Category of Hask, where:

• Types are the objects of the category
• Functions are the morphisms from object to object in the category.

Similarly for Functor we have:

• a Type constructor as the mapping of objects from one category to another
• fmap for the mapping of morphisms from one category to another.

Now, when we write program we basically transform values (not types) and it seems that the Category of Hask doesn't talk about values at all. I tried to fit values in the whole equation and came up with the following observation:

• Each Type is a category itself. Ex: Int is a category of all integers.
• Functions from a value to another value of same type are morphism of the category. Eg: Int -> Int
• Functions from one value to another value of different type are functor for mapping values of one type to another.

Now my question is - Do values even make sense in the Category of Hask (or in general category theory)? If yes then any reference to read about it OR if not, then any reason for that.

I hope the question makes sense :)

Answer 1

(I'll use words with their meaning from maths/category theory rather than programming, unless I mark it as code.)

One category at a time

One of the big ideas of category theory is to treat large complex things as a point, so, true to form the set/group/ring/class/category of all integers is considered a single point when you're thinking of the category Hask.

Similarly, you could have a very complicated function on integers, but it's just considered a single element (point/arrow) of a collection (set/class) of morphisms.

The first thing you do in category theory is ignore the detail. So the category Hask doesn't care that Int can be considered a category - that's at a different level. Int is just a point (object) in Hask.

One level down

Every monoid is a category with one object. Let's use that.

How are the integers a category?

There's more than one answer to this (since the integers are a monoid under addition and a monoid under multiplication). Let's do addition:

You can consider the integers as a category with a single object, and the morphisms are functions such as (+1), (+2), (subtract 4).

You have to hold in your head that I'm considering the integer 7 as the number 7 but using the representation (+7) to make it appear to be a category. The laws of category theory deliberately don't say your morphisms have to be functions, but it's clearer that something's a category if it has the structure of a set of functions containing identity and closed under composition.

Any monoid makes a single-object category in the same way as we've just done with the integers.

Functors from the integers?

A function f from the integers as a category under the operation +, to some other type with an operation ￡ that forms a category could only be a functor if you had f(x+y) = f(x) ￡ f(y). (This is called a monoid homomorphism). Most functions aren't morphisms.

Example morphism

Strings are a monoid under ++, so they're a category.

len :: String -> Int
len = length

len is a monoid morphism from String to Int, because len (xs ++ ys) = len xs + len ys, so if you're considering (String,++) and (Int,+) as category, len is a functor.

Example non-morphism

(Bool,||) is a monoid, with False as the identity, so it's a one-object category. The function

quiteLong :: String -> Bool
quiteLong xs = length xs > 10

isn't a morphism because quiteLong "Hello " is False and quiteLong "there!" is also False, but quiteLong ("Hello " ++ "there!") is True, and False || False is not True.

Because quiteLong isn't a morphism, it's not a functor either.

What's your point, Andrew?

My point is that some Haskell types can be considered categories, but not all functions between them are morhpisms.

We don't think of the categories at different levels at the same time (unless you're using both categories for some weird purpose), and there's deliberately no theoretical interaction between the levels, because there's deliberately no detail on the objects and morphisms.

This is partly because category theory took off in maths to provide a language to describe Galois theory's lovely interaction between finite groups/subgroups and fields/field extensions, two apparently completely different structures that turn out to be closely related. Later, homology/homotopy theory made functors between topological spaces and groups that turn out to be both fascinating and useful, but the main point is that the objects and the morphisms are allowed to be very different to each other in the two categories of a functor.

(Normally category theory comes into Haskell in the form of a functor from Hask to Hask, so in practice in functional programming the two categories are the same.)

So... what exactly is the answer to the original question?

• Each Type is a category itself. Ex: Int is a category of all integers.

If you think of them in particular ways. See PhilipJF's answer for details.

• Functions from a value to another value of same type are morphism of the category. Eg: Int -> Int

I think you mixed up the two levels. Functions can be morphisms in Hask, but not all functions Int -> Int are Functors under the addition structure, for example f x = 2 * x + 10 isn't a functor between Int and Int, so it's not a category morphism (another way of saying functor) from (Int,+) to (Int,+) but it is a morphism Int -> Int in the category Hask.

• Functions from one value to another value of different type are functor for mapping values of one type to another.

No, not all functions are functors, for example quiteLong isn't.

Do values even make sense in the Category of Hask (or in general category theory)?

Categories don't have values in category theory, they just have objects and morphisms, which are treated like vertices and directed edges. The objects don't have to have values, and values aren't part of category theory.