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.

Answer 2

As I commented on Andrew's answer (which is otherwise very good) , you can regard values in a type as objects of that type as a category, and regard functions as functors. For completeness, here are two ways:

Sets as Boring Categories

One of the most commonly used tools in mathematics is a "setoid"--that is, a set with an equivalence relation over it. We can think of this categorically via the concept of a "groupoid". A groupoid is a category where every morphism has an inverse such that f . (inv f) = id and (inv f) . f = id.

Why does this capture the idea of an equivalence relation? Well, an equivalence relation must be reflexive, but this is just the categorical claim that it has identity arrows, and it must be transitive, but this is just composition, finally it needs to be symmetric (which is why we added inverses).

The ordinary notion of equality in mathematics on any set thus gives rise to a groupoid structure: namely one where the only arrows are the identity arrows! This is often called the "discrete category".

It is left as an exercise to the reader to show that all functions are functors between discrete categories.

If you take this idea seriously, you begin to wonder about types with "equalities" that are not just identity. This would allow us to encode "quotient types." What is more, the groupoid structure has some more axioms (associativty, etc) that are claims about "equality of equality proofs" which leads down the road of n-groupoids and higher category theory. This is cool stuff, although to be usefull you need dependent types and some not fully worked out bits, and when it finally makes it into programming languages should allow

data Rational where     Frac :: Integer -> Integer -> Rational     SameRationa :: (a*d) ~ (b*c) -> (Frac a b) ~ (Frac c d) 

Such that every time you patterned matched you would also have to match on the extra equality axiom and thus prove that your function respected the equivalence relation on Rational But don't worry about this. The take away is just that the "Discrete category" interpretation is a perfectly good one.

Denotational Approaches

Every type in Haskell is inhabited by an extra value, namely undefined. What is going on with this? Well, we could define a partial order on each type related to how "defined" a value is, such that

forall a. undefined <= a 

but also things like

forall a a' b b'. (a <= a') /\ (b <= b') -> ((a,b) <= (a',b')) 

Undefined is less defined in that it refers to value that doesn't terminate (actually, the undefined function is implemented by throwing an exception in every haskell, but lets pretend it was undefined = undefined. You can't be sure something does not terminate. If you are given an undefined all you can do is wait and see. Thus, it could be anything.

A partial order gives rise to a category in a standard way.

Thus, every type gives rise to a category where the values are objects in this way.

Why are functions functors? Well, a function can't tell it has gotten an undefined because of the halting problem. As such, it either has to give back an undefined when it encounters one, or it has to produce the same answer no matter what it was given. It is left to you to show that really is a functor.