Maths - Category Theory - Programming

How do we model categories using a computer program?

There are various impemetations of category theory in various languages:

• Haskell: Category extras
• Scala: Scalez
• Aldor: sandbox

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

where:

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

functor/mapping/function examples:

utilities:

data list A -> C = nil : 1     -> C
                 | cons: A * C -> C.

data SF A -> C = ss: A -> C
               | ff: 1 -> C.

data coprod(A, B) -> C = b0: A -> C
                       | b1: B -> C.

data bool -> C = false | true: 1 -> C.

data nat -> C = zero: 1 -> C
              | succ: C -> C.

Inductive Datatypes

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

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.

EuclideanSpace

home

Prerequisites

This page discusses how to model category theory in a computer program.

For a discussion about the theoretical links between category theory and computing see this page.

For a discussion about modelling datatype see this page.

Set Symbols

Group Theory

Functional Programming and Category Theory