4 ms·

Category theory is much beloved of functional programming researchers, at least in my computer science department, mostly as a way of analysing and conceptualis

Category theory is much beloved of functional programming researchers, at least in my computer science department, mostly as a way of analysing and conceptualising type theory. For example, one of my friends is working on showing equivalences between I/O in Haskell (purely functional) and Lucid (demand-driven dataflow). Category theory shows a neat relationship between the models and a way to move between them.

tydok 15y ago
For a demonstration, I recommend the "Going Deep" show episodes of Erik Meijer and Brian Beckman, http://channel9.msdn.com/search?term=erik+meijer+brian+beckman&type=All http://channel9.msdn.com/search?term=erik+meijer+brian+beckm... plus the book "Algebra of Programming" by Richard Bird, Oege de Moor http://www.amazon.com/Algebra-Programming-Prentice-Hall-International-Computer/dp/013507245X http://www.amazon.com/Algebra-Programming-Prentice-Hall-Inte...
chalst 15y ago
Not just FP researchers, although they are a particularly good fit because typed lambda calculi are Cartesian closed categories. Other areas of CS where category theory is applied: 1. Algebraic data types and modules. E.g., http://reperiendi.wordpress.com/2007/11/03/category-theory-for-the-java-programmer/ http://reperiendi.wordpress.com/2007/11/03/category-theory-f... 2. Semantics of non-terminating programs. E.g., http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2502 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2... 3. Semantics of concurrency. E.g., http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.8814 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.8... These are probably the most important places, besides FP, where categories are used in computer science, but there are others: logic programming, computer graphics and vision, knowledge representation, ontology, &c. The applications to FP are most visible because (i) Haskell monads are a little slice of category theory, so users as well as language designers need to get their hands dirty[+], and (ii) it's very natural to want a realisation of a categorical semantics to have first-class functions, ideally lazy functions, because that makes the realisation easier. [+] Categorical abstractions in semantics are dirty, don't let people fool you into believing they are pure and clean.
xyzzyz 15y ago
So one should introduce category theory along with its usage. Category theory makes little sense without it -- it turns to mundane symbol (or rather, diagram) manipulation. The category-theoretical notions do not seem to have any relevance if you do not know what other notions they try to generalize. What I mean is that it is more natural to notice that various products in all kind of mathematical structures have some universal property in common, than to say that these are examples of categorical notion of product. Or, it is more natural to notice that van Kampen's theorem really says something about connection between fundamental groups of a space and its subspaces, than to say that fundamental grupoid of a space is a colimit of a diagram created by fundamental grupoids of certain families of subspaces, with arrows being induced by inclusions. The second approach in case of van Kampen theorem (and many more, actually) is useful when you want to prove or use van Kampen theorem, because it is a bit easier to prove an universal property of a colimit than to prove that the fundamental group of a space is a free product product of the fundamental group of its subspaces with an amalgamation along fundamental group of their intersection. Nevertheless, categorical approach does not provide you with the intuition which initially led to the formulation of this theorem. I believe that the case is similar with your friend's work -- it's his intuition and insight which led him to notice this equivalence, and category theory only helps him formulate his thoughts in an elegant way. Learning category theory before learning more substantial facts is in my opinion going totally in backward order. Or maybe I'm just an (metaphorically) old grump and refuse to acknowledge the revolution just like mathematicians in the beginning of twentieth century were refusing to accept set theory.
- mjw 15y ago
  I'm inclined to agree. I've tried a few times to learn category theory in the abstract, and struggled to motivate myself when I couldn't clearly "see" the structure and the application, in categories (like Hask or Vect) which I know reasonably well. I'm glad it exists though, so I know where to look if I want some kind of deeper unifying intuition about structural ideas in whatever area of maths I'm studying, which might help me connect them to other areas, and as I read more graduate-level maths I imagine more of these opportunities will crop up. Perhaps it's one of those things where it's helpful to learn the basic definitions early on, and their implications in categories (initially probably fairly straightforward ones) which you already know. But then, just keep it gently percolating while you study other things, rather than trying to force it and make sense of adjoint functors etc before you've studied enough applications to justify the abstraction.

tydok 15y ago

For a demonstration, I recommend the "Going Deep" show episodes of Erik Meijer and Brian Beckman, http://channel9.msdn.com/search?term=erik+meijer+brian+beckman&type=All http://channel9.msdn.com/search?term=erik+meijer+brian+beckm... plus the book "Algebra of Programming" by Richard Bird, Oege de Moor http://www.amazon.com/Algebra-Programming-Prentice-Hall-International-Computer/dp/013507245X http://www.amazon.com/Algebra-Programming-Prentice-Hall-Inte...

chalst 15y ago

Not just FP researchers, although they are a particularly good fit because typed lambda calculi are Cartesian closed categories. Other areas of CS where category theory is applied: 1. Algebraic data types and modules. E.g., http://reperiendi.wordpress.com/2007/11/03/category-theory-for-the-java-programmer/ http://reperiendi.wordpress.com/2007/11/03/category-theory-f... 2. Semantics of non-terminating programs. E.g., http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2502 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.2... 3. Semantics of concurrency. E.g., http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.8814 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.62.8... These are probably the most important places, besides FP, where categories are used in computer science, but there are others: logic programming, computer graphics and vision, knowledge representation, ontology, &c. The applications to FP are most visible because (i) Haskell monads are a little slice of category theory, so users as well as language designers need to get their hands dirty[+], and (ii) it's very natural to want a realisation of a categorical semantics to have first-class functions, ideally lazy functions, because that makes the realisation easier. [+] Categorical abstractions in semantics are dirty, don't let people fool you into believing they are pure and clean.

xyzzyz 15y ago

So one should introduce category theory along with its usage. Category theory makes little sense without it -- it turns to mundane symbol (or rather, diagram) manipulation. The category-theoretical notions do not seem to have any relevance if you do not know what other notions they try to generalize. What I mean is that it is more natural to notice that various products in all kind of mathematical structures have some universal property in common, than to say that these are examples of categorical notion of product. Or, it is more natural to notice that van Kampen's theorem really says something about connection between fundamental groups of a space and its subspaces, than to say that fundamental grupoid of a space is a colimit of a diagram created by fundamental grupoids of certain families of subspaces, with arrows being induced by inclusions. The second approach in case of van Kampen theorem (and many more, actually) is useful when you want to prove or use van Kampen theorem, because it is a bit easier to prove an universal property of a colimit than to prove that the fundamental group of a space is a free product product of the fundamental group of its subspaces with an amalgamation along fundamental group of their intersection. Nevertheless, categorical approach does not provide you with the intuition which initially led to the formulation of this theorem. I believe that the case is similar with your friend's work -- it's his intuition and insight which led him to notice this equivalence, and category theory only helps him formulate his thoughts in an elegant way. Learning category theory before learning more substantial facts is in my opinion going totally in backward order. Or maybe I'm just an (metaphorically) old grump and refuse to acknowledge the revolution just like mathematicians in the beginning of twentieth century were refusing to accept set theory.

mjw 15y ago
I'm inclined to agree. I've tried a few times to learn category theory in the abstract, and struggled to motivate myself when I couldn't clearly "see" the structure and the application, in categories (like Hask or Vect) which I know reasonably well. I'm glad it exists though, so I know where to look if I want some kind of deeper unifying intuition about structural ideas in whatever area of maths I'm studying, which might help me connect them to other areas, and as I read more graduate-level maths I imagine more of these opportunities will crop up. Perhaps it's one of those things where it's helpful to learn the basic definitions early on, and their implications in categories (initially probably fairly straightforward ones) which you already know. But then, just keep it gently percolating while you study other things, rather than trying to force it and make sense of adjoint functors etc before you've studied enough applications to justify the abstraction.