Gytis Žilinskas | 25 Nov 22:41 2012
Picon

Category Theory and Haskell

Greetings,

I'm only taking my very first steps learning Haskell, but I believe
that this mailing list might be appropriate for my question.

How difficult would it be to study category theory and simultaneously
come up with Haskell examples of various results that it presents?

I believe some background is in order. I am a second year maths
student (well actually I'm in-between 2nd and 3rd, but let's not delve
into details). I have also done some 2nd year CS courses so I have
some background in that too. My general interests seem to lie
somewhere between maths and compsci (I guess theoretical cs is the
word for it), but it doesn't look like there is a good way to study
the subject at an undergrad level. Most CompSci undergrad courses seem
to concentrate too much on the trade of being a programmer and only
present the basics of the theoretical results. While maths departments
seem to be reluctant to make room in the undergrad curriculum for a
huge subject that, after all, is maths.

Recently, whenever I try reading up on something that looks like an
exciting topic to me, I hit my head against category theory. That
seems to suggest, that I should check it out, as it might be a fun
subject to study, or at least provide valuable insights elsewhere.

I've tried looking for some resources online. Most of them are
outright scary and clearly have prerequisites that I lack. Some a
little bit more accessible. Overall, various similar questions on
different stackexchanges and even some old discussions on this mailing
list, imply that to study category theory one has to know many
(Continue reading)

Alexander Solla | 26 Nov 02:11 2012
Picon

Re: Category Theory and Haskell

The general idea of category theory is to come up with formalizations of common abstract "patterns" found in mathematical constructs.  For example, there are homomorphisms of groups, vector spaces (under linear transformations), topological spaces (under continuous functions), etc.  Category theory abstracts these into the notions of a "morphism" or an "arrow" (which correspond to the homomorphisms) and "objects" (which correspond to particular spaces of a particular kind).  Objects and morphisms are (globally) taken to be undefined primitives, much how sets are undefined primitives in set theory.

With the notion of a category in place, we can begin constructing arbitrary categories, or proving that algebras satisfy the category axioms.  It is possible to define mappings between categories -- suitably nice mappings are called "functors", and are morphisms in the (small) Category of Categories.

The interesting thing about category theory is how rich it can be.  It had its origins in algebraic topology, but algebraic topology has rich connections with the theory of lattices and order, set theory, logic, group theory, computation, etc.  For example, topological nets and filters can be recast as categories, and limits in these categories generalize to the categorical notion of a limit.  Similarly, a topology's "closure operator" can be recast in terms of monads -- 'join' witnesses that a monad is idempotent, in the sense that an (m a) and an (m (m a)) are the same "kind" of structure.

Check out Goldblatt's "Topoi - A Categorical Analysis of Logic".  It focuses specifically on modeling logics using categorical methods, and the preliminary chapters are a fine introduction to the basics.

I'm sure you can turn that into a semester course. 
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
John Wiegley | 26 Nov 02:30 2012

Re: Category Theory and Haskell

>>>>> Gytis Žilinskas <gytis.zilinskas <at> gmail.com> writes:

> How difficult would it be to study category theory and simultaneously come
> up with Haskell examples of various results that it presents?

There are some aspects of CT that you will not be able to express in Haskell
easily (try encoding the forgetful functor, for instance).  But there are
other things which translate quite nicely.  As one example, I've been using
Haskell to explore the connection between adjunctions and monads, and have
found it quite rewarding.  My efforts so far are here:

    https://github.com/jwiegley/posts/blob/master/Adjunctions%20in%20Haskell/Adjunction.hs

What I found most compelling from that code is I only need a minimal
definition of the Prod ⊣ Hom adjunction, (ε and η -- and their definitions are
trivial), I get all the behavior of the well-known State monad, whose typical
implementation via >>= is rather tricky.

Doing this exploration in Haskell -- with the aid of the type-checker -- made
certain connections clear that were difficult to see in the abstract.  And it
was plenty of fun besides. :)

Happy brain spelunking,
--

-- 
John Wiegley
FP Complete                         Haskell tools, training and consulting
http://fpcomplete.com               johnw on #haskell/irc.freenode.net

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
AUGER Cédric | 30 Nov 09:49 2012
Picon

Re: Category Theory and Haskell

Le Sun, 25 Nov 2012 21:41:47 +0000,
Gytis Žilinskas <gytis.zilinskas <at> gmail.com> a écrit :

> Greetings,
> 
> I'm only taking my very first steps learning Haskell, but I believe
> that this mailing list might be appropriate for my question.
> 
> How difficult would it be to study category theory and simultaneously
> come up with Haskell examples of various results that it presents?
> 
> I believe some background is in order. I am a second year maths
> student (well actually I'm in-between 2nd and 3rd, but let's not delve
> into details). I have also done some 2nd year CS courses so I have
> some background in that too. My general interests seem to lie
> somewhere between maths and compsci (I guess theoretical cs is the
> word for it), but it doesn't look like there is a good way to study
> the subject at an undergrad level. Most CompSci undergrad courses seem
> to concentrate too much on the trade of being a programmer and only
> present the basics of the theoretical results. While maths departments
> seem to be reluctant to make room in the undergrad curriculum for a
> huge subject that, after all, is maths.
> 
> Recently, whenever I try reading up on something that looks like an
> exciting topic to me, I hit my head against category theory. That
> seems to suggest, that I should check it out, as it might be a fun
> subject to study, or at least provide valuable insights elsewhere.
> 
> I've tried looking for some resources online. Most of them are
> outright scary and clearly have prerequisites that I lack. Some a
> little bit more accessible. Overall, various similar questions on
> different stackexchanges and even some old discussions on this mailing
> list, imply that to study category theory one has to know many
> examples from other advanced fields, in order to see the patterns that
> category theory describes. Now I obviously lack that. Some basic group
> theory, linear algebra, real/complex analysis and metric spaces is
> pretty much all I've got. Moreover, most sources say that without the
> knowledge of examples - category theory is an extremely dry subject to
> study. Therefore, my preliminary plan is the following:
> 
> Read:
> * Barry Mazur - When is one thing equal to some other thing?
> * Conceptual mathematics : a first introduction to categories / F.
> William Lawvere, Stephen H. Schanuel. (People say that it is rather
> lightweight, but at this point my goal is to see the general idea of
> category theory and get some taste of it)
> 
> Then, in the 2nd semester, I have an option of taking a self-study
> module, and if I don't get bored by cats by that time - it would be
> great to invest some more time in it (or rather, I'll do anything to
> avoid applied maths *shudder*). However, I'll need to present my case
> before the department staff and this, basically, is why I'm here.
> Right now, it looks like the main argument against me, would be that I
> can't appreciate the subject since I lack the fundamentals in other
> areas of maths. So I was hoping, I could convince them that everything
> I lack example wise - I'll find in Haskell. Okay, "everything" might
> be too strong of a statement, but I don't really know what I'm talking
> about so it's a bit difficult to calibrate. Could you comment whether
> Haskell would serve me well for this purpose?
> 
> I've also seen these lecture notes:
> http://www.haskell.org/haskellwiki/User:Michiexile/MATH198. But I'm
> not sure if they won't be deemed too comp sci targeted. Therefore, I'm
> putting more hope into "The Joy of Cats" which, at least according to
> the first few pages, doesn't assume any prior knowledge that I don't
> have.
> 
> So that's that, I would appreciate any advice you could give.
> 
> Gytis
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

 I would suggest reading Saunders MacLane book (Categories for the
working mathematician). I am happy to have bought this one. But do not
be impressed by the given exercises, they have no correction, and some
are not understandable for a new comer. (The first exercise of the book
talks about Lie groups and algebra, that is hard to start with). So for
the examples, only read the ones involving the "Set", "Ab", "Rng"
categories if you are not used to the other ones.
 The terminology is also annoying, as the formalization was done rather
lately, and some concepts merged, so for instance the concept of limit.
In the terminology, you have "limit"="inverse limit" and
"colimit"="direct limit" which is quite confusing (but MacLane is not
at fault for that).

Some other resource is the categories channel on IRC (Freenode), the
nLab wiki (and Wikipedia of course).

You may also be interested in Agda, which would help in using the laws
of each category (not ensured by raw Haskell). I learned Coq rather
than Agda, so you can also try it too.

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

Gmane