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).
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.
|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|
- x = W -> X
- y = W -> Y
- v = X -> W
- w = Y -> W
|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.
|bTree - binary tree||
data bTree (A, B) -> C = leaf: A -> C | node: B * (C * C) -> C.
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)).
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).
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.
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:
- Generative Programming - One program generates code for another program.
- 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.
See this site for type level programming in Scala.
|Related Concepts||In Language|
|First class modules||OCAML|
|ADT and GADT - (Generalised) Algebraic Data Type (List, Tuple, Etc.). Product Type - special case of GADT|