Difference between revisions of "Category theory"

From HaskellWiki
Jump to: navigation, search
m (Link to Wikipedia's list of category theory topics was broken)
m (typo)
Line 6: Line 6:
The Haskell wikibooks has [http://en.wikibooks.org/wiki/Haskell/Category_theory an introduction to Category theory], written specifically with Haskell programmers in mind.
The Haskell wikibooks has [http://en.wikibooks.org/wiki/Haskell/Category_theory an introduction to Category theory], written specifically with Haskell programmers in mind.
==Defintion of a category==
==Definition of a category==

Revision as of 16:59, 22 April 2008

Haskell theoretical foundations

Mathematics - Category theory
Research - Curry/Howard/Lambek

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

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.

The Haskell wikibooks has an introduction to Category theory, written specifically with Haskell programmers in mind.

Definition 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 \mathrm{id}, when there is no chance of confusion).


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)

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.

Haskell libraries and tools

See also