Thanks Sebastien, This paper has passed in my radar's field but I must confess that although I think I grasped the idea, I was quickly lost in the profusion of symbols and notations. I am no mathematician, only a simple developer, although I am fascinated by several topics in mathematics so my attention tend to drop sharply when confronted with more or less complex proofs and layers of defintions and mappings. But of course, this may be a requisite to get to something so I am willing to pay some price, to the limit of my capabilities. Arnaud On Wed, Jun 22, 2011 at 8:17 AM, Sebastien Zany wrote:

Hi Arnaud, I'm not the best person to answer this question, and I'm not certain this constitutes an answer, but you might be interested in Conal Elliott's paper "Denotational design with type class morphisms" available at http://conal.net/papers/type-class-morphisms/. Sebastien

On Tue, Jun 21, 2011 at 11:30 PM, Arnaud Bailly wrote:

...

(2nd try, took my gloves off...) Hello Café, I have been fascinated by Cat. theory for quite a few years now, as most people who get close to it I think.

I am a developer, working mostly in Java for my living and dabbling with haskell and scala in my spare time and assuming the frustration of having to live in an imperative word. More often than not, I find myself trying to use constructs from FP in my code, mostly simple closures and typical data types (eg. Maybe, Either...). I have read with a lot of interest FPS (http://homepages.mcs.vuw.ac.nz/~tk/fps/) which exposes  a number of OO patterns inspired by FP.

Are there works/thesis/books/articles/blogs that try to use Cat. theory explicitly as a tool/language for designing software (not as an underlying formalisation or semantics)? Is the question even meaningful?

Thanks in advance, Arnaud

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Jun 22, 2011 at 2:59 PM, Arnaud Bailly wrote:

Hello Greg and Alexander, Thanks for your replies. Funnily, I happen to own the 3 books you mentionned :-) My interest in category theory is a long standing affair...

Note that owning a book, having read (most of) it and knowing a theory (or at least its principles and main concepts) is really quite a different thing from being able to apply it. Although I am certainly able to understand the Yoneda lemma, I am certainly unable to

Well, you're way ahead of me. I don't even "get" adjunctions, to tell you the truth. By which I mean that I have no intuition about them; it's not so hard to understand the formal definition, but it's another thing altogether to grasp the deep significance.

recognize the opportunity of using that knowledge to derive some new knowledge about something else. And being able to define a topoi is very different from being able to construct one or infer one out of a given category. This is an actual limitation of myself of course.

Indeed. But I'll bet your next paycheck that eventually CT will replace set theory as the basic mode of thinking about math, even at elementary levels. It just awaits that brilliant writer who can connect the dots appropriately.

Alexander's advice about using diagrams and simple notations is something I often try to do and something which most of the times end in writing a bunch of functions and data types in Haskell... What I am really looking for is a more systematic way of thinking about systems (or system fragments, or components) in a categorical way, perhaps starting with a bunch of arrows in some abstract category with objects as components and trying to infer new objects out of categorical consturctions which are made possible by the current diagrams (eg. what would be a pullback in such a category ? What would be its meaning ? Does the question itself have a meaning ?).

Maybe this is really foggy and on the verge to fall into "abstract nonsense"...

Long live abstract nonsense!

Completely off topic: a few months ago I had an idea about using category theory to provide rigorous semantics for the web (esp. rdf stuff etc.) I'll probably never find time to work out the details, but it's a fun exercise in any case; if you want to mess around with applying CT to the real world maybe you can coem up with improvements. See http://blog.mobileink.com/2011/03/resource-token-exchange.html. It's a bit of a mess, and some of it I would radically revise, but it might give you some ideas, if you're interested in the semantic web thingee.

Best regards, arnaud

On Wed, Jun 22, 2011 at 5:03 PM, Gregg Reynolds wrote: Well, you're way ahead of me. I don't even "get" adjunctions, to tell you

the truth. By which I mean that I have no intuition about them; it's not so hard to understand the formal definition, but it's another thing altogether to grasp the deep significance.

In short, an adjunction is the relationship that for every "limit" of type A, there is a corresponding limit of type "B", and vice-versa, realized by a functor F that maps A to B and a functor F* that maps B to A. Since F and F* map limits to limits, they preserve more algebraic structure than just any old functors F :: A -> B and G :: B -> A. In particular, adjoint functors are "continuous". (There are very strong parallels with topology, owing to Category theory's history as a language for describing topological constructs without reference to point sets.) Every adjunction gives rise to a monad -- a generalized closure operator (topology and lattice theory are very intimately related). In particular, if a category is complete (contains all its limits), then it will have the same structure as the monad generated by an adjunction. There are some good videos on youtube for gaining intuition about some of these issues: http://www.youtube.com/watch?v=loOJxIOmShE&feature=related is a good place to start the series.