Sunday, 18 January 2009

The Category Theory of Appendages

There has been much discussion recently on haskell-cafe about Monoids, much (too much!) focusing on the possibility of renaming of the existing monoid typeclass to "Appendable"... which is a daft idea, not least because then we'd need to rename Monad to be "Appendage".

Anyway, I wanted to focus a bit on the link between the two concepts (monoid and monad), and how that's treated from the Category Theoretic perspective. (I'm not aiming at any kind of rigour ... simply trying to gain some basic intuitions). In terms of assumptions, I assume familiarity with the definitions of Category, Functor and ideally categorical products / co-products, initiality and finality.

This article aims to cover similar ground to one of sigfpe's here, but at a slightly higher (hopefully simpler) level.


Traditional Monoids

The basic concept of Monoid is treated from the standard mathematical (abstract algebra) perspective here, and from the practical (Haskell) perspective sigfpe has a nice article here.

So, from a traditional point of view, a monoid is:

* A set, along with...
* an associative binary function over that set, accompanied by ...
* an identity element

The basic (non-category theoretic) view of monoids in Haskell is pretty much the standard one, viewing Haskell types as sets. So in Haskell common examples of monoids are: (String, (++), []) and (Int, (+), 0) and (Int, (*), 1) and (Bool, (&&), True) and (Bool, (||), False).

In the Haskell setting this means that the function has both arguments and result with the same type - ie the function's type is "a -> a -> a", and the identity element is a distinguished value of type "a". And, of course, it is exactly this which is embodied in the Data.Monoid typeclass.

Category takes this standard view of monoids and generalises it somewhat. This generalisation has two parts - not only does it generalise so that we can talk about monoids in different categories, but it also generalises so that we can have multiple ways of identifying monoids within a single category.


Categories which can contain Monoids

From the category theory perspective, a category can only "play host" to monoids under the following conditions:

* It must be equipped with a functor over the category which maps any pair of objects to another object, and any pair of arrows to another arrow. (This type of functor is similar to a normal functor apart from operating on pairs - and is known as a Bifunctor). Let us call this functor "B".

* It must have a distinguished object (which we'll call "e") which acts as an identity for this functor.

This then gives us what is known as a Monoidal Category. (Note that by making different choices for the (bi)functor and distinguished object we may have several different ways to view an underlying category as monoidal).

The simplest example is on Set - we take the standard product as the (bi)functor (which maps any pair of sets to the set which is their product), and a single-element set (ie terminal object) as the distinguished object.

In the context of Haskell, we take as the (bi)functor, the product (bi)functor (which maps any pair of types, say 'a' and 'b', to their product type "(a,b)", and any pair of functions, say 'a->c' and 'b->d' to the function '(a,b)->(c,d)'). As the distinguished object we take "()" - the unit type whose sole value "()" is written syntactically identically to its type.


Category Theoretical Monoids

Once we have those two components, we have a category in which it is possible to identify categorical monoids, but we don't actually have the definition of a categorical monoid itself. A monoid within a monoidal category is defined to be:

* An object (which we'll call "c")
* An arrow from B (c,c) to c.
* An arrow from e to c.

...such that some basic diagrams commute. Now, recall that "B" is the (bi)functor which we selected when creating our monoidal category, so "B (c,c)" is just another object.

So, to make this concrete - if we consider Haskell as a monoidal category as above, then we can take "c" to be "String", our first arrow to be "(++) :: (String,String) -> String", and our second arrow to be the function ":: () -> String" which takes "()" as its argument and returns "[]".

If we compare this with our first, non-categorical, definition of (String, (++), []) as a monoid above, the parallels are quite clear. The differences are firstly that we now need to pretend that (++) has type "(String,String) -> String" rather than "String -> String -> String", which we can do simply by viewing it as an uncurried function, and secondly that we're representing "[]" by a function rather than a value. This extra baggage only really becomes useful when we look at other categorical monoids (which aren't plain, normal monoids).


Monads

So far, when discussing Haskell, we've implicitly had in mind the category "Hask" which has types as its objects, and Haskell functions between those types as its arrows. What we can now do, is to consider another category which is closely related to "Hask" - namely the category formed by taking as objects all Haskell functors ("Maybe", "[]", etc...) and as arrows all functions from one functor type to another ("listToMaybe :: [a] -> Maybe [a]", "maybeToList :: Maybe a -> [a]", etc...). This is the "endofunctor" category over Hask, and these arrows are natural transformations.

Next we're going to go looking for monoids in this "endofunctor" category using our above definitions. We need to keep a slightly clear head at this point, because we need to remember that the objects of this category are functors over another category - hence when we just say "functor" we need to be clear whether we're talking about one of these objects (ie a functor in the underlying category), or about a functor over this category.

First we need to choose a (bi)functor over this category - we'll choose composition of functors (so this takes a pair of objects - say "Maybe" and "[]" and maps them to their composition "[Maybe]"). Secondly we need to choose a distinguished object - we'll choose the identity functor "Id".

Finally, using our second definition, we can see that a monoid in this category must be an object along with two suitable arrows (ie this will be a functor and two natural transformations in Hask). We can take 'Maybe' as the object, 'join :: Maybe (Maybe a) -> Maybe a' as the first arrow, and 'Just :: a -> Maybe a' as our second arrow.

Thus equipped, "Maybe" can be seen as a monoid in the endofunctor category over Hask. And that, of course, is what a monad is - a monad over a category 'C' is a (categorical) monoid in the endofunctor category over 'C'.


Back to Set (...and Hask?)

We can now go back and take another look at the Set category. This time we can look for some monoids which are monoids from the category theoretic perspective, but not from the traditional perspective.

We can do this by viewing Set as a monoidal category using co-product as the (bi)functor (ie disjoint union rather than product) and taking the initial object (the empty set) as the distinguished object. Under this definition, "monoids" would be objects (ie Sets - as before), equipped with (a) a function to the set from the disjoint union of the set with itself, and (b) a function to the set from the empty set - ie the empty function.

Now, I have to confess I don't remotely understand the implications of this. I haven't ever seen any reference to what such objects would be called in "Set". In Hask, the coproduct of 'a' and 'b' is 'Either a b', and on functions takes 'a->c' and 'b->d' to 'Either a b -> Either c d'. Also, I'm not sure how much sense it makes to talk about an empty type in Hask, or an empty function in Hask.

It seems like there ought to be something useful (back in Haskell land) to drop out of this... I'd be very interested in anyone has any ideas / pointers...

8 comments:

Anonymous said...

> Under this definition, "monoids" would be objects (ie Sets - as before), equipped with (a) a function to the set from the disjoint union of the set with itself, and (b) a function to the set from the empty set - ie the empty function.

Let’s see what we can make out of this. I’m going to write the elements of S={x,y,..}, and the elements of the disjoint union of S with itself as {Lx,Rx,Ly,Ry,...}, and the function that you describe in (a) as f.

Looking at the diagrams on http://en.wikipedia.org/wiki/Monoid_object, I think associativity requires f(f(LRx))=f(f(RLx)) and the other diagram implies that f(Lx) = x and f(Rx) = x (given that α, λ and ρ are chosen in the expected way).

It seems to me that this shows that each set is a categorial monoid in exactly one way. Basically, it’s forgetting which copy in a disjoint union an element lies.

In Haskell, this would be the function
> forgetEither :: Either a a -> a
> forgetEither (Left x) = x
> forgetEither (Right x) = x
and the empty function could be this one:
http://hackage.haskell.org/packages/archive/category-extras/latest/doc/html/Data-Void.html

Twan van Laarhoven said...

I think the coproduct monoid would correspond to a Haskell class with methods "copappend :: Either a a -> a" and "copempty :: Void -> a". The latter function is completely useless, since there are no values of type Void.

nomeata said...

While I’m at it, I find it strange that this library defines these instances:
> HasIdentity Hask (,) Void
> Monoidal Hask (,) Void

I’d expect
> HasIdentity Hask Either Void
> Monoidal Hask Either Void
> HasIdentity Hask (,) ()
> Monoidal Hask (,) ()

Also I’d expect the methods "idl" and "idr", which correspond λ and ρ, as methods of HasIdentiy and I’m missing an method of Monoidal representing α (using the notation of http://en.wikipedia.org/wiki/Monoidal_category). Maybe I should submit a patch.

nomeata said...

I wrote a patch and submitted it, you can have a look at it here:
http://darcswatch.nomeata.de/repo_http:__comonad.com_haskell_category-extras.html

Edward Kmett said...

Hi there.

Actually the choice of Void over () is deliberate and somewhat subtle.

() has two distinguishable members. _|_ and (), so there is extra 'information' available in a pair of () and another value, while Void is always _|_, so there is no information lost, hence its status as an identity. Technically since (,) introduces a bottom, it is already a bit of an approximation to say that Hask is Monoidal. If you go back to ~1.4 with strict pairs its true though. You can't have any extra information imparted because of the requirement that idr/coidr reflects a natural isomorphism. coidr should be called opidr or something, but see below.

> Why do you define inl and indr as methods of Monoidal? To me it seems
as if they'd belong to HasIdentity, as they are defined for this
property (based on http://en.wikipedia.org/wiki/Monoidal_category)

In Hask^op, (,) is the Sum, which has an identity, but coidr and coidl are defined, not idl and idr, so integrating them into HasIdentity is flawed because of lax scenarios where one way exists but not the other.

* Are you sure
> HasIdentity Hask (,) Void
and
> Monoidal Hask (,) Void
is correct?

Yeah


I'd expect
> HasIdentity Hask Either Void
> Monoidal Hask Either Void
> HasIdentity Hask (,) ()
> Monoidal Hask (,) ()

The use of the terms Monoidal and Comonoidal in that file are non-standard and apparently I dropped my documentation to that effect. ;) Mainly because idl and idr only witness the 'forward half' of the natural isomorphism between I * A and A for an identity I for * and so should probably be called something like LaxMonoidal, while coidl/coidr witness the 'backwards half' of the natural transformation, which is required for a lax comonoidal category. Since you need a full natural isomorphism to be truly monoidal, the irony is you need both definitions for idr/idl and coidr/coidl to be truly monoidal, and similarly you need the same definitions to be truly comonoidal. However, this then necessitates 4 functions with the exact same signature and no ambiguity, I should go through and clarify that in the commentary, and probably rename Monoidal/Comonoidal. Arguably they should be something like idr/idl/opidr/opidl and coidr/coidl/coopidr/coopidl, but the signatures are the same, co and op 'cancel' and it gets really confusing fast, i.e. which comes first in the name, co or op?

With that in mind, in a perfect world, a language's category could be a monoidal category over (,) and a comonoidal category over Either, which means in the terminology above, that Either would have a Monoidal Void-like Identity, unfortunately, for Either to have a true identity the type has to be truly uninhabited, which isn't possible in Haskell because _|_ is a member of every type. An Monoidal Identity for Either wouldn't even have _|_ as a member, so calling that identity 'Absurd' for the nonce, it would mean that if you have Either a Absurd, that you cannot have used the Right constructor at all, because you couldn't have applied it to a value. This means that it'd be safe to idr to always reduce Either a Absurd -> a without creating a _|_. Unfortunately the decision to allow _|_ in the Right slot is a decision of how Either and laziness interact and has nothing to do with the definition of Absurd. This is clearly required by the requirement that idr/opidr (er.. coidr currently) reflect a natural isomorphism. Either a Absurd can't have any more members than 'a', but Right _|_ is an extra member in Haskell. Contradiction.

An arguably more correct choice of terminology would be to move idl and idr into something like HasLaxIdentity and coidl and coidr into something like HasColaxIdentity, then make Monoidal and Comonoidal both require HasLaxIdentity and HasColaxIdentity, then correctness would be restored.

Anonymous said...

In the coproduct monoidal category, shouldn't the coidentity be 'a' (the type of 'undefined')?

Edward Kmett said...

dysfunctor, unfortunately _|_ inhabits 'a' as well. this seems like it works until you realize that there can't be a natural isomorphism between Either a Whatever and a because the extra member Right _|_ has no place it can be mapped to uniquely in a.

Anonymous said...

Homes For Sale, Foreclosures listings from homesbylender.com register free. If you are selling your home by owner visit homes by lender and list it here for free. Homes For Sale