Personal tools

Category theory

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(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 is 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 make it a Cartesian closed category.
+
'''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 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 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 accompanies the deep categorical theory topic with Haskell examples.
+
* 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 science perspective, assuming no prior knowledge of categories.
+
* 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'').
+
*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 theory articles], although, typically of Wikipedia, they're a rather dense introduction.
+
* 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

Haskell theoretical foundations

General:
Mathematics - Category theory
Research - Curry/Howard/Lambek

Lambda calculus:
Alpha conversion - Beta reduction
Eta conversion - Lambda abstraction

Other:
Recursion - Combinatory logic
Chaitin's construction - Turing machine
Relational algebra

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


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