Re: [ALACPP] [OT] Ocaml and category theory

[Josh Dybnis <jdybnis@xxxxxxxxx>]

--- Kevin Scaldeferri <kevin@xxxxxxxxxxxxxxx> wrote:
> Anyway, this all has basically nothing to do with C++ (except that
> C++ has yet another [completely unrelated] concept of "functors"...)

Well it has some relevance to C++ because C++'s templates are based on
ML's type system. ML's functors exist to work around some limitations
in ML's type system.

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

Any function/module in ML can be generic, not just functors. The whole
ML type system is built around generics and any parameter can have an
unspecified type. Its expressive power lies somewhere between Java
generics and C++ templates. For example unlike in C++, you are not
allowed to do anything in a function's definition that depends on the
specifics of a parameter with an unspecified type. This would be like a
C++ template where you were not allowed to call member functions on any
object thats class is a template parameter.

The reason C++ templates don't have the same limitations as ML is that
conceptually C++ is compiled in two stages where the first stage is
untyped. So after the first stage, a class may have been substituted
into a template even if the class does not include the methods that the
template definition tries to invoke on its objects. This kind of error
is not caught until the second stage of compilation, when the normal
C++ rules are used to typecheck the code output of the template. 

ML does not do it the C++ way because that makes separate compilation
of generics a real bitch (among other things). Evidenced by how
difficult it turns out to be to implement the 'export' keyword in C++.
It would be an even bigger problem in ML since every single function
can be generic. The ML solution is to just say that no operations can
be performed on parameters with unspecified types. 

Java gets around the problem by allowing you to specify that a generic
parameter extends a class or implements a specific interface. ML can't
do this because it's type system does not include inheritance.  Instead
ML works around the limitation with what it calls "functors". ML
functors are parameterized modules, where you can tell the compiler
which operations will work on a given parameter, but without tying down
the specific representation of the parameter. This makes a module
signature into a kind of abstract class. But unlike Java where every
object is cast to Object inside a generic method, functors are more
like C++ templates in that each instance gets its own distinct type.

> Now, my problem is that there's nothing [in Caml] 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.
> ...
> 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.

Another example is the category of sets and functions (not C++
functions but mathematical functions, i.e. a kind of binary relation
between elements of one set and another). The "objects" of the category
are the sets, and the "morphisms" of the category are the functions.
This satisfies the definition of a category because the existence of
the identity function for every set, and the fact that function
composition (i.e. applying a function to the result of another
function) is an associative operation (meaning that if you compose a
sequence of functions it doesn't matter if you start with the first
pair or the last pair in the sequence).

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

An important point is that the objects of a category have no internal
structure. In mathematics that is synonymous with not being able to
perform any operations on them. Even something like a set has no
structure to it when looked at as an object of a category, even though
it is normally defined as a structure containing elements. However, we
can get around this problem with functors. For example, cartesian
product is a functor that allows us to build sets which we know contain
pairs of elements. Then we can perform operations on them like
projecting out the first and second elements. The funny thing is that
we can apply the same functor to other categories and automatically get
products for other kinds of objects besides sets. That is something to
appreciate about category theory, it ties together a general notion
like product that appears in many different contexts.

Continuing the example of cartesian products, we write the this functor
as A x B. I will describe it as an operation between "objects" (sets in
this case) that also applies to the "morphisms" (functions between
sets). If A and B are sets, then their product A x B is another set,
which is defined as all pairs of elements with the first in A and the
second in B. Then for the "morphisms", if f : A -> B and g : X -> Y are
functions then (f x g) : (A x X) -> (B x Y) is another function which
is defined as (f x g)(a,x) = (f(a),g(x)). This functor goes from a
category to itself. We can use it to go back and define projection
functions in the category, one going from each product to each of it's
two constituent sets.

Functors in category theory give structure to objects and morphisms
which have an unknown structure. Analogously, "functors" in ML allow us
apply operations to modules with unspecified types, i.e. types that
have an unknown structure. I think that is why they are called
"functors". To understand what is meant by an unspecified type in this
context it is important to note that a module's signature is not
considered it's type. Even though a signature includes the type of a
module's operations, it does not define a module's internal
datatype(s). 

As for the question of what categories ML "functors" operate on, I
don't really know. Probably the objects of the categories are types,
and maybe the morphisms are the functions in a module. I haven't seen
any of it spelled out in the papers I looked at. But you could probably
find it in a paper from the late 80's when the ML module system was
first proposed.

(BTW, my feeling is that this post is an example of how it is usually
easier to explain something in its own terminology, than it is to first
explain category theory and then use it to explain what you are after.
Understanding an ML "functor" is much easier than understanding a
functor in category theory.)

links to some papers:

http://wwwhome.cs.utwente.nl/~fokkinga/mmf92b.html
http://citeseer.nj.nec.com/tofte96essentials.html

A disclaimer: I don't actually use ML, category theory, C++, or Java
for anything. So don't take any of this as gospel.

-Josh

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