Markdown of literate Haskell program. Program source: /src/CTNotes/P1Ch03b_FiniteCats.lhs

Note about CTFP Part 1 Chapter 3. Categories great and small. Finite category construction in Haskell.

This note is about Haskell representation of categories created from simple directed graphs (finite enumeration of objects and morphisms). I use DataKinds to encode category objects as types (of a custom kind) and enumerate all possible morphisms using a GADT. Using GADTs makes it simple to visualize what is going on because I use them to enumerate all possible morphisms.

The approach looks generic (should be easily adjusted to other finite categories) but I am not trying to build some generic library here (if that is even possible).
I am just using a simple example category A->B=>C. (Free category generated by from simple graph with objects A, B, C and 3 generating morphisms: one A -> B and two B -> C). This category is so simple that it does not even express the (non-trivial) associativity law. There are just to few morphism and there are no 3 non-trivial morphisms that can be composed.

Because this construction allows for pattern matching on morphisms, it also allows to implicitly infer type information. Prametricity is lost and so are free theorems.

This approach is similar to Natural Numbers note N_P1Ch03a_NatsCat.

This note supplements Simple Graphs section of CTFP Ch 3.

 {-# LANGUAGE GADTs 
  , DataKinds 
  , KindSignatures 
  , FlexibleInstances 
  , PolyKinds 
  , StandaloneDeriving 
  , MultiParamTypeClasses 
  , AllowAmbiguousTypes  --needed for FinCategory instance only
 #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

 module CTNotes.P1Ch03b_FiniteCats where
 import Control.Category 
 import Prelude(Show, undefined)

Simple Finite Category

All objects in A->B=>C are defined as data type

 data Object = A | B | C deriving Show

and promoted (DataKinds pragma) to a kind Object with types A B and C.
Objects in A->B=>C are the types A B, and C.

All morphism in A->B=>C are defined using the following GADT

 data HomSet (a :: Object) (b :: Object) where
    -- generating edges in A->B=>C
    MorphId :: HomSet a a    -- polymorphic identity data constructor
    MorphAB :: HomSet 'A 'B
    MorphBC1 :: HomSet 'B 'C   
    MorphBC2 :: HomSet 'B 'C 
    -- derived 
    MorphAC1 :: HomSet 'A 'C -- MorphCB1 . MorphAB
    MorphAC2 :: HomSet 'A 'C -- MorphCB2 . MorphAB

 deriving instance Show (HomSet a b)

 newtype CoHomSet b a = CoHomSet (HomSet a b)

 deriving instance Show (CoHomSet a b)

Morphism composition:

 compose :: HomSet b c -> HomSet a b -> HomSet a c
 compose MorphId mab  = mab      -- GHC knows b == c
 compose mbc MorphId =  mbc      -- GHC knows a == b
 compose MorphBC1 MorphAB = MorphAC1
 compose MorphBC2 MorphAB = MorphAC2

Cool! GHC knows that this pattern match is exhaustive, something that takes a minute to digest.

Note: I have assumed the free construction, MorphAC1 and MorphAC2 are different. If, instead, I created a GADT with one MorphAC and have defined

compose MorphBC1 MorphAB = MorphAC
compose MorphBC2 MorphAB = MorphAC 

I would have gotten an equalizer-like diagram and it would be very hard to functor it into Hask.
Explicitly enumerating all possible morphisms in a GADT looks like redundant coding, but it provides flexibility to play with different categorical designs.

A->B=>C is Control.Category:
Here is the definition of Category quoted from base package Control.Category module:

class Category cat where
       id :: cat a a
       (.) :: cat b c -> cat a b -> cat a c

PolyKinds pragma causes Category to infer most general kind on cat which is k -> k -> * so Category class automatically infers Object -> Object -> * for me matching HomSet kind signature.
From the categorical stand point, cat :: Object -> Object -> * acts as a hom-set and Hask acts as the Set category. A better name would be 'Hom-Hask'.

 instance Category HomSet where
   id = MorphId
   (.) = compose

(Side-note: a cool way to think about this construction is as Object enriched over Hask, see N_P3Ch12a_HaskEnrich.)

Expressions like MorphCB . MorphAB will not compile, but 'correct' compositions work fine:

ghci> :t MorphId . MorphAB
MorphId . MorphAB :: HomSet 'A 'B

ghci> :t MorphBC1 . MorphAB
MorphBC1 . MorphAB :: HomSet 'A 'C

It is quite amazing that you can do stuff like this. Investigating non-Hask categories seems like an interesting direction to play with.

A Better Alternative

HomSet uses polymorphic definition of id morphisms MorphId. This is sometimes convenient by does not work well if there is a need to isolate the object on which id works on. (No pattern matching on types.)
The following definition could be a better for finite categories like the A->B=>C.

 data ObjectRep (a :: Object) where
    ARep :: ObjectRep 'A  
    BRep :: ObjectRep 'B 
    CRep :: ObjectRep 'C 

 deriving instance Show (ObjectRep a)

 data HS (a :: Object) (b :: Object) where
    MoId :: ObjectRep a -> HS a a    -- non-polymorphic version
    MoAB :: HS 'A 'B
    MoBC1 :: HS 'B 'C   
    MoBC2 :: HS 'B 'C 
    MoAC1 :: HS 'A 'C -- MorphCB1 . MorphAB
    MoAC2 :: HS 'A 'C -- MorphCB2 . MorphAB

 deriving instance Show (HS a b)
 
 comp :: HS b c -> HS a b -> HS a c
 comp (MoId _) mab  = mab      
 comp mbc (MoId _) =  mbc      
 comp MoBC1 MoAB = MoAC1
 comp MoBC2 MoAB = MoAC2

Except, I no longer get the polymorphic id:

 instance Category HS where
   id = undefined
   (.) = comp

but I could consider something similar to the definition of HaskEnrichedCategory in N_P3Ch12b_EnrichedPreorder.

 class FinCategory (ob :: k -> *) (cat:: k -> k -> *) where
   finid :: ob a -> cat a a
   fincomp :: cat b c -> cat a b -> cat a c

 instance FinCategory ObjectRep HS where
   finid = MoId
   fincomp = comp

Functors

N_P1Ch07b_Functors_AcrossCats provides example functors from this category.

Parametricity is lost

See N_P1Ch10b_NTsNonHask

Possibly relevant: Retricted Parametricity