(Converting HaWiki page, reorganizing)
m (→Defintion of a category: link)
Revision as of 18:40, 7 October 2006Category 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
1 Defintion of a category
A category consists of two collections:
Ob, the objects of
Each arrow f in Ar has a domain, dom f, and a codomain, cod f, each chosen from Ob. The notation means f is an arrow with domain A and codomain B. Further, there is a function called composition, such that is defined only when the codomain of f is the domain of g, and in this case, has the domain of f and the codomain of g.
In symbols, if and , then .
Also, for each object A, there is an arrow , (often simply denoted as 1 or id, when there is no chance of confusion).
The following axioms must hold for to be a category:
- If then (left and right identity)
- If and and , then (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.
- 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
3 See also
- Michael Barr and Charles Wells have a paper that presents category theory from a computer science perspective, assuming no prior knowledge of categories.
- Michael Barr and Charles Wells: 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).
- A Gentle Introduction to Category Theory - the calculational approach written by Maarten M Fokkinga.
- Wikipedia has a good collection of category theory articles, although, typically of Wikipedia, they're a rather dense introduction.