# Difference between revisions of "Category theory"

BrettGiles (talk | contribs) (Add infobox) |
m (fixed typos, some rewording) |
||

Line 1: | Line 1: | ||

{{Foundations infobox}} |
{{Foundations infobox}} |
||

− | '''Category theory''' can be helpful in understanding Haskell's type system. There |
+ | '''Category theory''' can be helpful in understanding Haskell's type system. There exists a "Haskell category", of which the objects are Haskell types, and the morphisms from types <hask>a</hask> to <hask>b</hask> are Haskell functions of type <hask>a -> b</hask>. Various other Haskell structures can be used to make it a Cartesian closed category. |

__TOC__ |
__TOC__ |
||

Line 67: | Line 67: | ||

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. |
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 |
+ | * 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 knowledge of category theory—the paper is self-contained with regard to understanding catamorphisms, anamorphisms 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] |
||

− | * Varmo Vene: [http://www.cs.ut.ee/~varmo/papers/thesis.pdf Categorical Programming with Inductive and Coinductive Types]. The book |
+ | * Varmo Vene: [http://www.cs.ut.ee/~varmo/papers/thesis.pdf Categorical Programming with Inductive and Coinductive Types]. The book gives Haskell examples to illustrate the deep categorical theory topic. |

* Tatsuya Hagino: [http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf A Categorical Programming Language] |
* Tatsuya Hagino: [http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf A Categorical Programming Language] |
||

* [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. |
||

Line 76: | Line 76: | ||

==See also== |
==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 |
+ | * 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 |
+ | *Michael Barr and Charles Wells: [http://www.cwru.edu/artsci/math/wells/pub/ttt.html Toposes, Triples and Theories]. The online, freely available book is both an introductory and a detailed description of category theory. It also contains a category-theoretical description of the concept of ''monad'' (but calling it a ''triple'' instead of ''monad''). |

*[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]. |
*[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 |
+ | * Wikipedia has a good [http://en.wikipedia.org/List_of_category_theory_topics collection of category-theory articles], although, as is typical of Wikipedia articles, they are rather dense. |

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

## Revision as of 18:31, 3 February 2007

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

to `b`

are Haskell functions of type `a -> b`

. Various other Haskell structures can be used to make it a Cartesian closed category.

## Contents

## 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 in Ar has a domain, dom , and a codomain, cod , each chosen from Ob. The notation means is an arrow with domain and codomain . Further, there is a function called composition, such that is defined only when the codomain of is the domain of , and in this case, has the domain of and the codomain of .

In symbols, if and , then .

Also, for each object , there is an arrow , (often simply denoted as or , when there is no chance of confusion).

### Axioms

The following axioms must hold for to be a category:

- If then (left and right identity)
- If and and , then (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:

## 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 self-contained with regard to understanding catamorphisms, anamorphisms 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 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

## 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, freely available book is both an introductory and a detailed description of category theory. It also contains a category-theoretical description of the concept of
*monad*(but calling it a*triple*instead of*monad*). - A Gentle Introduction to Category Theory - the calculational approach written by Maarten M Fokkinga.
- Wikipedia has a good collection of category-theory articles, although, as is typical of Wikipedia articles, they are rather dense.