Polynomial functors III What I call "distributive functors" are called "applicative" in the modern functional programming literature.
Despite what I thought previously:
Statement. All polynomial functors are distributive.
Proof.A polynomial functor can be rewritten (up to isomorphism) using a Horner-like formula,
F(t) = c
0 + t*(c
1 + t*(c
2 + t*(... + t*c
n) ...)
Here the "coefficients" c
i are fixed types (independent of "t"): they could be 0, 1, or some nontrivial types.
Now, we will show by induction that F(t) is distributive, that is, there exists a natural transformation F(a)*F(b) ~> F(a*b) of functors C*C->C.
For the base of induction, we need to show that the constant functor F(t)=c (mapping everything to "c") is distributive. This is easy: F(a)*F(b) = c*c, F(a*b) = c. We need a natural transformation c*c ~> c. To produce such a natural transformation, we just ignore one of the factors of "c" (say, the second one).
For the step of induction, we need to show that, for a distributive functor F, the functor c+t*F is distributive. We first show that t*F is distributive:
a*F(a)*b*F(b) ~> a*b*F(a*b) can be constructed since we have already F(a)*F(b) ~> F(a*b).
Now we show that, for a distributive F, the functor c+F is also distributive.
We need to find a natural transformation (c+F(a))*(c+F(b)) ~> c+F(a*b).
The functor on the left is isomorphic to
c*c + c*F(b) + F(a)*c + F(a)*F(b).
To construct a natural transformation from this to c+F(a*b), we need to provide a natural transformation into either "c" or "F(a*b)", for each of the four terms separately.
For any functor G, we have a natural transformation c*G ~> c by simply ignoring the factor G.
So, we can provide natural transformations c*c ~> c, c*F(b) ~> c, and F(a)*c ~> c.
The last term, F(a)*F(b), has a natural transformation to F(a*b) by virtue of F being distributive. So, we can provide the required natural transformation, and c+F is distributive.
Q.E.D.
The dual property is that any polynomial functor F(t) is co-distributive: F(a+b) ~> F(a) + F(b). This can be proved in a different way.
Lemma: If a functor F(t) is co-distributive and either pointed or co-pointed, the functor t*F(t) is also co-distributive.
Proof: We need to construct a natural transformation (a+b)*F(a+b) ~> a*F(a) + b*F(b). First, we use the co-distributivity of F to construct a natural transformation (a+b)*F(a+b) ~> (a+b)*(F(a)+F(b)) = a*F(a) + a*F(b) + b*F(a) + b*F(b). For each of these four terms, we now need to construct a natural transformation to a*F(a) + b*F(b). This is easy for the first and the fourth terms.
For the second term, we need a*F(b) ~> a*F(a) + b*F(b). Consider two cases: either F is pointed, or F is co-pointed.
If F is pointed, we have a natural transformation a ~> F(a). Therefore, we can construct a natural transformation a ~> a*F(a) as well (just repeat the factor "a"). So we also have a*F(b) ~> a*F(a) by ignoring the factor F(b).
If F is co-pointed, we have a natural transformation F(b)~>b. Therefore, we can construct a natural transformation F(b) ~> b*F(b) by just repeating the factor F(b). So we also have a*F(b) ~> b*F(b) by ignoring the factor "a".
In both cases, we can construct the required natural transformation a*F(b) ~> a*F(a) + b*F(b).
Similarly, we show that we can construct the natural transformation b*F(a) ~> a*F(a) + b*F(b).
Q.E.D.
Statement: Any polynomial functor F(t) is co-distributive.
Proof: Any polynomial functor is a sum of "monomial" functors of the form c*t*t*...*t, for some constant type c. A sum of two co-distributive functors is again co-distributive. So it will be sufficient to prove that a monomial functor of the form c*t*t*...*t is co-distributive.
If a functor F is co-distributive, then so is c*F, where c is a constant type. This is so because the natural transformation F(a+b) ~> F(a)+F(b) leads directly to the natural transformation c*F(a+b) ~> c*(F(a)+F(b)) = c*F(a) + c*F(b).
So now it remains to show that "monic monomial" functors of the form t*t*...*t are co-distributive.
We first note that the functor F(t)=t (i.e. the identity functor) is co-pointed. It follows that all "monic monomial" functors of the form t*t*...*t are co-pointed.
Now we use the Lemma and show by induction that t*t*...*t is co-distributive.
Base of induction: the functor F(t)=t is co-distributive.
Step of induction: if F(t)=t*t*...*t is co-distributive, then so is t*F(t) because F is co-pointed and the Lemma holds.
Q.E.D.