beuke.org

A personal blog about computer science topics.

Category
Collection of Objects Linked by Arrows
Posted on Oct 2 2023 ~ 10 min read
#category theory  #haskell 


Functor Functor Applicative Applicative Functor->Applicative Traversable Traversable Functor->Traversable Applicative->Traversable Alternative Alternative Applicative->Alternative Monad Monad Applicative->Monad Apply Apply Apply->Applicative Semigroup Semigroup Semigroup->Apply Monoid Monoid Semigroup->Monoid MonadPlus MonadPlus Monad->MonadPlus MonadFix MonadFix Monad->MonadFix ArrowApply ArrowApply Monad->ArrowApply Monoid->Applicative Monoid->Alternative Monoid->Monad Monoid->MonadPlus Category  Category Monoid->Category ArrowPlus ArrowPlus Monoid->ArrowPlus Foldable Foldable Monoid->Foldable Arrow Arrow Category->Arrow Foldable->Traversable Arrow->ArrowApply ArrowChoice ArrowChoice Arrow->ArrowChoice ArrowZero ArrowZero Arrow->ArrowZero ArrowZero->ArrowPlus

A category C \mathcal{C} consists of a collection of objects, denoted Obj ( C ) \text{Obj}(\mathcal{C}) and, for every two objects A , B Obj ( C ) A, B \in \text{Obj}(\mathcal{C}) , a set of morphisms Hom ( A , B ) \text{Hom}(A,B) , also called hom-sets, satisfying the following properties:

  • For every three objects A , B , C Obj ( C ) A,B,C \in \text{Obj}(\mathcal{C}) , there exist a binary operation \circ , called composition of morphisms, that satisfies the composition law:

    • : Hom ( B , C ) × Hom ( A , B ) Hom ( A , C ) \circ : \text{Hom}(B,C) \times \text{Hom}(A,B) \rightarrow \text{Hom}(A,C) , that can be written as: ( g , f ) g     f (g,f) \rightarrow g\ \circ\ f
  • Composition is associative: for all A , B , C , D Obj ( C ) , f Hom ( B , C ) A,B,C,D \in \text{Obj}(\mathcal{C}), f \in \text{Hom}(B,C) , g Hom ( A , B ) g \in \text{Hom}(A,B) , h Hom ( D , A ) h \in \text{Hom}(D,A) we have:

    • f ( g h ) = ( f g ) h f \circ (g \circ h) = (f \circ g) \circ h
  • For each A Obj ( C ) A \in \text{Obj}(\mathcal{C}) , there is a unique element 1 A Hom ( A , A ) 1_{A} \in \text{Hom}(A,A) (identity morphism), such that, for every B Obj ( C ) B \in \text{Obj}(\mathcal{C}) , we have left and right unit laws:

    • f 1 A = f f \circ 1_{A} = f for all f Hom ( A , B ) f \in \text{Hom}(A, B)
    • 1 A f = f 1_{A} \circ f = f for all f Hom ( B , A ) f \in \text{Hom}(B,A)

It is common to express A C A \in \mathcal{C} instead of A Obj ( C ) A \in \text{Obj}(\mathcal{C}) and when indicating f f is a function from A A to B B , it’s typically written as f : A B f: A \rightarrow B rather than f Hom ( A , B ) f \in \text{Hom}(A,B) .

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 A , B , C A, B, C and collection of morphisms denoted f , g , g f f, g, g \circ f , 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 1 A 1_{A} and 1 A 1'_{A} is an identity morphism. Then by left and right unit laws we have: 1 A 1 A = 1 A 1'_{A} \circ 1_{A} = 1'_{A} and 1 A 1 A = 1 A 1'_{A} \circ 1_{A} = 1_{A} , hence 1 A = 1 A 1 A = 1 A 1'_{A} = 1'_{A} \circ 1_{A} = 1_{A}

\pmb{\scriptstyle \square}

In Coq.
Section Category.
  Variable Obj : Type.
  Variable Hom : Obj -> Obj -> Type.

  Variable composition : forall {X Y Z : Obj},
      Hom Y Z -> Hom X Y -> Hom X Z.
  Notation "g o f" := (composition g f) (at level 50).

  Variable id : forall {X : Obj}, Hom X X.

  Hypothesis id_left : forall {X Y : Obj} (: Hom X Y), id o f = f.
  Hypothesis id_right : forall {X Y : Obj} (: Hom X Y), f o id = f.

  Theorem id_unique : forall {X : Obj} (id1 id2 : Hom X X),
        (forall {Y : Obj} (: Hom Y X), id1 o f = f) ->
        (forall {Y : Obj} (: Hom X Y), f o id1 = f) ->
        (forall {Y : Obj} (: Hom Y X), id2 o f = f) ->
        (forall {Y : Obj} (: Hom X Y), f o id2 = f) ->
        id1 = id2.
    Proof.
      intros X id1 id2 H1 H2 H3 H4.
      transitivity (id o id1).
      - symmetry.
        apply id_left.
      - transitivity (id o id2).
        + rewrite H2.
          symmetry.
          rewrite H4.
          reflexivity.
        + apply id_left.
    Qed.
End Category.

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.

class Category cat where
    -- the identity morphism
    --    Hom(A, A)
    id :: a `cat` a

    -- morphism composition
    --      Hom(B, C)   ×   Hom(A, B)  →  Hom(A, C)
    (.) :: (`cat` c) -> (`cat` b) -> (`cat` c)

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:

instance Category (->) where
    id :: a -> a
    id x = x

    (.) :: (-> c) -> (-> b) -> a -> c
    g . f = \-> g (f x)

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:

id . f = f . id = f       -- left and right identity law
(. g) . h = f . (. h) -- composition is associative

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.

newtype Kleisli m a b = Kleisli {
    runKleisli :: a -> m b
}

instance Monad m => Category (Kleisli m) where
    id :: Kleisli m a a
    id = Kleisli return

    (.) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c
    Kleisli f . Kleisli g = Kleisli (join . fmap g . f)

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:

(<=<) :: Monad m => (-> m c) -> (-> m b) -> (-> m c)
(<=< f) a = f a >>= g

-- m >>= f = (f <=< return) m

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:

ghci> (show . (*2) . sqrt . (+2) . abs) 14
"8.0"

ghci> import Control.Monad
ghci> (Just . (+2)) <=< (Just 2 >>=) $ return
Just 4

ghci> putStrLn <=< (getLine >>=) $ return
Hello World
Hello World

Here are some more examples:

  • S e t \mathbf{Set} , the category of sets and set functions
  • M o n \mathbf{Mon} , the category of monoids and monoid morphisms
  • G r p \mathbf{Grp} , the category of groups and group morphisms
  • R n g \mathbf{Rng} , the category of rings and ring morphisms
  • G r p h \mathbf{Grph} , the category of graphs and graph morphisms
  • T o p \mathbf{Top} , the category of topological spaces and continuous maps
  • P r e o r d \mathbf{Preord} , the category of preorders and order preserving maps
  • C P O \mathbf{CPO} , the category of complete partial orders and continuous functions
  • C a t \mathbf{Cat} , 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


  1. 0.The diagram displayed at the top of this post is a modified version of Brent Yorgey's Typeclassopedia diagram
  2. 1.Control.Category