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 18:
 
* [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