Category theory: Difference between revisions

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.

Defintion of a category

A category $C$ consists of two collections:

Ob $(C)$ , the objects of $C$

Ar $(C)$ , the arrows of $C$ (which are not the same as Arrows defined in GHC)

Each arrow $f$ in Ar $(C)$ has a domain, dom $f$ , and a codomain, cod $f$ , each chosen from Ob $(C)$ . The notation $f : 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 : A \to B$ and $g : B \to C$ , then $g \circ f : A \to C$ .

Also, for each object $A$ , there is an arrow ${i d}_{A} : A \to A$ , (often simply denoted as $1$ or $i d$ , when there is no chance of confusion).

Axioms

The following axioms must hold for $C$ to be a category:

If $f : A \to B$ then $f \circ {i d}_{A} = {i d}_{B} \circ f = f$ (left and right identity)
If $f : A \to B$ and $g : B \to C$ and $h : C \to D$ , then $h \circ (g \circ f) = (h \circ g) \circ f$ (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 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

@@ Line 3: / Line 3: @@
 __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 ==
-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.
 * 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://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]]