Project 13: Category Theory Visualizer

Project 13: Category Theory Visualizer

Project Overview

Attribute Details
Difficulty Expert
Time Estimate 3-4 weeks
Primary Language Haskell
Alternative Languages Scala, Idris, PureScript
Knowledge Area Category Theory / Mathematics / Type Classes
Tools Required GHC, Cabal/Stack, diagrams library, optionally GraphViz
Primary Reference “Category Theory for Programmers” by Bartosz Milewski
Prerequisites Projects 6 (Functor-Applicative-Monad Hierarchy) and 11 (Lenses/Optics), mathematical maturity

Learning Objectives

By completing this project, you will be able to:

  1. Define and implement categories including objects, morphisms, identity, and composition with verified laws
  2. Represent functors as structure-preserving maps between categories and verify functor laws algorithmically
  3. Construct and visualize natural transformations as morphisms between functors with commutative diagram verification
  4. Explain the meaning of “monad as monoid in endofunctors” with concrete visual examples
  5. Connect categorical abstractions to Haskell type classes demonstrating how Functor, Applicative, and Monad arise from category theory
  6. Generate visual diagrams of categories, functors, and natural transformations programmatically
  7. Verify categorical laws using property-based testing and symbolic computation

Deep Theoretical Foundation

Why Category Theory Matters for Programming

Category theory is often dismissed as abstract nonsense, but it is actually the mathematics of composition. When we write programs, we compose small pieces into larger ones. Category theory studies this composition at the most general level possible.

Haskell’s type class hierarchy—Functor, Applicative, Monad, Arrow, and beyond—did not emerge from engineering intuition. These abstractions were discovered by mathematicians studying categorical structures. Understanding category theory transforms these type classes from arbitrary APIs into inevitable consequences of mathematical structure.

The famous phrase “a monad is just a monoid in the category of endofunctors” sounds like a joke, but it is literally true. By the end of this project, you will not only understand what that means—you will have built a tool that visualizes it.

What is a Category?

A category C consists of:

  1. Objects: A collection of “things” (we will call them Ob(C))
  2. Morphisms: For any two objects A and B, a collection of “arrows” Hom(A, B) from A to B
  3. Identity: For each object A, an identity morphism id_A : A -> A
  4. Composition: For morphisms f : A -> B and g : B -> C, a composite g . f : A -> C

These must satisfy two laws:

Identity Law: For any morphism f : A -> B:

id_B . f = f = f . id_A

Associativity Law: For morphisms f : A -> B, g : B -> C, h : C -> D:

h . (g . f) = (h . g) . f

This is the most fundamental structure in mathematics. Nearly everything can be viewed as a category.

Examples of Categories

Set: The category of sets and functions

  • Objects: Sets (like {1,2,3}, the integers, the reals)
  • Morphisms: Total functions between sets
  • Identity: The function that returns its input unchanged
  • Composition: Function composition

Hask: The category of Haskell types (with some caveats)

  • Objects: Haskell types (Int, String, Bool, Maybe a, [a], etc.)
  • Morphisms: Haskell functions of type a -> b
  • Identity: id :: a -> a
  • Composition: (.) :: (b -> c) -> (a -> b) -> (a -> c)

Mon: The category of monoids and monoid homomorphisms

  • Objects: Monoids (like (Int, +, 0) or (String, ++, “”))
  • Morphisms: Functions preserving the monoid structure
  • Identity: The identity homomorphism
  • Composition: Composition of homomorphisms

1: The category with one object and one morphism

  • Objects: A single object (call it *)
  • Morphisms: Just id_*
  • This is the simplest non-trivial category

0: The empty category

  • Objects: None
  • Morphisms: None
  • This is trivially a category (vacuously satisfies all laws)

Functors: Structure-Preserving Maps

A functor F from category C to category D is a mapping that preserves categorical structure:

  1. Object mapping: F maps each object A in C to an object F(A) in D
  2. Morphism mapping: F maps each morphism f : A -> B in C to a morphism F(f) : F(A) -> F(B) in D

Functors must preserve identity and composition:

Identity Preservation: F(id_A) = id_{F(A)}

Composition Preservation: F(g . f) = F(g) . F(f)

In Haskell, the Functor type class captures exactly this:

class Functor f where
    fmap :: (a -> b) -> f a -> f b

-- The functor laws (not enforced by the compiler):
-- fmap id = id
-- fmap (g . f) = fmap g . fmap f

The type constructor f is the object mapping (Int becomes f Int, String becomes f String). The function fmap is the morphism mapping (a function a -> b becomes a function f a -> f b).

Endofunctors

An endofunctor is a functor from a category to itself: F : C -> C.

All Haskell Functors are endofunctors on Hask:

  • Maybe : Hask -> Hask
  • [] : Hask -> Hask
  • Either e : Hask -> Hask
  • IO : Hask -> Hask

This is crucial because monads are defined on endofunctors.

Natural Transformations: Morphisms Between Functors

Given two functors F, G : C -> D, a natural transformation eta : F => G is a family of morphisms:

For each object A in C, a morphism eta_A : F(A) -> G(A) in D

These must satisfy the naturality condition: For any morphism f : A -> B in C:

G(f) . eta_A = eta_B . F(f)

This is often drawn as a commutative square:

    F(A) ----eta_A----> G(A)
      |                   |
   F(f)|                  |G(f)
      v                   v
    F(B) ----eta_B----> G(B)

In Haskell, natural transformations are polymorphic functions:

-- Natural transformation from [] to Maybe
safeHead :: [a] -> Maybe a
safeHead []    = Nothing
safeHead (x:_) = Just x

-- Natural transformation from Maybe to []
maybeToList :: Maybe a -> [a]
maybeToList Nothing  = []
maybeToList (Just x) = [x]

-- Natural transformation from Either e to Maybe
eitherToMaybe :: Either e a -> Maybe a
eitherToMaybe (Left _)  = Nothing
eitherToMaybe (Right x) = Just x

The naturality condition is guaranteed by parametric polymorphism—a profound result called the “free theorem” or “theorems for free” (Wadler, 1989).

The Category of Endofunctors

We can form a new category [C, C] (endofunctors on C):

  • Objects: Endofunctors on C
  • Morphisms: Natural transformations between them
  • Identity: The identity natural transformation
  • Composition: Vertical composition of natural transformations

This category is crucial for understanding monads.

Monoids

A monoid is a set M with:

  • A binary operation: m : M x M -> M
  • An identity element: e in M

Satisfying:

  • Associativity: m(m(a, b), c) = m(a, m(b, c))
  • Identity: m(e, a) = a = m(a, e)

Examples:

  • (Int, +, 0)
  • (Int, *, 1)
  • (String, ++, “”)
  • ([a], ++, [])
  • (Bool, &&, True)
  • (Bool,   , False)

In Haskell:

class Monoid m where
    mempty  :: m
    mappend :: m -> m -> m  -- also written as (<>)

-- Laws:
-- mempty <> x = x
-- x <> mempty = x
-- (x <> y) <> z = x <> (y <> z)

Monoids in Monoidal Categories

To generalize monoids, we need monoidal categories—categories equipped with a “tensor product” operation on objects and morphisms.

A monoidal category (C, tensor, I) has:

  • A bifunctor tensor : C x C -> C
  • A unit object I
  • Associator and unitor natural isomorphisms satisfying coherence conditions

A monoid object in a monoidal category is an object M with:

  • Multiplication: mu : M tensor M -> M
  • Unit: eta : I -> M

Satisfying associativity and identity laws (expressed as commutative diagrams).

Monads as Monoids in the Category of Endofunctors

Here is the key insight:

The category of endofunctors [C, C] is monoidal:

  • Tensor product: Functor composition (F . G)
  • Unit: The identity functor Id

A monad is a monoid object in this monoidal category.

Concretely, a monad on C is an endofunctor M : C -> C with:

  • Unit: eta : Id => M (natural transformation from identity)
  • Multiplication: mu : M . M => M (natural transformation from M composed with M)

Satisfying:

  • Left identity: mu . eta_M = id_M
  • Right identity: mu . M(eta) = id_M
  • Associativity: mu . mu_M = mu . M(mu)

In Haskell terms:

  • Unit is return :: a -> m a
  • Multiplication is join :: m (m a) -> m a
  • The bind operation (>>=) is derived: ma >>= f = join (fmap f ma)

Let us verify for Maybe:

-- Unit (return)
return :: a -> Maybe a
return x = Just x

-- Multiplication (join)
join :: Maybe (Maybe a) -> Maybe a
join Nothing         = Nothing
join (Just Nothing)  = Nothing
join (Just (Just x)) = Just x

-- Left identity: join . return = id
-- join (return (Just 5)) = join (Just (Just 5)) = Just 5 ✓

-- Right identity: join . fmap return = id
-- join (fmap return (Just 5)) = join (Just (Just 5)) = Just 5 ✓

-- Associativity: join . join = join . fmap join
-- For Maybe (Maybe (Maybe a)):
-- join (join x) = join (fmap join x) ✓

This is why “a monad is just a monoid in the category of endofunctors” is literally true.

Applicative Functors Categorically

Applicative functors have categorical interpretations too. They are lax monoidal functors—functors that preserve monoidal structure up to coherent natural transformations.

An applicative functor is an endofunctor F with:

  • pure :: a -> F a (unit)
  • (<*>) :: F (a -> b) -> F a -> F b (application)

The categorical view provides the monoidal presentation:

  • unit :: () -> F ()
  • (**) :: F a -> F b -> F (a, b)

These are equivalent formulations, connected by:

fa ** fb = (,) <$> fa <*> fb
ff <*> fa = fmap (uncurry ($)) (ff ** fa)

Kleisli Categories

Every monad M on C gives rise to a Kleisli category K_M:

  • Objects: Same as C
  • Morphisms: A “Kleisli arrow” from A to B is a morphism A -> M(B) in C
  • Identity: return : A -> M(A)
  • Composition: Kleisli composition using bind

In Haskell, this is the Category instance for Kleisli:

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

instance Monad m => Category (Kleisli m) where
    id = Kleisli return
    Kleisli g . Kleisli f = Kleisli (\x -> f x >>= g)

Kleisli categories are how monadic effects compose.

Adjunctions

Adjunctions are pairs of functors with a special relationship. Given categories C and D:

An adjunction F -| G (F left adjoint to G) consists of:

  • F : C -> D (left adjoint)
  • G : D -> C (right adjoint)
  • A natural bijection: Hom_D(F(A), B) ~ Hom_C(A, G(B))

The profound fact: Every adjunction gives rise to a monad. The monad is G . F with:

  • Unit from the adjunction’s unit
  • Multiplication from the adjunction’s counit

Many familiar monads arise from adjunctions:

  • State monad from curry/uncurry adjunction
  • Reader monad from product/function adjunction
  • Continuation monad from double negation

Yoneda Lemma

The Yoneda lemma is one of the most important results in category theory. It states:

For a locally small category C and functor F : C -> Set, natural transformations from the hom-functor Hom(A, -) to F are in bijection with elements of F(A):

Nat(Hom(A, -), F) ~ F(A)

In Haskell, this becomes:

-- Yoneda lemma
yoneda :: Functor f => (forall b. (a -> b) -> f b) -> f a
yoneda k = k id

-- Inverse
coyoneda :: Functor f => f a -> (forall b. (a -> b) -> f b)
coyoneda fa f = fmap f fa

-- These are inverses:
-- yoneda . coyoneda = id
-- coyoneda . yoneda = id

The Yoneda lemma enables powerful optimizations (fusion) and is the basis for lens representations.

Coyoneda Optimization

The Coyoneda construction lets us defer fmap applications:

data Coyoneda f a where
    Coyoneda :: (b -> a) -> f b -> Coyoneda f a

instance Functor (Coyoneda f) where
    fmap f (Coyoneda g fb) = Coyoneda (f . g) fb  -- Compose functions, no fmap!

liftCoyoneda :: f a -> Coyoneda f a
liftCoyoneda = Coyoneda id

lowerCoyoneda :: Functor f => Coyoneda f a -> f a
lowerCoyoneda (Coyoneda f fa) = fmap f fa

This allows fmap f . fmap g . fmap h to become a single fmap (f . g . h), fusing multiple traversals.

Complete Project Specification

What You Are Building

A category theory visualization tool called category-viz that:

  1. Defines categories with objects, morphisms, and composition
  2. Constructs functors between categories with law verification
  3. Represents natural transformations with naturality checking
  4. Visualizes categorical structures as diagrams
  5. Demonstrates monad structure as monoid in endofunctors
  6. Provides an interactive REPL for exploring category theory

Functional Requirements

category-viz repl                    # Interactive exploration
category-viz show category Hask      # Display category structure
category-viz show functor Maybe      # Show functor action
category-viz show natural safeHead   # Show natural transformation
category-viz show monad Maybe        # Show monad as monoid
category-viz verify functor-laws Maybe
category-viz verify monad-laws Maybe
category-viz diagram functor Maybe -o functor.svg
category-viz diagram natural safeHead -o natural.svg
category-viz compare List Maybe      # Compare functors

Core Data Types

-- Categories
data Category obj mor = Category
    { catObjects   :: [obj]
    , catMorphisms :: [(mor, obj, obj)]  -- (morphism, source, target)
    , catIdentity  :: obj -> mor
    , catCompose   :: mor -> mor -> Maybe mor  -- Nothing if not composable
    , catName      :: String
    }

-- Functors
data CFunctor c1 c2 = CFunctor
    { functorName     :: String
    , functorObjMap   :: Object c1 -> Object c2
    , functorMorMap   :: Morphism c1 -> Morphism c2
    , functorSource   :: c1
    , functorTarget   :: c2
    }

-- Natural transformations
data NatTrans f g a = NatTrans
    { natName      :: String
    , natComponent :: f a -> g a
    }

-- Monad structure
data MonadStructure m = MonadStructure
    { monadFunctor :: CFunctor Hask Hask
    , monadUnit    :: forall a. a -> m a
    , monadMult    :: forall a. m (m a) -> m a
    }

Expected Output

$ category-viz show category Hask

Category: Hask (Haskell types and functions)
============================================

Objects (sample types):
  Int, String, Bool, [a], Maybe a, Either e a, IO a, a -> b

Morphisms (sample functions):
  show    : Int -> String
  length  : [a] -> Int
  even    : Int -> Bool
  not     : Bool -> Bool
  id      : a -> a
  (.)     : (b -> c) -> (a -> b) -> (a -> c)

Identity:
  id :: a -> a
  Verified: id . f = f = f . id

Composition:
  (.) :: (b -> c) -> (a -> b) -> (a -> c)
  Verified: (f . g) . h = f . (g . h)

$ category-viz show functor Maybe

Functor: Maybe : Hask -> Hask
=============================

Object Mapping:
  Int     |-> Maybe Int
  String  |-> Maybe String
  Bool    |-> Maybe Bool
  [a]     |-> Maybe [a]

Morphism Mapping (fmap):
  show : Int -> String
    |->
  fmap show : Maybe Int -> Maybe String

Implementation:
  fmap f Nothing  = Nothing
  fmap f (Just x) = Just (f x)

Functor Laws:
  Identity:    fmap id = id                          [VERIFIED]
  Composition: fmap (f . g) = fmap f . fmap g        [VERIFIED]

$ category-viz show monad Maybe

Monad: Maybe as Monoid in [Hask, Hask]
======================================

Underlying Endofunctor: Maybe : Hask -> Hask

Unit (return : Id => Maybe):
  return :: a -> Maybe a
  return x = Just x

  Components:
    return_Int    : Int -> Maybe Int
    return_String : String -> Maybe String
    return_Bool   : Bool -> Maybe Bool

Multiplication (join : Maybe . Maybe => Maybe):
  join :: Maybe (Maybe a) -> Maybe a
  join Nothing         = Nothing
  join (Just Nothing)  = Nothing
  join (Just (Just x)) = Just x

Monad Laws (Monoid Laws):
  Left Identity:  join . return        = id    [VERIFIED]
  Right Identity: join . fmap return   = id    [VERIFIED]
  Associativity:  join . join = join . fmap join [VERIFIED]

Diagram:
         eta
    Id ========> M
                 |
                 | mu
                 v
    M . M =====> M
          mu

Connection to (>>=):
  ma >>= f = join (fmap f ma)

Solution Architecture

Module Structure

src/
  Category/
    Core.hs           -- Category, Functor, NatTrans types
    Hask.hs           -- The Hask category
    Examples.hs       -- Set, Mon, Kleisli categories
  Functor/
    Core.hs           -- Functor representation
    Laws.hs           -- Functor law verification
    Examples.hs       -- Maybe, [], Either, etc.
  Natural/
    Core.hs           -- Natural transformation
    Laws.hs           -- Naturality verification
    Examples.hs       -- safeHead, maybeToList, etc.
  Monad/
    Core.hs           -- Monad as monoid structure
    Laws.hs           -- Monad law verification
    Kleisli.hs        -- Kleisli category construction
  Visualization/
    Diagram.hs        -- Diagram generation
    ASCII.hs          -- ASCII art diagrams
    SVG.hs            -- SVG output
  REPL/
    Core.hs           -- REPL implementation
    Parser.hs         -- Command parsing
    Commands.hs       -- Command handlers
  Main.hs             -- CLI entry point

Key Design Decisions

1. Representing Hask

We cannot enumerate all Haskell types. Instead, we work with a finite subcategory of Hask containing sample types:

data HaskObj = HInt | HString | HBool | HList HaskObj | HMaybe HaskObj | ...
    deriving (Eq, Show)

data HaskMor = HId HaskObj | HShow | HLength | HEven | HNot | HComp HaskMor HaskMor | ...
    deriving (Eq, Show)

2. Functors as Type Constructors

We represent functors using GADTs to capture the type-level mapping:

data HaskFunctor where
    MaybeFunctor :: HaskFunctor
    ListFunctor  :: HaskFunctor
    EitherFunctor :: HaskObj -> HaskFunctor
    ...

applyFunctor :: HaskFunctor -> HaskObj -> HaskObj
applyFunctor MaybeFunctor t = HMaybe t
applyFunctor ListFunctor t = HList t
...

3. Law Verification

Use QuickCheck to verify laws for concrete instances:

prop_FunctorIdentity :: (Functor f, Eq (f Int)) => f Int -> Bool
prop_FunctorIdentity fa = fmap id fa == fa

prop_FunctorComposition :: (Functor f, Eq (f Int)) =>
    f Int -> (Int -> Int) -> (Int -> Int) -> Bool
prop_FunctorComposition fa f g = fmap (f . g) fa == (fmap f . fmap g) fa

4. Diagram Generation

Use the diagrams library for SVG generation:

categoryDiagram :: Category obj mor -> Diagram B
functorDiagram :: CFunctor c1 c2 -> Diagram B
naturalDiagram :: NatTrans f g -> Diagram B
monadDiagram :: MonadStructure m -> Diagram B

Core Algorithms

Composition Verification:

verifyAssociativity :: Category obj mor -> [(mor, mor, mor)] -> [Bool]
verifyAssociativity cat triples =
    [ catCompose cat (catCompose cat f g) h ==
      catCompose cat f (catCompose cat g h)
    | (f, g, h) <- triples
    , composable3 cat f g h
    ]

Naturality Checking:

checkNaturality :: (Functor f, Functor g, Eq (g b)) =>
    (forall a. f a -> g a) -> (a -> b) -> f a -> Bool
checkNaturality eta f fa =
    (eta . fmap f) fa == (fmap f . eta) fa

Monad Law Verification:

checkLeftIdentity :: (Monad m, Eq (m a)) => m a -> Bool
checkLeftIdentity ma = (join . return) ma == ma

checkRightIdentity :: (Monad m, Eq (m a)) => m a -> Bool
checkRightIdentity ma = (join . fmap return) ma == ma

checkAssociativity :: (Monad m, Eq (m a)) => m (m (m a)) -> Bool
checkAssociativity mmma =
    (join . join) mmma == (join . fmap join) mmma

Phased Implementation Guide

Phase 1: Category Foundation (Days 1-5)

Goal: Implement basic category representation and the Hask subcategory.

Tasks:

  1. Define Category data type with objects, morphisms, identity, composition
  2. Implement finite subcategory of Hask with sample types
  3. Add composition and identity functions
  4. Write verification for identity and associativity laws
  5. Create ASCII visualization for categories

Validation: Display Hask category, verify all laws pass.

Hints:

  • Start with just 5-6 types: Int, String, Bool, Maybe Int, [Int]
  • Morphisms can be represented as an ADT of known functions
  • Use pattern matching for composition

Phase 2: Functor Implementation (Days 6-10)

Goal: Implement functors with law verification.

Tasks:

  1. Define CFunctor data type with object and morphism mappings
  2. Implement Maybe, List, Either as functors
  3. Create fmap representation that works on HaskMor
  4. Write QuickCheck properties for functor laws
  5. Visualize functor action (object and morphism mapping)

Validation: All functor laws verified for Maybe, List, Either.

Hints:

  • The morphism mapping must produce a valid morphism in target category
  • Remember: F(id_A) must equal id_{F(A)}
  • F(g . f) must equal F(g) . F(f)

Phase 3: Natural Transformations (Days 11-15)

Goal: Implement natural transformations with naturality verification.

Tasks:

  1. Define NatTrans as family of morphisms
  2. Implement safeHead, maybeToList, eitherToMaybe, etc.
  3. Verify naturality condition programmatically
  4. Draw commutative squares showing naturality
  5. Implement composition of natural transformations

Validation: Naturality verified for all examples, diagrams generated.

Hints:

  • Naturality is: eta_B . F(f) = G(f) . eta_A
  • Draw the square: F(A) -> G(A) -> G(B) must equal F(A) -> F(B) -> G(B)
  • Use parametric polymorphism’s free theorems

Phase 4: Monad as Monoid (Days 16-20)

Goal: Implement monad structure showing monoid nature.

Tasks:

  1. Define MonadStructure with unit and multiplication
  2. Implement for Maybe, List, Either, Reader, State
  3. Verify monad laws as monoid laws in endofunctors
  4. Show relationship between join/return and =
  5. Construct Kleisli category from monad

Validation: All monad laws verified, Kleisli composition demonstrated.

Hints:

  • Unit: eta : Id => M (return)
  • Multiplication: mu : M . M => M (join)
  • Derive = from join: ma = f = join (fmap f ma)

Phase 5: Visualization and REPL (Days 21-28)

Goal: Create interactive exploration tool with diagram generation.

Tasks:

  1. Implement command parser for REPL
  2. Create ASCII and SVG diagram generators
  3. Add side-by-side comparison of functors/monads
  4. Implement interactive law verification
  5. Add export to various formats

Validation: Full REPL working, diagrams exported correctly.

Hints:

  • Use diagrams library for SVG
  • ASCII diagrams with box-drawing characters
  • Allow user to define custom categories

Testing Strategy

Property-Based Testing

-- Functor laws
prop_functorIdentity :: TestFunctor f => f Int -> Property
prop_functorComposition :: TestFunctor f => f Int -> Fun Int Int -> Fun Int Int -> Property

-- Natural transformation naturality
prop_naturality :: (Functor f, Functor g, Eq (g b), Show (g b)) =>
    (forall a. f a -> g a) -> f Int -> Fun Int Int -> Property

-- Monad laws
prop_leftIdentity :: TestMonad m => m Int -> Property
prop_rightIdentity :: TestMonad m => m Int -> Property
prop_associativity :: TestMonad m => m (m (m Int)) -> Property

-- Category laws
prop_categoryIdentityLeft :: Category obj mor -> mor -> Property
prop_categoryIdentityRight :: Category obj mor -> mor -> Property
prop_categoryAssociativity :: Category obj mor -> mor -> mor -> mor -> Property

Unit Tests

-- Specific verification
test_maybeJoinLeftId = join (return (Just 5)) @?= Just 5
test_maybeJoinRightId = join (fmap return (Just 5)) @?= Just 5
test_maybeJoinAssoc = let x = Just (Just (Just 5))
                      in join (join x) @?= join (fmap join x)

-- Natural transformation
test_safeHeadNaturality =
    let f = (+1) :: Int -> Int
        xs = [1,2,3]
    in (safeHead . fmap f) xs @?= (fmap f . safeHead) xs

-- Kleisli composition
test_kleisliAssoc =
    let f = \x -> Just (x + 1)
        g = \x -> Just (x * 2)
        h = \x -> Just (x - 3)
    in runKleisli ((Kleisli h . Kleisli g) . Kleisli f) 5 @?=
       runKleisli (Kleisli h . (Kleisli g . Kleisli f)) 5

Diagram Verification

-- Ensure generated diagrams are well-formed
test_diagramObjects = length (diagramObjects (categoryDiagram hask)) > 0
test_diagramMorphisms = all validArrow (diagramArrows (functorDiagram maybeF))
test_diagramCommutes = verifyCommutes (naturalDiagram safeHeadNat)

Common Pitfalls and Debugging

Pitfall 1: Confusing Object and Morphism Mappings

Symptom: Functor verification fails mysteriously.

Cause: Mixing up how functors map objects vs morphisms.

Solution: Clearly separate the two:

-- Object mapping (on types)
Maybe : Type -> Type
Maybe Int = Maybe Int

-- Morphism mapping (on functions)
fmap : (a -> b) -> (Maybe a -> Maybe b)
fmap show : Maybe Int -> Maybe String

Pitfall 2: Forgetting Composition Compatibility

Symptom: Composition returns Nothing unexpectedly.

Cause: Trying to compose morphisms where target of first does not equal source of second.

Solution: Always check composability:

composable :: Category obj mor -> mor -> mor -> Bool
composable cat f g = target cat f == source cat g

Pitfall 3: Natural Transformation Generality

Symptom: Naturality check passes for specific types but concept seems wrong.

Cause: Not testing across enough types.

Solution: Use polymorphism to ensure naturality holds for all types:

-- Good: truly polymorphic
safeHead :: forall a. [a] -> Maybe a

-- Bad: only works for specific type
safeHeadInt :: [Int] -> Maybe Int  -- Not a natural transformation!

Pitfall 4: Monad Law Verification Order

Symptom: Monad laws seem to fail.

Cause: Confusing the three different formulations of monad laws.

Solution: Pick one formulation and stick to it:

-- Kleisli formulation (>>=)
-- 1. return x >>= f  =  f x
-- 2. m >>= return    =  m
-- 3. (m >>= f) >>= g =  m >>= (\x -> f x >>= g)

-- Join formulation
-- 1. join . return      = id
-- 2. join . fmap return = id
-- 3. join . join        = join . fmap join

-- Categorical (monoid in endofunctors)
-- 1. mu . eta_M     = id_M
-- 2. mu . M(eta)    = id_M
-- 3. mu . mu_M      = mu . M(mu)

Debugging Tips

  1. Print intermediate structures: Log object mappings, morphism mappings at each step
  2. Test on trivial categories: Verify laws on 1-object, 1-morphism category first
  3. Use specific examples: Test with Int -> String -> Int composition chain
  4. Draw diagrams by hand: Verify your code matches hand-drawn commutative diagrams

Extensions and Challenges

Extension 1: Adjunction Visualization

Implement adjunctions and show how they give rise to monads:

data Adjunction f g = Adjunction
    { leftAdjoint  :: CFunctor c d    -- F : C -> D
    , rightAdjoint :: CFunctor d c    -- G : D -> C
    , unit   :: NatTrans Id (g . f)   -- eta : Id => G . F
    , counit :: NatTrans (f . g) Id   -- epsilon : F . G => Id
    }

-- Derive monad from adjunction
adjunctionToMonad :: Adjunction f g -> MonadStructure (Compose g f)

Extension 2: Kan Extensions

Implement left and right Kan extensions:

-- Left Kan extension of F along K
data LanK k f a where
    Lan :: (k b -> a) -> f b -> LanK k f a

-- Right Kan extension of F along K
newtype RanK k f a = Ran { runRan :: forall b. (a -> k b) -> f b }

Extension 3: Limits and Colimits

Visualize categorical limits (products, equalizers, pullbacks) and colimits (coproducts, coequalizers, pushouts):

-- Product as limit
data Product a b = Product a b  -- Limit of discrete category {a, b}

-- Coproduct as colimit
data Coproduct a b = InL a | InR b  -- Colimit

-- Equalizer
data Equalizer f g a = Equalizer a  -- where f a == g a

-- Pullback
data Pullback f g a b c = Pullback a b  -- where f a == g b

Challenge: Free Theorems Generator

Given a polymorphic type signature, generate the corresponding free theorem:

freeTheorem :: Type -> String
freeTheorem "forall a. [a] -> [a]" =
    "For all functions f, map f . reverse = reverse . map f"
freeTheorem "forall a b. (a -> b) -> [a] -> [b]" =
    "map f . map g = map (f . g)"

Challenge: Category Browser

Build an interactive browser for exploring famous categories:

  • Grp (groups and homomorphisms)
  • Top (topological spaces)
  • Vect (vector spaces)
  • Cat (small categories themselves!)

Real-World Connections

Where Category Theory Appears

  1. Type System Design: Scala, Haskell, and Rust type systems influenced by CT
  2. Database Query Languages: Functorial data migration, categorical query semantics
  3. Compiler Design: SSA form as free category, optimization as functor
  4. Quantum Computing: Categorical quantum mechanics, compact closed categories
  5. Machine Learning: Backpropagation as functor, automatic differentiation
  6. Distributed Systems: CRDTs as join-semilattices (categorical structure)

Industry Applications

  • AWS Step Functions: State machines as categories
  • Apache Kafka Streams: Stream processors as functors
  • Stripe’s type-safe API design: Inspired by categorical thinking
  • Facebook’s Haxl: Free monad for data fetching (categorical)
  • Bloomberg’s functional finance DSL: Compositional contract algebra

Interview Questions

After completing this project, you should be able to answer:

  1. What is a category and what are its laws?
    • Define objects, morphisms, identity, composition
    • State and explain identity and associativity laws
    • Give examples: Set, Hask, monoids as single-object categories
  2. What does it mean for a functor to “preserve structure”?
    • Object and morphism mappings
    • Preservation of identity and composition
    • Why this makes functors the “right” notion of mapping between categories
  3. What is a natural transformation and why is naturality important?
    • Family of morphisms indexed by objects
    • The naturality square and its meaning
    • Connection to parametric polymorphism and free theorems
  4. Explain “a monad is a monoid in the category of endofunctors”
    • Define monoid (set, operation, identity, laws)
    • Define the category of endofunctors (objects: functors, morphisms: natural transformations)
    • Show monad unit = monoid identity, monad join = monoid multiplication
  5. How do the three formulations of monad laws relate?
    • Kleisli formulation (bind laws)
    • Join formulation
    • Categorical formulation (monoid in endofunctors)
    • Derive each from the others
  6. What is the Yoneda lemma and why is it important?
    • Statement: Nat(Hom(A,-), F) isomorphic to F(A)
    • Haskell encoding and intuition
    • Applications: lens, optimization
  7. How do adjunctions give rise to monads?
    • Definition of adjunction (unit, counit, triangle identities)
    • Construction: monad from G . F where F - G
    • Examples: State from curry-uncurry, Reader from product-function

Self-Assessment Checklist

Before considering this project complete, verify:

  • You can define a category with objects, morphisms, and verified laws
  • You can implement a functor and verify both functor laws
  • You can implement a natural transformation and verify naturality
  • You can explain why polymorphic functions are natural transformations
  • You can show monad structure (unit, multiplication) for Maybe and List
  • You can verify monad laws in the join/return formulation
  • You understand the connection between = and join
  • You can construct the Kleisli category from a monad
  • You can visualize functor action and natural transformation squares
  • You can explain “monad is monoid in endofunctors” to another programmer
  • You understand how the Yoneda lemma enables optimization
  • Your tool generates correct diagrams for all categorical structures

Resources

Essential Reading

Topic Resource Notes
Categories, functors, naturals “Category Theory for Programmers” by Bartosz Milewski, Ch. 1-10 Free online, excellent for programmers
Monads categorically “Category Theory for Programmers” Ch. 21 The famous “monoid in endofunctors”
Formal CT foundations “Category Theory” by Steve Awodey, Ch. 1-4 Rigorous mathematical treatment
Applied CT “Seven Sketches in Compositionality” by Fong & Spivak Modern applications
CT for working programmer “Programming with Categories” (MIT draft) Category theory via code
Haskell type classes “Haskell Programming from First Principles” Ch. 16-18 Functor/Applicative/Monad
Free theorems “Theorems for Free” by Wadler (1989) Naturality from polymorphism
Yoneda in Haskell “Yoneda and Coyoneda” on Hackage Practical applications

Papers

  • “Monads for functional programming” - Philip Wadler (1992)
  • “Notions of computation and monads” - Eugenio Moggi (1991)
  • “Comprehending monads” - Philip Wadler (1990)
  • “Categories for the Working Mathematician” - Saunders Mac Lane (the bible)
  • “Adjunctions” - nLab (comprehensive online resource)

Tools and Libraries

  • diagrams: Haskell library for declarative vector graphics
  • graphviz: DOT graph visualization
  • QuickCheck: Property-based testing for law verification
  • lens: Practical application of categorical ideas

Videos

  • Bartosz Milewski’s Category Theory lecture series (YouTube)
  • “Category Theory for the Working Hacker” - Philip Wadler (Strange Loop)
  • “Categories for the Working Haskeller” - Jeremy Gibbons

“Category theory is the subject where you’re allowed to assume everything is as nice as possible.” - John Baez

After completing this project, you’ll understand why Haskell’s type classes feel so mathematically elegant: they weren’t designed—they were discovered.