I’ve decided to spent some time reading up on denotational semantics and concurrency and as a prelude I thought it would be a great idea to read up on some category theory. Despite studying some algebraic topology at college, the course didn’t cover any category theory. I picked up the nice and slim Basic Category Theory For Computer Scientists by Benjamin Pierce which turned out to be a good introduction to the subject. Of course, the only way to get really familiar with the material is to work through the exercises, and as part of that I really needed a way to look at some examples.

The obvious answer is to use F# to look at some simple categories. The REPL (read-eval-print loop) makes it easy to take arrows from the category and study their properties in order to find counter-examples. This should be not surprise – ML was originally invented as the implementation language of the LCF theorem proving system. Theorems could be represented as instances of abstract datatypes within the language, and the datatypes could expose functionality that allowed only valid theorems to be constructed. There is a book which I have just started reading, Computational Category Theory for which the source is available here, which covers some implementation of category theory in ML.

A category is basically a collection of objects and arrows with a means for finding the start and end objects of a given arrow, together with a means for getting the identity arrow corresponding to any object and a means of composing the arrows. Of course, there are constraints on these various functions which we cannot express in the type system.

type Category<‘arrow, ‘ob> =

{ Start : ‘arrow -> ‘ob; End : ‘arrow -> ‘ob; Identity : ‘ob -> ‘arrow; Compose : ‘arrow -> ‘arrow -> ‘arrow }

{ Start : ‘arrow -> ‘ob; End : ‘arrow -> ‘ob; Identity : ‘ob -> ‘arrow; Compose : ‘arrow -> ‘arrow -> ‘arrow }

We can then define a type representing an arrow, and define a function that generates one of the standard finite categories, that of a preorder on a list of elements where each element is < than the elements to the right of it in a list.

type Arrow<‘a> = { From : ‘a; To : ‘a}

let GenerateOrderCategory elements =

let startfn x = x.From

let endfn x = x.To

let check x =

if not (List.mem x elements)

then failwith "Invalid element for generating identity arrow"

else x

let identity x =

{ From = check x; To = x}

let compose arrow1 arrow2 =

if check(arrow1.To) = arrow2.From

then { From = check arrow1.From; To= check arrow2.To }

else failwith "Invalid composition"

{ Start = startfn; End=endfn; Identity= identity; Compose=compose }

let startfn x = x.From

let endfn x = x.To

let check x =

if not (List.mem x elements)

then failwith "Invalid element for generating identity arrow"

else x

let identity x =

{ From = check x; To = x}

let compose arrow1 arrow2 =

if check(arrow1.To) = arrow2.From

then { From = check arrow1.From; To= check arrow2.To }

else failwith "Invalid composition"

{ Start = startfn; End=endfn; Identity= identity; Compose=compose }

let OrderCategoryArrows elements =

let rec generate a b sofar =

if b = []

then if a = []

then sofar

else generate (List.tl a) (List.tl a) sofar

else generate a (List.tl b) ({ From = List.hd a; To = List.hd b } :: sofar)

Set.of_seq(generate elements elements [])

let rec generate a b sofar =

if b = []

then if a = []

then sofar

else generate (List.tl a) (List.tl a) sofar

else generate a (List.tl b) ({ From = List.hd a; To = List.hd b } :: sofar)

Set.of_seq(generate elements elements [])

A finite category can be expressed as a collection of functions representing the category, together with a Set of the arrows.

type FiniteCategory<‘arrow, ‘ob> =

{ Category : Category<‘arrow, ‘ob>; Arrows : Set<‘arrow> }

{ Category : Category<‘arrow, ‘ob>; Arrows : Set<‘arrow> }

We can then define the finite category over a finite set of elements.

let OrderCategory elements =

{ Category = GenerateOrderCategory elements; Arrows = OrderCategoryArrows elements}

{ Category = GenerateOrderCategory elements; Arrows = OrderCategoryArrows elements}

let cat1 = OrderCategory [1]

let cat2 = OrderCategory [1;2]

let cat3 = OrderCategory [1;2;3]

We cannot express the constraints on the fucntions representing the category in the type system, but for a finite category we can loop across all of the arrows to validate that the rules hold.

let canCompose category arrow1 arrow2 =

category.End arrow1 = category.Start arrow2

category.End arrow1 = category.Start arrow2

let CheckFiniteCategory finiteCategory =

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

let mutable objs = Set.empty

for arrow in arrows do objs <- Set.add (category.Start arrow) objs

for arrow in arrows do objs <- Set.add (category.End arrow) objs

// Identities

for ob in objs do

let id = category.Identity ob

if not (Set.mem id arrows && category.Start id = ob && category.End id = ob)

then failwith "No identity"

// Well defined

for a1 in arrows do

for a2 in arrows do

if canCompose category a1 a2

then

let result = category.Compose a1 a2

if not (Set.mem result arrows && category.Start result = category.Start a1 && category.End result = category.End a2)

then failwith "Invalid composition"

// Associative

for a1 in arrows do

for a2 in arrows do

for a3 in arrows do

if canCompose category a1 a2 && canCompose category a2 a3

then

let r1 = category.Compose (category.Compose a1 a2) a3

let r2 = category.Compose a1 (category.Compose a2 a3)

if r1 <> r2 then failwith "Not associative"

// Check identity composes with f to give f

for ob in objs do

let id = category.Identity ob

for arrow in arrows do

if canCompose category id arrow && category.Compose id arrow <> arrow

then failwith "Composing identity and arrow"

if canCompose category arrow id && category.Compose arrow id <> arrow

then failwith "Composing arrow and identity"

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

let mutable objs = Set.empty

for arrow in arrows do objs <- Set.add (category.Start arrow) objs

for arrow in arrows do objs <- Set.add (category.End arrow) objs

// Identities

for ob in objs do

let id = category.Identity ob

if not (Set.mem id arrows && category.Start id = ob && category.End id = ob)

then failwith "No identity"

// Well defined

for a1 in arrows do

for a2 in arrows do

if canCompose category a1 a2

then

let result = category.Compose a1 a2

if not (Set.mem result arrows && category.Start result = category.Start a1 && category.End result = category.End a2)

then failwith "Invalid composition"

// Associative

for a1 in arrows do

for a2 in arrows do

for a3 in arrows do

if canCompose category a1 a2 && canCompose category a2 a3

then

let r1 = category.Compose (category.Compose a1 a2) a3

let r2 = category.Compose a1 (category.Compose a2 a3)

if r1 <> r2 then failwith "Not associative"

// Check identity composes with f to give f

for ob in objs do

let id = category.Identity ob

for arrow in arrows do

if canCompose category id arrow && category.Compose id arrow <> arrow

then failwith "Composing identity and arrow"

if canCompose category arrow id && category.Compose arrow id <> arrow

then failwith "Composing arrow and identity"

We can then check the categories we have defined.

CheckFiniteCategory cat1

CheckFiniteCategory cat2

CheckFiniteCategory cat3

CheckFiniteCategory cat2

CheckFiniteCategory cat3

For the finite case, we can validate that certain arrows are epi- and mono- morphisms.

let isMonomorphism arrow finiteCategory =

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

Seq.for_all

(fun g ->

Seq.for_all

(fun h ->

if category.Start g = category.Start h && category.End g = category.End h

then if canCompose category g arrow

then if category.Compose g arrow = category.Compose h arrow

then g = h

else false

else true

else true)

arrows)

arrows

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

Seq.for_all

(fun g ->

Seq.for_all

(fun h ->

if category.Start g = category.Start h && category.End g = category.End h

then if canCompose category g arrow

then if category.Compose g arrow = category.Compose h arrow

then g = h

else false

else true

else true)

arrows)

arrows

let isEpimorphism arrow finiteCategory =

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

Seq.for_all

(fun g ->

Seq.for_all

(fun h ->

if category.Start g = category.Start h && category.End g = category.End h

then if canCompose category arrow g

then if category.Compose arrow g = category.Compose arrow h

then g = h

else false

else true

else true)

arrows)

arrows

let arrows = finiteCategory.Arrows

let category = finiteCategory.Category

Seq.for_all

(fun g ->

Seq.for_all

(fun h ->

if category.Start g = category.Start h && category.End g = category.End h

then if canCompose category arrow g

then if category.Compose arrow g = category.Compose arrow h

then g = h

else false

else true

else true)

arrows)

arrows

isMonomorphism {From=1;To=3} cat3

isEpimorphism {From=1;To=3} cat3;;

isEpimorphism {From=1;To=3} cat3;;

Another standard example is that of representing a group using arrows and a single object. We can construct it like so.

type GroupElement = Element

let CycleGroupProduct n =

let startfn _ = Element

let endfn _ = Element

let identity Element = (0,0)

let compose (a,b) (c,d) = ((a + c) % n, (b+d) % n)

let category =

{ Start=startfn; End=endfn; Identity=identity; Compose=compose }

let arrows =

seq {

for i in 0 .. n-1 do

for j in 0 .. n-1 do

yield (i,j)

}

{ Category = category; Arrows = Set.of_seq arrows}

let startfn _ = Element

let endfn _ = Element

let identity Element = (0,0)

let compose (a,b) (c,d) = ((a + c) % n, (b+d) % n)

let category =

{ Start=startfn; End=endfn; Identity=identity; Compose=compose }

let arrows =

seq {

for i in 0 .. n-1 do

for j in 0 .. n-1 do

yield (i,j)

}

{ Category = category; Arrows = Set.of_seq arrows}

We can then define the Klein four group as a category and validate the representation.

let V4 = CycleGroupProduct 2

CheckFiniteCategory V4

isMonomorphism (0,0) V4

isMonomorphism (1,0) V4

isMonomorphism (1,1) V4

isMonomorphism (1,0) V4

isMonomorphism (1,1) V4

There’s much more to do, but at least we have a start.

Advertisements