[ALACPP] [OT] Ocaml and category theory

[Kevin Scaldeferri <kevin@xxxxxxxxxxxxxxx>]

During lunch it briefly came up that ostensibly the (O)Caml language 
has some connection to category theory (that's what the C stands for), 
and that there are some relatively impenetrable papers out there 
wherein it is explained that various language features are "simply" 
explained as some type of category.

Now, I know a little bit about OCaml and a little bit about category 
theory, and I could never quite figure out this connection (nor did 
asking profs or TAs yield enlightenment.)  So, let me explain the 
problem:

So, basically, a category is a bunch of thingies and a bunch of 
morphisms, which are gadgets which connect one thingie to another 
thingie.  (Usually a "thingie" is called an "object", but there's not 
really any more information there, and it could lead to confusion with 
OO "objects".)  There are some rules that morphisms have to obey, 
basically that they can be composed and that composition is 
associative.  A fairly well known example is the category of groups, in 
which the thingies are groups and the morphisms are group homomorphisms.

Now, things get interesting when you introduce what are called 
functors.  A functor is a gadget which maps between two categories, 
taking thingies to thingies and morphisms to morphisms in a way that 
makes sure that the morphisms work right in the target category.

This is only the tip of the category theory iceberg, but it's enough to 
explain my problem.

In Caml, there are module types, which are basically like Java 
interfaces, and there are modules, which are basically like concrete 
classes, and then there are "functors", which are sort of like 
templates/generics, in that they have a slot where you stick in a 
module of some type, and you get out a module of some other type.  Now, 
my problem is that there's  nothing here that I can interpret as a 
morphism.  We've got thingies in category A (modules of type A) being 
mapped to thingies in category B (modules of type B), but I was never 
able to figure out what takes the part of morphisms.


Anyway, this all has basically nothing to do with C++ (except that C++ 
has yet another concept of "functors" which aren't actually real 
functors, but then no one ever claimed that the "C" in C++ stood for 
"category".)  But, if anyone has an answer to this anyway, or if Josh 
want to post a link to any of the papers he was mentioning, I'd be 
interested to hear it.


Kevin

_______________________________________________
alacpp mailing list
alacpp@xxxxxxxxxxx
http://lists.ellipsis.cx/mailman/listinfo/alacpp