|
| |||
|
|
Polynomial functors VII. Pointed and co-pointed recursive polynomial functors Polynomial functors I. Basic motivations. All polynomial type constructors are functors. Polynomial functors II. Basic definitions: (co)pointed, (co)distributive, (co)monadic. Monadic functors are distributive. Co-pointed functors are co-distributive Polynomial functors III: all polynomial functors are (co)distributive Polynomial functors IV: all polynomial functors are pre-(co)-monadic Polynomial functors V: recursive functors are (co)distributive Polynomial functors VI: how to characterize pairs of functors with natural transformations between them Polynomial functors VII. Pointed and co-pointed recursive polynomial functors (this post) Characterization of co-pointed functors We denote by 0 the initial object in the category. (This is the "void" type, i.e. a type with no values.) As before, we denote by 1 the final object in the category. We assume that they both exist. For example, in Scala the initial object is "Nothing" and the final object is "()". A functor F is co-pointed if there exists a natural transformation to the identity functor, F(t) ~> t. Statement: A polynomial functor F is co-pointed iff there is a morphism F(0) -> 0. Proof: Write the polynomial functor in the distributive normal form: F(t) = c0 + c1*t +c2*t*t + ... Then F(0) = c0. The condition F(0) -> 0 means that c0 = 0, in other words, this term is absent from the distributive normal form. In that case, F(t) = t*G(t) for some functor G(t). This is the same as the condition for the functor F to be co-pointed. Statement: A recursive polynomial functor F is co-pointed iff there is a morphism P(0,0) -> 0 for the defining bifunctor P(t,f). Equivalently, P(t,f) = t*A(t,f) + f*B(t,f) for some bifunctors A and B. Proof: The functor F satisfies F(t) = P(t,F(t)). If we have F(0) -> 0 then we have P(0,F(0)) -> 0. Since 0 is the initial object, we have 0 -> F(0). Since P(t,f) is a functor in the argument f, we can lift 0 -> F(0) to P(0,0) -> P(0,F(0)). Therefore, we can construct P(0,0) -> P(0,F(0))->0 as required. Conversely, if we have P(0,0)->0, we can write P in the distributive normal form and conclude that P(t,f) = t*A(t,f) + f*B(t,f) for some bifunctors A and B. If the bifunctor A is nonzero then we can have a natural transformation P(t,f)~>t. This makes F co-pointed since F = P(t,F). If A is zero but B is nonzero then we have a natural transformation P(t,f)~>f. This gives is the construction of F(t) ~> t recursively: if the functor G is co-pointed then the functor P(t,G) is also co-pointed. Statement: A recursive polynomial functor F is pointed if the defining bifunctor P(t,f) has the form P(t,f) = t^m * f^n + Q(t,f), where m>=0 and n>=0, and Q is some bifunctor. Proof: We will show the recursion step: if G is pointed (i.e. t ~> G(t)) then there is a natural transformation t ~> P(t,G(t)). This is easy since P(t, G(t)) = t^m * G(t)^n + Q, and we have t ~> G(t). So we can construct a natural transformation t ~> P(t, G(t)) by generating the term of type t^m * G(t)^n. |
||||||||||||||