Polynomial functors II I'm fascinated with the mysterious properties of polynomial functors. A lot of what I initially expected to hold about them turned out to be incorrect. Perhaps the intuition about them will be useful for applications in computer science.
Also, to a programmer, polynomial functors are much more obviously useful as examples of functors than any examples drawn from abstract mathematics. If I wanted to explain to programmers why category theory is at all relevant to practical programming, I'd rather use polynomial functors as examples.
At the same time, looking at polynomial functors (which represent "generic data containers") will help programmers understand natural transformations. From the programmer's point of view, a natural transformation is a function that transforms one kind of data container into another, while being "completely generic" about the type of data stored in the container.
Some definitionsWe always work in a fixed category C. We assume that the category C contains the terminal object "1", and that it always contains products (a*b) and sums (i.e. co-products, a+b) for any pair of objects a,b. In an application to programming, objects of the category C are the available types in some (functional) programming language. Morphisms of C are the available functions (each taking one argument of some type, and returning one value of some type). Functors correspond to polymorphic data types.
Definition. A
polynomial functor is a functor C->C defined as either a
constant functor F(t)=b (where b is a fixed object), or the
identity functor F(t)=t, or a product of two polynomial functors F(t)*G(t), or a sum of two polynomial functors F(t)+G(t).
The definition of polynomial functor is consistent because the sum and the product of two functors is also a functor.
Definition (not quite rigorous). A
recursive polynomial functor is defined as the "largest" functor F that satisfies a polynomial fixed-point equation of the form
F(t) =(isomorphic to)= P(F(t)), where P is some polynomial functor.
(The "isomorphism" of functors is defined via natural transformations.)
For example, an important functor is
List, which represents a (finite or infinite) list, a fundamental data structure widely used in functional programming. It is a recursive polynomial functor defined by
List(t) = 1 + t*List(t).
It is tempting to "solve" this equation by writing
List(t) = 1 + t + t*t + t*t*t + ...
but the infinite sum in this formula is hard to make rigorous.
Another important recursive polynomial functor is
BinaryTree:
BinaryTree(t) = t + BinaryTree(t)*BinaryTree(t).
One can prove that any recursive polynomial functors are truly functors, with the function
fmap: (a->b)->(F(a)->F(b)) defined recursively. A sufficiently sophisticated compiler will be able to derive the code for
fmap automatically, for any user-defined polynomial or recursive polynomial data type!
Some propertiesIn most applications to functional programming, and especially for deciding the properties of functors, it suffices to distinguish functors only up to isomorphism (defined using natural transformations). However, sometimes it is still important (for specific applications) to distinguish a+b from b+a, or even to distinguish the order of the two factors in a*a.
If we consider polynomial functors only up to isomorphism, it makes sums and products commutative, and "1" a multiplicative unit. Polynomial functors become quite similar to ordinary polynomials.
Statement. Any polynomial functor F is isomorphic to a functor in a distributive normal form:
F(t) = c
0 + c
1*t+c
2*t*t+...
where c
i are fixed ("constant") types.
Proof: by induction on the definition of a polynomial functor.
It seems to be important to understand when two polynomial functors are related by a natural transformation. In general, for a given polynomial functor F(t), I'd like to characterize all other polynomial functors G(t) such that there exists a natural transformation F~>G or G~>F. How to characterize them? Division of polynomials does not seem to help here...
So far I have been looking at specific examples such as these:
Statement: If there exists a natural transformation from F(t) to the identity functor then F(t) must be a "homogeneous" polynomial functor (with no coefficient c
0). Such F(t) is equivalent to t*G(t) where G(t) is any functor.
Statement: If there exists a natural transformation from the identity functor to F(t) then F(t) is equivalent to the sum of some functor G (which could be 0) and a polynomial "with unit coefficients", that is, a polynomial functor such that all c
i are polynomial in the unit type "1", and contain no other fixed types.
Statement: If there exists a natural transformation from a constant functor "c" to F(t), where "c" is a type which has no naturally defined morphism 1->c, then F(t) must be equivalent to a constant functor P(c), for some polynomial functor P.
Distributive functorsDefinition. A functor F(t) is
distributive if there exists a natural transformation F(a)*F(b) ~> F(a*b), where both sides are understood as functors C*C -> C.
A functor is
co-distributive if there exists a natural transformation F(a+b) ~> F(a)+F(b). Again, both sides of the natural transformation are to be understood as functors C*C -> C.
Note that the natural transformations F(a*b) ~> F(a)*F(b) and F(a)+F(b) ~> F(a+b) always exist by virtue of F being a functor. But the reverse transformations do not always exist.
For example, the functor F(t)=c+t is not distributive; F(t)=c*t is not co-distributive. (Here, c is a "nontrivial", fixed object, for which there is no natural morphism 1->c.)
Distributive functors are important for programming because they represent a concept of "containers of data" over which one can "conveniently iterate", in a certain precise sense. For example,
List is distributive, and so one can transform a pair of two lists into a list of pairs. However,
List is not co-distributive: a list of co-pairs "a+b" cannot be transformed into a co-pair of lists.
The significance of co-distributivity for practical programming is not immediately obvious to me. However, so far the experience taught us that category-theoretic constructions are always eventually found to be useful for functional programming, and that dual constructions sometimes need to wait longer until their use is discovered.
Statement: Functors F(t)=c and F(t)=t are distributive and co-distributive. If F and G are distributive, F*G is also distributive. If F and G are co-distributive, F+G is also co-distributive.
To me, the importance of recognizing the existence of natural transformations between polynomial functors is given by this property:
Statement: If there exists a natural transformation F ~> G between distributive functors F and G, the functor F+G is again distributive. Similarly, for co-distributive F, G, the functor F*G is co-distributive.
The proof is pretty easy. However, I'd like to strengthen this statement to say that if a natural transformation does not exist as neither F~>G nor G~>F, the functor F+G will not be distributive. I don't yet know how to prove that.
Monadic functorsDefinition: A functor F is
pointed if there exists a natural transformation Id ~> F (where Id is the identity functor).
Definition: A functor F is
monadic if it is pointed and, additionally, if there exists a natural transformation F.F ~> F, where F.F is the composition of F with itself, i.e. the functor F(F(t)).
Example: The functor F(t)=1+t is monadic.
Pointed polynomial functors can be characterized as those with "unit" coefficients. However, I'm not sure yet how to characterize polynomial functors that are monadic.
Statement: If there exists a natural transformation F.F ~> F then F is distributive.
Corollary: A monadic functor is distributive.
The proof is a somewhat non-obvious calculation, and I'd like to know how to get an "elegant" argument. Or, perhaps, there is no such argument because the statement is only true for categories C that correspond to programming languages, and I'm unaware of some other required properties of C?
Proof (not quite rigorous): Since the category C has products, then for any b we have a morphism
*b: a -> a*b. We can lift this morphism into the functor F and get a morphism F(a)->F(a*b). This is the same as to say that, in our programming language, we have code that computes a value of type F(a*b) given a value of type F(a) and any value of type
b. Since this is defined for any
b, we can rearrange the code so that it is a function of type F(a)->b->F(a*b). In other words, for any value of type F(a), it computes a function of type b -> F(a*b). Now, we can lift this function into the functor F and obtain a morphism F(b) -> F(F(a*b)). We can apply the monadic natural transformation F.F~>F to obtain F(a*b) instead of F(F(a*b)). So now we have a morphism F(a)->F(b)->F(a*b). Finally, we observe that this is equivalent to a morphism F(a)*F(b) -> F(a*b).
The importance of monadic functors in functional programming cannot be underestimated. Many recursive polynomial functors (such as the data containers
List and
Tree) are monadic. Widely used asynchronous concurrency primitives such as "promises" and "futures" are monadic. "Reactive streams" are monadic. The entire input/output system of Haskell is implemented via a monadic functor, and many standard libraries and data structures expose a monadic interface. In Scala, the
database interface library "Slick" invites the user to code all relational database operations as monadic functor applications.
When a programmer defines a new data type (usually, a polynomial functor), it would be quite useful to be able to determine (automatically?) whether this functor is distributive and/or monadic, or perhaps co-distributive or co-monadic. How to do that? Are there some classification theorems?