Polynomial functors IX. Pre-monadic and pre-comonadic recursive functors All recursive polynomial functors are pre-monadic, as I showed earlier. In the previous post, I tried to see whether they are also pre-comonadic, but I was only able to derive a weaker result that they are pre-comonadic if the defining bifunctor F(t,x) has the form A(x)*B(t).
In this post, I relax this assumption and prove that all recursive functors defined as
G(t) = Fix
xF(t,x),
for any bifunctor F, are pre-comonadic. This provides a large class of pre-comonadic recursive functors that also covers all recursive polynomial functors. In fact, the same construction shows that
any functor is pre-comonadic (although perhaps not in the most interesting way)!
I will also prove a stronger result for pre-monadic recursive functors: any recursive functor defined as Fix
xF(t,x)) is pre-monadic if there exist natural transformations
A(x) ~> F(t,x) ~> t + A(x)
for a suitable functor A.
Using these results, we can generate monadic and comonadic functors out of various bifunctors, including non-polynomial bifunctors.
Theorem 1. The recursive functor G defined by
G(t) = Fix
xF(t,x),
for any bifunctor F, admits a natural transformation G(t) ~> G(G(t)). (I.e. G is pre-comonadic.)
Proof. The functor G satisfies G(t) = F(t, G(t)). We need to produce a natural morphism
G(t) = F(t,
G(t)) ~> F(G(t),
G(G(t)), where the boldface
G denotes a functor for which this natural morphism already exists by inductive assumption. We can produce this morphism by lifting two morphisms p and q into the bifunctor F: the first morphism is p: t -> G(t), and the second is q:
G(t) ->
G(G(t)). The first morphism is simply returning the constant value g of type G(t) that we start with on the left-hand side, p = const g. The second morphism, q, exists by the inductive assumption.
Q.E.D.
Corollary. All recursive polynomial functors are pre-comonadic.
Example: List as a pre-comonadTo illustrate this construction, let us consider the familiar functor "List".
List(t) = 1 + t*List(t).
This is a recursive polynomial functor defined through the bifunctor F(t,x) = 1 + t*x as List(t) = Fix
xF(t,x).
Usually we think of List as a monad, not a comonad. This is true - List is not a real comonad because it lacks the co-pointed property. However, Theorem 1 says List is a pre-comonad, in that it at least admits the transformation List(t) -> List(List(t)). Let us see how this transformation works on a specific value of type List(t), for instance, on the list [a,b,c] of type List(t).
The transformation List(t) ~> List(List(t)) is defined recursively as follows. The base case is the empty list, which is the left variant of F(t,x) = 1 + t*x, that is,
g = 1 : 1 + 0 -- as a variant of 1 + t*x = F(t,G(t)) = G(t).
According to the construction in the proof of Theorem 1, this variant is transformed by first lifting the two morphisms p and q into the bifunctor F, and then by acting with the resulting morphism on 1+0. However, the bifunctor F(t,x)=1+t*x is such that lifting anything into that bifunctor will always act on 1+0 by just leaving 1+0 unchanged. So the result of transforming an empty list of type List(t) is again an empty list (but that empty list is of type List[List(t)]).
Now we apply the transformation to the value [a,b,c] of type List(t). This value is represented in the recursive step as 0 + a*[b,c], where [b,c] is again of type List(t). We lift the morphisms p: t -> [a,b,c] and q: List(t)->List(List(t)) into the functor F(t,x)=1+t*x, and apply the resulting morhpism to 0 + a*[b,c]. The result is 0 + [a,b,c]*q([b,c]). This is repeated recursively to yield
0 + [a,b,c]*(0 + [b,c]*(0 + [c]*(0 + []*(1 + 0)). This value of type List(List(t)) can be written more conventionally as a nested list
[ [a,b,c], [b,c], [c], []]
This is the result of transforming [a,b,c] into the type List(List(t)) using the comonadic property that is automatically present in all recursive polynomial functors.
Any functor is pre-comonadicSince Theorem 1 has no restrictions on the bifunctor F(t,x), we may choose F so that it does not depend on x. In this case, there is no recursion and G(t) = F(t). Theorem 1 still says that the functor G is pre-comonadic. How does this work? Given a functor G, we need to construct a natural transformation G(t) ~> G(G(t)). Given a value g of type G(t), we take the constant morphism t -> G(t) that always returns the same value g, and lift this into the functor G(t). We obtain a morphism G(t) ~> G(G(t)) as required.
Applying this to the List functor, we transform [a,b,c] into
[ [a,b,c], [a,b,c], [a,b,c] ].
This has the right type (and satisfies the comonad's associativity law, something we will be checking explicitly later). However, one may argue that this comonad transformation is "less interesting" than the one we saw previously, when we considered List as a recursive polynomial functor.
Pre-monadic functorsWe will now return to considering pre-monadic functors and relax the previously held restrictions on constructing pre-monadic recursive functors.
Theorem 2. The recursive functor G defined by
G(t) = Fix
xF(t,x)
is pre-monadic if F is a bifunctor such that there exist natural transformations
A(x) ~> F(t,x) ~> t + A(x), for a suitable functor A.
Proof. The functor G satisfies
G(t) = F(t,
G(t)).
We need to produce a natural morphism
G(G(t)) = F(G(t),
G(t)(G(t))) -> F(t,
G(t)) = G(t),
where we may assume inductively that the morphism
G(G(t)) ~>
G(t) already exists.
First, we use the given natural transformation F(t,x) ~> t+A(x) to map
F(G(t),
G(t)(G(t))) ~> G(t) + A(
G(t)(G(t))).
The first term is trivially mapped to G(t). The second term is first mapped to A(G(t)) by the inductive assumption and then into F(t,G(t)) by the given natural transformation A(x) ~> F(t,x).
Q.E.D.
Note that the functor G defined in Theorem 2 will be automatically fully monadic if we strenghten the condition for F to
t + A(x) ~> F(t,x) ~> t + A(x),
because this will yield a natural transformation t ~> F(t,x) and thus a natural transformation t ~> G(t).
The resulting monad will be layered: there will be a natural transformation G(t) ~> t + 1, obtained from G(t) ~> t + A(G(t)) by mapping the second term in the right-hand side into 1 (the unit type).