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

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