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)
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.