Personal tools

Category theory

From HaskellWiki

Revision as of 19:53, 1 February 2007 by BrettGiles (Talk | contribs)

Jump to: navigation, search
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 is a "Haskell category", of which the objects are Haskell types, and the morphisms from types
are Haskell functions of type
a -> b
. Various other Haskell structures can be used make it a Cartesian closed category.


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