How laws help to validate the meaning of categories in haskell

Question

All categories in haskell (Monoid, Functor, Monad etc) have corresponding laws which an instance must satisfy in order to guarantee the category works as expected. What I am not able to understand is that how a specific law has been chosen for a category? For example, what is the reasoning behind choosing id & composition laws for functor?

Answer 1

A Long Rambling Ode to Functors

Categories, functors, natural transformations, limits and colimits appeared almost out of nowhere in a paper by Eilenberg & Mac Lane (1945) entitled “General Theory of Natural Equivalences.” We say “almost,” because their earlier paper (1942) contains specific functors and natural transformations at work, limited to groups. A desire to clarify and abstract their 1942 results led Eilenberg & Mac Lane to devise category theory. The central notion at the time, as their title indicates, was that of natural transformation. In order to give a general definition of the latter, they defined functor, borrowing the term from Carnap, and in order to define functor, they borrowed the word ‘category’ from the philosophy of Aristotle, Kant, and C. S. Peirce, but redefining it mathematically.

Thus speaks the Stanford Encyclopedia of Philosophy, an exceptionally wonderful resource if you want to dive into some citations into early CT papers. This paper, "General Theory of Natural Equivalences," is (I would say) a must-read for you. (You can circumvent the academic paywalls by searching for the title on Google, but here's a link that may or may not die soon.)

Let's take Functor as an example. The three laws are

• There exists an f a -> f b for every a -> b (we express this as a theorem with the type (a -> b) -> f a -> f b and we prove it by defining the function in Haskell value terms)
• fmap id = id
• fmap (f . g) = fmap f . fmap g

The typeclass Functor is meant to represent categorical functors in this way: if an instance Functor f exists, then we can treat f as a functor F from Hask to F(Hask). This alone is not useful, but category theory has this way of luring you into proving powerful, general results from simple, trivial properties about mathematical objects.

These three laws follow directly from Eilenberg and Mac Lane's original definition:

The notation is antiquated but the ideas are the same.

But, again, why? Why did we rest this foundational idea in category theory on these notions of objects, arrows, identity, composition, and distribution? A helpless answer is that they "work." Functors, once defined like this, appear everywhere: groups, vector spaces, topologies, graphs, Reader/State/IO, self-referentially within CT itself. They are just specific enough to allow the proof of various properties and just general enough to allow these proved properties to be interesting and useful.

A more helpful answer might be to read the introduction to Eilenberg and Mac Lane's paper, where they carefully carve out space for the work (which appeared almost out of nowhere!) that they are about to do. They take a vector space L and its conjugate space T(L); they notice that you can prove an isomorphism between the two but only if you can fix a basis. Then they take L and its iterated conjugate space T(T(L)); now here is an isomorphism that exists for all finite L without any special basis. This they call "naturality," a notion of elegance attached to a notion of equality. Once you notice this you begin to see it everywhere.

But to begin talking about this you first need to give a name to the thing that maps from L to T(L) to T(T(L)). And that name and its definition must be broad enough to apply to groups and topologies and whatever else you have on hand. So that's a functor. And its laws are adopted from pre-existing laws in each field. In software engineering terms, we might say that a functor is the refactoring of mathematical laws.

The analogy here to Haskell programming is that there are functions that show up all the time in other languages. You will see a mapMaybe :: (a -> b) -> Maybe a -> Maybe b or mapPromise :: (a -> b) -> Promise a -> Promise b or mapState :: (a -> b) -> State r a -> State r b. Perhaps not in those exact forms; perhaps as methods on a generic class instead if you're stuck in OOP land. There is something being duplicated in each of these library functions. There appears to be a natural equivalence between the universe of all the types and then the universe of Maybe/State r/Promise applied to all these types. You might even note that a language with algebraic data types can, as Ed Kmett points out, automatically generate these functions.

So, for example, why do we insist that identity be preserved in the mapping? Well it lets you automatically generate the one unique fmap per each ADT. And it makes equational reasoning easier because if you see fmap id you can automatically substitute id. Or maybe the reverse, where if you see id you can automatically substitute fmap id. And it works well with the free theorems for fmap. And a litany of other reasons. It was a guess made by mere mortals that paid off.

So, in another language, we would document or blog about this collection of same-looking map* functions as a curio of a mysterious life unled. But with typeclasses and strong types and, heck I'll see it, parametricity we can actually encode the idea in a language like Haskell. And that's the wonderful thing about Haskell.

Answer 2

leftaroundabout corrected your terminology a bit, but to elaborate: a category in category theory is an abstraction that consists of objects, transformations between those objects, and the ability to compose those transformations (where this composition is associative). We don't very often talk about categories themselves in haskell, but some of the abstractions we use which come from category theory we talk about as living more or less in the category we call Hask. There is a representation of the category abstraction in Control.Category; it's a more general version of (.).

But I would forget about the abstraction called category for now. The important thing to understand is that that the way we express abstractions like category in haskell is with type classes.

You ask why the laws are the way they are. The hallmark of a good abstraction is that it is general enough to be widely applicable, while still giving us something useful.

I think Monoid is the best example to consider. Lists, sets, the integers with respect to addition (and with respect to multiplication), functions from a thing to a monoid, etc. all form a monoid: that is we can define implementations for mempty and mappend which satisfy the laws you can read about here, so it's clearly widely applicable.

But what do the laws give us? The laws let us write more useful code that is generic in the choice of monoid. For instance knowing that mappend is associative lets us define a single:

mconcat :: [a] -> a

and our users don't need to care about whether this is implemented with a foldr or a foldl or something else. It also means the compiler is free to choose the optimal order of our fold based on the context. The fact that we have an identity object means that this function can be safely called on the empty list.

The monoid laws are also essential in the context of distributed computing too, e.g. you have the map-reduce pattern, in which a monoidal reduce operation may be freely applied in parallel over your distributed "list".

So when you ditch the laws you get something less useful. But why these laws? I think the simple answer is that because people have found them useful. It's also the case that relaxing or removing laws can create something more general and also useful in different contexts. For instance in haskell we have the Semigroup class, or in mathematics you have non-euclidean geometries.