What is the relation between functors in SML and Category theory?

Question

Along the same thinking as this statement by Andrej Bauer in this answer

The Haskell community has developed a number of techniques inspired by category theory, of which monads are best known but should not be confused with monads.

What is the relation between functors in SML and functors in Category theory?

Since I don't know about the details of functors in other languages such as Haskell or OCaml, if there is info of value then please also add sections for other languages.

Answer 1

Categories form a (large) category whose objects are the (small) categories and whose morphisms are functors between small categories. In this sense functors in category theory are "higher size morphisms".

ML functors are not functors in the categorical sense of the word. But they are "higher size functions" in a type-theoretic sense.

Think of concrete datatypes in a typical programming language as "small". Thus int, bool, int -> int, etc are small, classes in java are small, as well structs in C. We may collect all the datatypes into a large collection called Type. A type constructor, such as list or array is a function from Type to Type. So it is a "large" function. An ML functor is just a slightly more complicated large function: it accepts as an argument several small things and it returns several small things. "Several small things put together" is known as structure in ML. In terms of Martin-Löf type theory we have a universe Type of small types. The large types are usually called kinds. So we have:

1. values are elements of types (example: 42 : int)
2. types are elements of Type (example: int : Type)
3. ML signatures are kinds (example: OrderedType)
4. type constructors are elements of kinds (example: list : Type -> Type)
5. ML stuctures are elements of kinds (example: String : OrderedType)
6. ML functors are functions between kinds (example: Map.Make : Map.OrderedType -> Make.S)

Now we can draw an analogy between ML and categories, under which functors correspond to functors. But we also notice that datatypes in ML are like "small categories without morphisms", in other words they are like sets more than they are like categories. We could use an analogy between ML and set theory then:

1. datatypes are like sets
2. kinds are like set-theoretic classes
3. functors are like class-sized functions

Answer 2

A Standard ML structure is akin to an algebra. Its signature describes an entire class of algebras of similar shape.

A Standard ML functor is a map from a class of algebras to another class of algebras. An analogy is, for instance, with the functors $F : {\bf Mon} \to {\bf Grp}$, which adds an inverse operation to monoids, or $F : {\bf Ab} \to {\bf Rng}$ which adds a multiplicative monoid to abelian groups to make rings.

Most of these ideas were worked out in series of papers by Burstall and Goguen in designing a specification language called CLEAR (References c5 and c6 on the DBLP page.) David MacQueen was working jointly with Burstall and Sannella at that time, and was intimately familiar with the issues. The Standard ML module system is based on these ideas.

What most people would wonder is, what about morphisms? Category theoretic functors have an object part and a morphism part. Do Standard ML functors have the same? The answer is YES and NO.

• The YES part of the answer applies if the structures are first-order. Then, there are homomorphisms between different structures of the same signature, and Standard ML functors automatically map them to homomorphisms of the result signature.
• The NO part of the answer applies when the structures have higher-order operations.

Does this mean that Standard ML is deviating from category theory? I don't think so. I rather think that Standard ML is doing the right thing, and category theory is yet to catch up. Category theory doesn't yet know how to deal with higher-order functions. Some day, it will.

Answer 3

There is, to the best of my knowledge, no formal relation between functors in category theory and functors in ML (SML or OCaml, they're close enough for our purpose here).

In category theory, functors are functions that operate on objects. They are one level above morphisms, which are often functions that operate on elements (many categories have objects that are sets with some algebraic structure and arrows that are homomorphisms between these structures). An ML functor is a function that operates on modules, one level above the functions that operate on core language values. I think the resemblance stops here.

ML functors were baptized by Dave McQueen in his 1985 revision of Modules for Standard ML (citeseerx) that appeared in the Polymorphism Newsletter (the original paper used the expression “parametric module” — later publications tend to use the adjective “parametrized”). Unfortunately, I can't locate a copy of that paper. In his 1986 paper Using Dependent Types to Express Modular Structure (citeseerx) he gives the name as established.