# Category theory

### From HaskellWiki

m |
BrettGiles (Talk | contribs) (Converting HaWiki page, reorganizing) |
||

Line 3: | Line 3: | ||

__TOC__ | __TOC__ | ||

− | |||

− | + | ==Defintion of a category== | |

− | |||

− | + | A category <math>\mathcal{C}</math>consists of two collections: | |

+ | |||

+ | Ob<math>(\mathcal{C})</math>, the objects of <math>\mathcal{C}</math> | ||

+ | |||

+ | Ar<math>(\mathcal{C})</math>, the arrows of <math>\mathcal{C}</math> | ||

+ | (which are not the same as [[Arrows]] defined in [[GHC]]) | ||

+ | |||

+ | Each arrow <math>f</math> in Ar<math>(\mathcal{C})</math> has a | ||

+ | domain, dom <math>f</math>, and a codomain, cod <math>f</math>, each | ||

+ | chosen from Ob<math>(\mathcal{C})</math>. The notation <math>f\colon | ||

+ | A \to B</math> means <math>f</math> is an arrow with domain | ||

+ | <math>A</math> and codomain <math>B</math>. Further, there is a | ||

+ | function <math>\circ</math> called composition, such that <math>g | ||

+ | \circ f</math> is defined only when the codomain of <math>f</math> is | ||

+ | the domain of <math>g</math>, and in this case, <math>g \circ f</math> | ||

+ | has the domain of <math>f</math> and the codomain of <math>g</math>. | ||

+ | |||

+ | In symbols, if <math>f\colon A \to B</math> and <math>g\colon B \to | ||

+ | C</math>, then <math>g \circ f \colon A \to C</math>. | ||

+ | |||

+ | Also, for each object <math>A</math>, there is an arrow | ||

+ | <math>\mathrm{id}_A\colon A \to A</math>, (often simply denoted as | ||

+ | <math>1</math> or <math>\mathrm{id}</math>, when there is no chance of | ||

+ | confusion). | ||

+ | |||

+ | ===Axioms=== | ||

+ | The following axioms must hold for <math>\mathcal{C}</math> to be a category: | ||

+ | |||

+ | #If <math>f\colon A \to B</math> then <math>f \circ \mathrm{id}_A = \mathrm{id}_B\circ f = f</math> (left and right identity) | ||

+ | #If <math>f\colon A \to B</math> and <math>g \colon B \to C</math> and <math>h \colon C \to D</math>, then <math>h \circ (g \circ f) = (h | ||

+ | \circ g) \circ f</math> (associativity) | ||

+ | |||

+ | ===Examples of categories=== | ||

+ | * Set, the category of sets and set functions. | ||

+ | * Mon, the category of monoids and monoid morphisms. | ||

+ | * Monoids are themselves one-object 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. | ||

+ | |||

+ | * 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) | ||

+ | |||

+ | ===Further definitions=== | ||

+ | With examples in Haskell at: | ||

+ | * [[Category theory/Functor]] | ||

+ | * [[Category theory/Natural transformation]] | ||

== Categorical programming == | == 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 [[# | + | 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: [http://citeseer.ist.psu.edu/meijer91functional.html Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire]. See also related documents (in the CiteSeer page). Understanding the article does not require a category theory knowledge -- a self-contained material on the concept of catamorphism, anamoprhism and other related concepts. | * Erik Meijer, Maarten Fokkinga, Ross Paterson: [http://citeseer.ist.psu.edu/meijer91functional.html Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire]. See also related documents (in the CiteSeer page). Understanding the article does not require a category theory knowledge -- a self-contained material on the concept of catamorphism, anamoprhism and other related concepts. | ||

* Varmo Vene and Tarmo Uustalu: [http://citeseer.ist.psu.edu/vene98functional.html Functional Programming with Apomorphisms / Corecursion] | * Varmo Vene and Tarmo Uustalu: [http://citeseer.ist.psu.edu/vene98functional.html Functional Programming with Apomorphisms / Corecursion] | ||

Line 20: | Line 71: | ||

* [http://pll.cpsc.ucalgary.ca/charity1/www/home.html Charity], a categorical programming language implementation. | * [http://pll.cpsc.ucalgary.ca/charity1/www/home.html Charity], a categorical programming language implementation. | ||

* [http://okmij.org/ftp/Haskell/categorical-maxn.lhs Deeply uncurried products, as categorists might like them] article mentions a conjecture: relatedness to [[Combinatory logic]] | * [http://okmij.org/ftp/Haskell/categorical-maxn.lhs Deeply uncurried products, as categorists might like them] article mentions a conjecture: relatedness to [[Combinatory logic]] | ||

+ | |||

+ | ==See also== | ||

+ | |||

+ | * Michael Barr and Charles Wells have a [http://www.math.upatras.gr/~cdrossos/Docs/B-W-LectureNotes.pdf paper] that presents category theory from a computer science perspective, assuming no prior knowledge of categories. | ||

+ | *Michael Barr and Charles Wells: [http://www.cwru.edu/artsci/math/wells/pub/ttt.html Toposes, Triples and Theories]. The online free available book is both an introductory and a detailed description of category theory. By the way, it is also a category theoretical descripton of the concept of ''monad'' (the book uses another name instead of monad: ''triple''). | ||

+ | *[http://wwwhome.cs.utwente.nl/~fokkinga/mmf92b.html A Gentle Introduction to Category Theory - the calculational approach] written by [http://wwwhome.cs.utwente.nl/~fokkinga/index.html Maarten M Fokkinga]. | ||

+ | * Wikipedia has a good [http://en.wikipedia.org/List_of_category_theory_topics collection of category theory articles], although, typically of Wikipedia, they're a rather dense introduction. | ||

[[Category:Theoretical foundations]] | [[Category:Theoretical foundations]] |

## Revision as of 02:06, 2 October 2006

**Category theory**can be helpful in understanding Haskell's type system. There is a "Haskell category", of which the objects are Haskell types, and the morphisms from types

## Contents |

## 1 Defintion 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 one-object 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.

- 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 a category theory knowledge -- a self-contained material on the concept of catamorphism, anamoprhism and other related concepts.
- Varmo Vene and Tarmo Uustalu: Functional Programming with Apomorphisms / Corecursion
- Varmo Vene: Categorical Programming with Inductive and Coinductive Types. The book accompanies the deep categorical theory topic with Haskell examples.
- 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 See also

- Michael Barr and Charles Wells have a paper that presents category theory from a computer science perspective, assuming no prior knowledge of categories.
- Michael Barr and Charles Wells: Toposes, Triples and Theories. The online free available book is both an introductory and a detailed description of category theory. By the way, it is also a category theoretical descripton of the concept of
*monad*(the book uses another name instead of monad:*triple*). - A Gentle Introduction to Category Theory - the calculational approach written by Maarten M Fokkinga.
- Wikipedia has a good collection of category theory articles, although, typically of Wikipedia, they're a rather dense introduction.