Does it matter if Hask is (not) a category?

Andrej Bauer raises a question whether Hask is a real category. I think it’s a legitimate question to ask, especially by a mathematician or programming languages researcher. But I want to look closer at how a (probably negative) answer to this question would affect Haskell and its community.

To illustrate the fallacy of assuming blindly that Hask is a category, Andrej tells an anecdote (which I find very funny):

I recall a story from one of my math professors: when she was still a doctoral student she participated as “math support” in the construction of a small experimental nuclear reactor in Slovenia. One of the physicsts asked her to estimate the value of the harmonic series \(1+1/2+1/3+\cdots\) to four decimals. When she tried to explain the series diverged, he said “that’s ok, let’s just pretend it converges”.

Presumably here is what happened:

1. The physicists came up with a mathematical model of a nuclear reactor.
2. The model involved the sum of the harmonic series.
3. Andrej’s math professor tried to explain that the series diverged and therefore something was wrong with the model.

When we try to model a phenomenon, we should watch out for two types of problems:

1. The model itself is erroneous.
2. The model itself is fine; but the phenomenon we are describing does not meet all of the model’s assumptions.

The first type of problem means that the people who built the model couldn’t get their math right. That’s too bad. We let mathematicians to gloss over the messy real world, to impose whatever assumptions they want, but in return we expect a mathematically rigorous model upon which we can build. In Andrej’s story, hopefully the math support lady helped the physicists build a better model that didn’t rely on the convergence of the harmonic series.

But at some point the model has to meet the real world; and here, the issues are all but inevitable. We know that all models are wrong (meaning that they don’t describe the phenomenon ideally, not that they are erroneous) — but some are useful.

Physicists, for example, often assume that they are dealing with isolated systems, while being perfectly aware that no such system exists (except, perhaps, for the whole universe, which would be impossible to model accurately). Fortunately, they still manage to design working and safe nuclear reactors!

Consider Hask. Here, the abstraction is the notion of a category, and the phenomenon is the programming language Haskell. If types and functions of Haskell do not form a proper category, we have the second type of modelling problem. The foundation — the category theory — is, to the best of my knowledge, widely accepted among mathematicians as a solid theory.

Since category theory is often used to model other purely mathematical objects, such as groups or vector spaces, mathematicians may get used to a perfect match between the abstraction and the phenomenon being described. Other scientists (including computer scientists!) can rarely afford such luxury.

Usefulness is the ultimate criterion by which we should judge a model. We use monads in Haskell not because they are a cool CT concept, but because we tried them and found that they solve many practical problems. Comonads, which from the CT standpoint are “just” the dual of monads, have found much fewer applications, not because we found some kind of theoretical problems with them — we simply didn’t find that many problems that they help address. (To be fair, we tried hard, and we did manage to find a few.)

There are people who, inspired by some category theory constructions, come up with novel algorithms, data structures, or abstractions for Haskell. For these discoveries to work, it is neither necessary nor sufficient that they correspond perfectly to the original categorical abstractions they were derived from. And as long as playing with the “Hask category” yields helpful intuition and working programming ideas, we are going to embrace it.