Josh Dybnis on 19 Feb 2004 22:18:34 -0000 |
[Date Prev] [Date Next] [Thread Prev] [Thread Next] [Date Index] [Thread Index]
Re: [ALACPP] [OT] Ocaml and category theory |
--- 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