Personal tools

Category theory

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m
(Converting HaWiki page, reorganizing)
Line 3: Line 3:
__TOC__
__TOC__
-
== Foundations ==
 
-
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'').
+
==Defintion of a category==
-
HaWiki's [http://www.haskell.org/hawiki/CategoryTheory CategoryTheory] is also a good theoretical introduction, and besides that, it explains how concepts of category theory are important in Haskell programming.
 
-
[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].
+
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 [[#Foundations]] 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 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
a
to
b
are Haskell functions of type
a -> b
. Various other Haskell structures can be used make it a Cartesian closed category.

Contents


1 Defintion of a category

A category \mathcal{C}consists of two collections:

Ob(\mathcal{C}), the objects of \mathcal{C}

Ar(\mathcal{C}), the arrows of \mathcal{C} (which are not the same as Arrows defined in GHC)

Each arrow f in Ar(\mathcal{C}) has a domain, dom f, and a codomain, cod f, each chosen from Ob(\mathcal{C}). The notation f\colon A \to B means f is an arrow with domain A and codomain B. Further, there is a function \circ called composition, such that g \circ f is defined only when the codomain of f is the domain of g, and in this case, g \circ f has the domain of f and the codomain of g.

In symbols, if f\colon A \to B and g\colon B \to C, then g \circ f \colon A \to C.

Also, for each object A, there is an arrow \mathrm{id}_A\colon A \to A, (often simply denoted as 1 or id, when there is no chance of confusion).

1.1 Axioms

The following axioms must hold for \mathcal{C} to be a category:

  1. If f\colon A \to B then f \circ \mathrm{id}_A = \mathrm{id}_B\circ f = f (left and right identity)
  2. If f\colon A \to B and g \colon B \to C and h \colon C \to D, then h \circ (g \circ f) = (h \circ g) \circ f (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.

3 See also

Retrieved from "http://www.haskell.org/haskellwiki/Category_theory"

Category: Theoretical foundations