Maths - Category Theory - Programming

How do we model categories using a computer program?

There are various impemetations of category theory in various languages:

As far as I can see these implementations model category theory concepts like 'functor' and 'monad' but, they model them in terms of the internal structure of objects wheras the spirit of category theory seems to be to define a structure by its external properties. So I think these libraries are very useful for learning about the concepts, also implementations of things like monads are very useful in their own right (Haskell could not work without it), but I'm not sure if the implemations can be consdidered a general implementation of category theory?

Lets take the example of a functor, the above libraries might model it like this:

Functor: (A ->B) -> (F A -> F B)

Where 'a' and 'b' are object types in the domain category and 'F a' and 'F b' are object types in the codomain category. We need to 'lift' this away from describing in terms of these internal structures to give an external description purely in terms of the functor. There is another more practical issue, which is, we need to map all 'structure' not just unary functions (a -> b) but binary functions ((a,b) -> c) and so on.

As an example lets take a functor that goes from (R,0,+) to (R',1,*) where R is the real numbers and R' is the positive real numbers. We can model this in terms of the internal structure using arbitaty elements x and y (appologies for my misuse of notation):

EXP: (x + y) -> (exp x * exp y)

What we want to do is 'lift' out of the internal elements so that we are working purely in terms of the structure:

EXP: (+ -> *)

I guess one posibility might be to model concrete categories like sets, groups and so on and then model the arrows between them; perhaps as an object or alternativly as a function (domain ->codomain). So if we drill down through these objects we eventually get down to the concept of 'set'. I don't think this is in the spirit of category theory, what we need to do is hide the internals of the category and model the links between them. perhaps we could have an objects called 'category' with virtually no data or procedures, the we could have all the structure in objects which link these catagory objects.

How can we work in a more category theoretic way?

Category theory detemines an object to within an isomorphism, so it will not define an algebra explicitly in terms of what data and functions it contains, there may be more that one way to perform a calculation. We may be able to get more specific by defining a limited number of simple categories, in terms of arrows, the defining other categories by combining already defined categories (see comma categories).


There is a programming language called 'Charity' ( which models the concepts of category theory. This program seems to have been developed in the 1990's and I can't see much sign of ongoing development on the website.


1: X -> X identity
!: Z -> 1 terminal map
<x,y>: W -> X * Y product factorisor
P0: X * Y -> X first projection
P1: X * Y -> Y second projection
C = P0,P1 : X * Y = Y * X product symmetry
Δ = <1,1>: X -> X * X product diagonal map
<v|w>: X + Y -> W coproduct factorisor
b0: X -> X + Y first coprojection
b1: Y -> X + Y second coprojection


functor/mapping/function examples:

nil: 1 -> C nil is a function which takes no inputs and returns a single value
ss: A -> C ss is a function which takesone input and returns a single value
cons: A * C -> C cons is a function which takes two inputs and returns a single value



list (built in)
data list A -> C = nil : 1     -> C
                 | cons: A * C -> C.
the "success or failure" datatype: the datatype of exceptions
data SF A -> C = ss: A -> C
               | ff: 1 -> C.
the coproduct (sum) datatype
data coprod(A, B) -> C = b0: A -> C
                       | b1: B -> C.
the boolean datatype (builtin)
data bool -> C = false | true: 1 -> C.
the natural number datatype
data nat -> C = zero: 1 -> C
              | succ: C -> C.

Inductive Datatypes

bTree - binary tree
data bTree (A, B) -> C = leaf: A           -> C
                       | node: B * (C * C) -> C.

Coinductive Datatypes

data T -> triple(A, B, C) = p0_3: T -> A
                          | p1_3: T -> B
                          | p2_3: T -> C.
data C -> conat = denat: C -> SF(C).
data C -> colist(A) = delist: C -> SF(A * C).
data C -> cobTree(A, B) = debTree: C -> A + (B * (C * C)).

Infinite Datatypes

data C -> infnat = poke: C -> C.
data I -> inflist(A) = head: I -> A
                     | tail: I -> I.
data C -> infbTree(B) = infnode: C -> B * (C * C).

Lazy Datatypes

data Eid A -> C = eid: A -> C.     % eager identify datatype
data C -> Lid A = lid: C -> A.     % lazy identify datatype
data C -> Lprod(A, B) = fst: C -> A
                      | snd: C -> B.
data Lnat -> N = Lzero: 1      -> N
               | Lsucc: Lid(N) -> N.
data Llist(A) -> L = Lnil : 1          -> L
                   | Lcons: A * Lid(L) -> L.

Higher-Order Datatype

The exponetial datatype: the datatype of total functions
data C -> exp(A, B) = fn: C -> A => B.
* the datatype of total, deteministic processes
data C -> proc(A, B) = pr: C -> A => B * C.
* the datatype of partial processes
data C -> Pproc(A, B) = Ppr: C -> A => SF(B * C).
* the datatype of nondeteministic processes
data C -> NDproc(A, B) = NDpr: C -> A => list(B * C).
data S -> stack(A) = push: S -> SF(A) => S
                   | pop : S -> S * SF(A).
data Q -> queue(A) = enq: Q -> SF(A) => Q
                   | deq: Q -> Q * SF(A).


Types of metaprogramming:

In Lisp metaprogramming uses the quasiquote operator (comma) which introduces code that is evaluated at program definition time rather than at run time.

In Axiom this is done by incorporating an interpreter in the program in addition to the compiler. Another language that supports this is Object Pascal.

Type-Level Programming

See this site for type level programming in Scala.

Related Concepts In Language
Metaclass Python
First class modules OCAML
Dependant types  
Type universe  
ADT and GADT - (Generalised) Algebraic Data Type (List, Tuple, Etc.). Product Type - special case of GADT  

metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag The Princeton Companion to Mathematics - This is a big book that attempts to give a wide overview of the whole of mathematics, inevitably there are many things missing, but it gives a good insight into the history, concepts, branches, theorems and wider perspective of mathematics. It is well written and, if you are interested in maths, this is the type of book where you can open a page at random and find something interesting to read. To some extent it can be used as a reference book, although it doesn't have tables of formula for trig functions and so on, but where it is most useful is when you want to read about various topics to find out which topics are interesting and relevant to you.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.