Category theory
From HaskellWiki
(oops, already here...) 

(19 intermediate revisions by 13 users not shown) 
Revision as of 11:26, 16 September 2012
"Haskell category", of which the objects are Haskell types, and the morphisms from typesContents 
The Haskell wikibooks has an introduction to Category theory, written specifically with Haskell programmers in mind.
1 Definition of a category
A category consists of two collections:
Ob, the objects of
Ar, the arrows of (which are not the same as Arrows defined in GHC)
Each arrow f in Ar has a domain, dom f, and a codomain, cod f, each chosen from Ob. The notation means f is an arrow with domain A and codomain B. Further, there is a function called composition, such that is defined only when the codomain of f is the domain of g, and in this case, has the domain of f and the codomain of g.
In symbols, if and , then .
Also, for each object A, there is an arrow , (often simply denoted as 1 or id, when there is no chance of confusion).
1.1 Axioms
The following axioms must hold for to be a category:
 If then (left and right identity)
 If and and , then (associativity)
1.2 Examples of categories
 Set, the category of sets and set functions.
 Mon, the category of monoids and monoid morphisms.
 Monoids are themselves oneobject categories.
 Grp, the category of groups and group morphisms.
 Rng, the category of rings and ring morphisms.
 Grph, the category of graphs and graph morphisms.
 Top, the category of topological spaces and continuous maps.
 Preord, the category of preorders and order preserving maps.
 CPO, the category of complete partial orders and continuous functions.
 Cat, the category of categories and functors.
 Hask
 the category of data types and functions on data structures
 the category of functions and data flows (~ data flow diagram)
 the category of stateful objects and dependencies (~ object diagram)
 the category of values and value constructors
 the category of states and messages (~ state diagram)
1.3 Further definitions
With examples in Haskell at:
2 Categorical programming
Catamorphisms and related concepts, categorical approach to functional programming, categorical programming. Many materials cited here refer to category theory, so as an introduction to this discipline see the #See also section.
 Erik Meijer, Maarten Fokkinga, Ross Paterson: Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. See also related documents (in the CiteSeer page). Understanding the article does not require knowledge of category theory—the paper is selfcontained with regard to understanding catamorphisms, anamorphisms and other related concepts.
 Roland Backhouse, Patrik Jansson, Johan Jeuring and Lambert Mertens. Generic Programming  an Introduction: Detailed introduction to categorial sums, product, polynomial functors and folds for the purpose of generic programming. Supplements the bananas paper.
 Varmo Vene and Tarmo Uustalu: Functional Programming with Apomorphisms / Corecursion
 Varmo Vene: Categorical Programming with Inductive and Coinductive Types. The book gives Haskell examples to illustrate the deep categorical theory topic.
 Tatsuya Hagino: A Categorical Programming Language
 Charity, a categorical programming language implementation.
 Deeply uncurried products, as categorists might like them article mentions a conjecture: relatedness to Combinatory logic
3 Haskell libraries and tools
 Category extras by David Menendez: libraries for e.g. comonads, infinite data types.
4 Books
 Michael Barr and Charles Wells: Toposes, Triples and Theories. The online, freely available book is both an introductory and a detailed description of category theory. It also contains a categorytheoretical description of the concept of monad (but calling it a triple instead of monad).
 R. F. C. Walters: Categories and Computer Science. Category Theory has, in recent years, become increasingly important and popular in computer science, and many universities now introduce Category Theory as part of the curriculum for undergraduate computer science students. Here, the theory is developed in a straightforward way, and is enriched with many examples from computer science.
 Arbib&Manes: Arrow, Structures and Functors  The Categorical Imperative. (c)1975 Academic Press, ISBN 0120590603. Sadly now out of print but very little prerequisite knowledge is needed. It covers monads and the Yoneda lemma.
5 See also
 Michael Barr and Charles Wells have a paper that presents category theory from a computerscience perspective, assuming no prior knowledge of categories.
 A Gentle Introduction to Category Theory  the calculational approach written by Maarten M Fokkinga.
 Wikipedia has a good collection of categorytheory articles, although, as is typical of Wikipedia articles, they are rather dense.