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...

48 comments:

nomeata 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.

dysfunctor 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.

逛街 said...

Happy New Year~~!!!............................................................

九份 said...

pleasure to find such a good artical! please keep update!! ........................................

冰淇淋 said...

nice to know you, and glad to find such a good artical!.........................

劭傑劭傑 said...

may the blessing be always with you!! ........................................

彭志文 said...

時間就是塑造生命的材料。......................................................

鍾FeR_Quade0426 said...

hello~welcome my world~<. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

嘉偉 said...

很喜歡你的blog哦...加油唷 ........................................

雅婷雅婷宛佳 said...

No pains, no gains.......................................................

Glennie9654 said...

thank you for you to make me learn more,thank you∩0∩ ........................................

韋于倫成 said...

處順境須謹慎,處逆境要忍耐。........................................

怡潔 said...

Never put off till tomorrow what may be done today................................................................

NealVa憲妤 said...

85cc卡通成人片 av免費視訊 尋夢網聊天室 免費成人 高雄交友網 女優寫真網站 性感影片 歐美 自拍 ut聊天室 女女愛愛 情趣桃園 成人網站 少女自拍 av影城 台灣a片免費看 情色漫畫 色情"" 一夜情 383 18禁 玩美女人 電眼美女 辣妹性感 人妻相簿, 激情熟女 影音視訊聊天室 視訊聊天 a圖片免費看 寫真免費影片 85cc成人圖片 杜雷斯成人微風 免費視訊 視訊聊天室 自拍性愛貼圖 援交妹拍影片 情人趣味 免費線上影片 av免費影片觀賞 洪爺影城如何下載 大奶色情影片 520sex 成人片下載 新任巨乳女教師奈奈下 性愛光碟 後宮電影院+入口 限制級 0204 性愛免費看 歐美正妹走光照

柏勳 said...

you always know the right thing to say!............................................................

東芳 said...

your english is incredible............................................................

AlysiaDraeger0417永瑞 said...

若無一番寒徹骨,焉得梅花撲鼻香。 ............................................................

SadeRa盈君iford0412 said...

青春一逝不復返,事業一失難有成。........................................

奕生 said...

你不能改變容貌~~但你可以展現笑容.................................................................

RoseH_Huls21365 said...

你不能左右天氣,但你可以改變心情..................................................................

麗芬 said...

人因夢想而偉大,要堅持自己的理想哦......................................................................

林奕廷 said...

人因夢想而偉大,要堅持自己的理想哦......................................................................

kristinawils 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

婉婷 said...

欣賞是一種美德~回應是最大的支持^^.................................................................                           

江婷 said...

噴泉的高度,不會超過它的源頭。一個人的事業也是如此,它的成就絕不會超過自己的信念。.................................................................                           

嘉琬嘉琬 said...

人不能像動物一樣活著,而應該追求知識和美德............................................................

天花天花 said...

成功多屬於那些很快做出決定,卻又不輕易變更的人。而失敗也經常屬於那些很難做出決定,卻又經常變更的人.................................................................

PearleY建佑 said...

這BLOG真是讓人意猶未盡!!..................................................................

恩如 said...

寂寞又無聊 看到你的BLOG 加油喔!!..................................................................

淑娟淑娟 said...

相逢即是有緣~~留個言問候一聲,祝您平安順利............................................................

吳婷婷 said...

當最困難的時候,也就是離成功不遠的時候。.......................................................

王美妹 said...

加油!期待更新哦!............................................................

denmitr said...

IS VERY GOOD..............................

蔡舜娟蔡舜娟 said...

要求適合自己的愛情方式,是會得到更多,還是會錯過一個真正愛你的人。.................................................................

林彥以林彥以 said...

留言支持,請繼續加油,謝謝您囉~~............................................................

吳淑芬吳淑芬 said...

祝福您春風得意。............................................................

陳雅吳水以竹 said...

安安唷~~幸運的日子送給妳(你)滿滿的幸福,也祝福你天天都開心唷..................................................................

家唐銘 said...

A stitch in time saves nine.............................................................

燕明中延 said...

走召糸及言贊白勺口拉............................................................

恩宛玲如 said...

與朋友在一起,分擔的痛苦是減半的痛苦,分享的快樂是加倍的快樂。......................................................................

por said...

河水永遠是相同的,可是每一剎那又都是新的。..................................................

冠陳儒 said...

「仁慈」二個字,就能讓冬天三個月都溫暖。..................................................

張王雅竹欣虹 said...

累死了…來去看看文章轉換心情~............................................................