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

## Charity

There is a programming language called 'Charity' (http://pll.cpsc.ucalgary.ca/charity1/www/home.html) 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.

terminology

 1: X -> X identity !: Z -> 1 terminal map : 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 : X + Y -> W coproduct factorisor b0: X -> X + Y first coprojection b1: Y -> X + Y second coprojection

where:

• x = W -> X
• y = W -> Y
• v = X -> W
• w = Y -> W

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

#### utilities:

 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

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

#### Infinite Datatypes

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

#### Lazy Datatypes

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

#### Higher-Order Datatype

 exp ```The exponetial datatype: the datatype of total functions data C -> exp(A, B) = fn: C -> A => B.``` proc ```* 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).``` stack ```data S -> stack(A) = push: S -> SF(A) => S | pop : S -> S * SF(A).``` queue ```data Q -> queue(A) = enq: Q -> SF(A) => Q | deq: Q -> Q * SF(A).```

### Metaprogramming

Types of metaprogramming:

• Generative Programming - One program generates code for another program.
• Incremental Compilation - This allows code to be generated or modified when the program is running and either compiled incramentally or interpreted at runtime. Its easier for interpreters, programs which allow this include: Forth, Frink, Groovy, JavaScript, Lisp, Lua, Perl, PHP, Python, REBOL, Ruby, Smalltalk, and Tcl.
• DSL - such as lex and yacc

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

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.

 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.