Defining Categories and Category Laws in Haskell

Question

I am having fun learning Category Theory by directly translating the definitions and laws to Haskell. Haskell is not Coq of course but it helps me getting an intuition for Category Theory. My question is: is the following a reasonable "translation" of a definition of a category into Haskell?

{-
  The following definition of a category is adapted from "Basic Category Theory" by Jaap van Oosten:

  A category is given by a collection of objects and a collection of morphisms.

  Each morphism has a domain and a codomain which are objects.

  One writes f:X->Y (or X -f-> Y) if X is the domain of the morphism f, and Y its codomain.

  One also writes X = dom(f) and Y = cod(f)

  Given two morphisms f and g such that cod(f) = dom(g), the composition
  of f and g, written (g f), is defined and has domain dom(f) and codomain cod(g):
  (X -f-> Y -g-> Z) = (X -(g f)-> Z)

  Composition is associative, that is: given f : X -> Y , g : Y -> Z and h : Z -> W, h (g f) = (h g) f

  For every object X there is an identity morphism idX : X -> X, satisfying
  (idX g) = g for every g : Y -> X and (f idX) = f for every f : X -> Y.
-}

module Code.CategoryTheory where

---------------------------------------------------------------------

data Category o m =
  Category
  {
  -- A category is given by a collection of objects and a collection of morphisms:
    objects    :: [o],
    morphisms  :: [m],
  -- Each morphism has a domain and a codomain which are objects:
    domain     :: m -> o,
    codomain   :: m -> o,
  -- Given two morphisms f and g such that codomain f = domain g,
  -- the composition of f and g, written (g f), is defined:
    compose    :: m -> m -> Maybe m,
  -- For every object X there is an identity morphism idX : X -> X
    identity   :: o -> m
  }

---------------------------------------------------------------------

-- Check if (Category o m) is truly a category (category laws)

is_category :: (Eq o,Eq m) => Category o m -> Bool

is_category cat =
     domains_are_objects         cat
  && codomains_are_objects       cat
  && composition_is_defined      cat
  && composition_is_associative  cat
  && identity_is_identity        cat

---------------------------------------------------------------------

-- Each morphism has a domain and a codomain which are objects:

domains_are_objects :: Eq o => Category o m -> Bool

domains_are_objects cat =
  all (\m -> elem (domain cat m) (objects cat)) (morphisms cat)

codomains_are_objects :: Eq o => Category o m -> Bool

codomains_are_objects cat =
  all (\m -> elem (codomain cat m) (objects cat)) (morphisms cat)

---------------------------------------------------------------------

-- Given two morphisms f and g such that cod(f) = dom(g),
-- the composition of f and g, written (g f), is defined
-- and has domain dom(f) and codomain cod(g)

composition_is_defined :: Eq o => Category o m -> Bool

composition_is_defined cat =
  go $ morphisms cat
  where
    go []       = True
    go (m : mx) = all (go2 m) mx && go mx

    go2 g f =
      if domain cat g /= codomain cat f then
        True
      else
        case compose cat g f of
          Nothing -> False
          Just gf -> domain cat gf == domain cat f && codomain cat gf == codomain cat g

---------------------------------------------------------------------

-- Composition is associative, that is:
-- given f:X->Y, g:Y->Z and h:Z->W, h (g f) = (h g) f

composition_is_associative :: (Eq o,Eq m) => Category o m -> Bool

composition_is_associative cat =
  go $ morphisms cat
  where
    go []           = True
    go (m : mx)     = go2 m mx && go mx

    go2 _ []        = True
    go2 f (g : mx)  = all (go3 f g) mx && go2 f mx

    go3 f g h =
      if codomain cat f == domain cat g && codomain cat g == domain cat h then
        case (compose cat g f, compose cat h g) of
          (Just gf, Just hg) ->
            case (compose cat h gf, compose cat hg f) of
              (Just hgf0, Just hgf1) -> hgf0 == hgf1
              _                      -> False
          _ -> False
      else
        True

---------------------------------------------------------------------

-- For every object X there is an identity morphism idX : X -> X, satisfying
-- (idX g) = g for every g : Y -> X -- and (f idX) = f for every f : X -> Y.

identity_is_identity :: (Eq m,Eq o) => Category o m -> Bool

identity_is_identity cat =
  go $ objects cat
  where
    go []     = True
    go (o:ox) = all (go2 o) (morphisms cat) && go ox

    go2 o m =
      if domain cat m == o then
        case compose cat m (identity cat o) of
          Nothing -> False
          Just mo -> mo == m
      else if codomain cat m == o then
        case compose cat (identity cat o) m of
          Nothing -> False
          Just im -> im == m
      else
        True

---------------------------------------------------------------------

instance (Show m,Show o) => Show (Category o m) where
  show cat = "Category{objects=" ++ show (objects cat) ++ ",morphisms=" ++ show (morphisms cat) ++ "}"

---------------------------------------------------------------------

testCategory :: Category String (String,String,String)

testCategory =
  Category
  {
    objects   = ["A","B","C","D"],
    morphisms = [("f","A","B"),("g","B","C"),("h","C","D"),("i","A","D")],
    domain    = \(_,a,_) -> a,
    codomain  = \(_,_,b) -> b,
    compose   = \(g,gd,gc) (f,fd,fc) ->
            if fc /= gd then
              Nothing
            else if gd == gc then
              Just (f,fd,fc)
            else if fd == fc then
              Just (g,gd,gc)
            else
              Just (g ++ "." ++ f,fd,gc),
    identity = \o -> ("id" ++ show o, o, o)
  }

---------------------------------------------------------------------

main :: IO ()

main = do
  putStrLn "Category Theory"
  let cat = testCategory
  putStrLn $ show cat
  putStrLn $ "Is category: " ++ show (is_category cat)

Answer 1

This seems like not a bad pass at a translation of the raw structure. But you cannot leverage the type system to do any of the checking for you.

The data-category package (https://hackage.haskell.org/package/data-category) uses a neat trick to do your construction "one level up" and enforce some properties of composition of morphisms, etc...

The core is

class Category k where
  src :: k a b -> Obj k a
  tgt :: k a b -> Obj k b
  (.) :: k b c -> k a b -> k a c

type Obj k a = k a a

Here he represents only morphisms and their compositions, and then captures objects simply as the identity morphisms on those objects. I've found this library pretty powerful in what it can express.