A category consists of a collection of objects, denoted and, for every two objects , a set of morphisms , also called hom-sets, satisfying the following properties:
-
For every three objects , there exist a binary operation , called composition of morphisms, that satisfies the composition law:
- , that can be written as:
-
Composition is associative: for all , , we have:
-
For each , there is a unique element (identity morphism), such that, for every , we have left and right unit laws:
- for all
- for all
It is common to express instead of and when indicating is a function from to , it’s typically written as rather than .
A category is a very general concept, the objects and morphisms can be anything, as long as they adhere to the stated conditions. The following is an example category with a collection of objects and collection of morphisms denoted , and the loops are the identity morphisms.
\begin{xy} \xymatrix{ A \ar@(l,u)^{1_A}[] \ar_{g\ \circ\ f}[dr] \ar^f[r] & B \ar@(u,r)^{1_B}[] \ar^g[d]\\ &C \ar@(d,r)_{1_C}[] } \end{xy}One interesting aspect that follows from the left and right unit laws is that the identity morphism is unique, so there really is just one way to loop back to itself.
Proposition. The identity morphism is unique.
Proof. Suppose that each of and is an identity morphism. Then by left and right unit laws we have: and , hence
In Coq.
Example
In Haskell, Category is a type class that abstracts the concept of a mathematical category. In the context of Haskell, types are considered as objects and functions as morphisms.
In Haskell, one traditionally works in the category (->) called Hask, in which any Haskell type is an object and functions are morphisms. We can implement Hask as follows:
As we can see, cat
has simply been replaced by Haskell arrows. The id
function is the identity morphism that leaves the object unchanged. The (.)
function is a composition of morphisms, which obey category laws in pseudo notation:
Haskell faces some challenges when considered in its entirety as category Hask due to features like non-termination and bottom values. Therefore, when speaking about Hask it is often referred to a constrained subset of Haskell that excludes these problematic aspects. Specifically, this subset only permits terminating functions operating on finite values. It also resolves other subtleties. In essence, this pragmatic subset removes everything preventing Haskell from being modeled as a category.
The Category typeclass[1] can also be used with other structures that can be viewed as categories, not just functions between types. For example, it can be used with the Kleisli category of a monad, where morphisms are functions of type a -> m b
. The objects in this category are identical to the types in Haskell as found in Hask
. However, the transformation between these entities are represented by Kleisli arrows.
Kleisli arrows are a way of composing monadic programs. They are a notational feature that can be useful, but they don’t provide any additional functionality beyond what the monad already provides. The use of this syntax in Haskell, since it overwrites id
and standard function composition (.)
, can be quite confusing if used in this manner. Instead, Kleisli composition is often defined using the “fish” operator, as shown below:
As we can see <=< can be expressed in terms of >>=
and vice versa, hence they form an isomorphism. All of the above is already implemented in the standard Haskell library, so you can simply open an interactive Haskell interpreter (ghci) and test the following examples:
Here are some more examples:
- , the category of sets and set functions
- , the category of monoids and monoid morphisms
- , the category of groups and group morphisms
- , the category of rings and ring morphisms
- , the category of graphs and graph morphisms
- , the category of topological spaces and continuous maps
- , the category of preorders and order preserving maps
- , the category of complete partial orders and continuous functions
- , the category of categories and functors
- Monoids are themselves one-object categories
- 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)
References
- 0.The diagram displayed at the top of this post is a modified version of Brent Yorgey's Typeclassopedia diagram ↩
- 1.Control.Category ↩