Functors of functors. Deriving the "free monad" The construction of a "free F-monad" looks like this: we take a functor F and create another functor out of it, M
F. However, the way we construct M
F does not use any specific properties of F except the assumption that F is a functor. So, in the category of functors, the construction of M
F out of F is a functor "M" of functors (
FF) that just happens to be applied to F, but could be applied to any other functor. The functoriality of an FF means that it commutes with transforming F by an ordinary natural transformation.
An FF takes any functor F and adds some additional structure around it, without knowing about the specific structure of F. The resulting new functor might have additional properties (such as, being pointed, distributive, or monadic) that F does not necessarily have. The usefulness of FFs comes from the fact that we can guarantee that the resulting new functor will have a given property, whether or not F had that property.
What are other useful functors of functors (
FFs)?
a) Mapping to a specific constant functor C, such as the Identity functor: F ~> C or F ~> Id.
b) Identity transformation, F ~> F.
c) Product of two functors, F ~> F*G where G is another functor.
d) Co-product of two functors, F ~> F + G.
e) Composition of two functors, F ~> F ∘ G.
Statement. All these operations produce functors out of functors. All these operations can be also used on bifunctors.
Proof: straightforward calculations.
As examples, consider the FFs
(f) F ~> Id + F
(g) F ~> Id * F
The result of (f) is the functor t + F(t), the result of (g) is the functor t*F(t). These functors have properties that F does not necessarily have: for instance, t + F(t) is always pointed, while t*F(t) is always co-pointed. As it happens, a co-pointed functor is automatically distributive and co-distributive.
Exercise. Show that a co-pointed functor is always distributive.
Proof. Assuming a natural transformation F(t)~>t, we need to show that F(s)*F(t)~>F(s*t). We first map F(s)~>s by assumption. It remains to show that s*F(t) ~> F(s*t). This is a simple matter of lifting the morphism t -> s*t (for a fixed s) into the functor F. Q.E.D.
In this way, we can add structure to any functor and convert it into a pointed or a co-pointed functor.
Exercise. Find an FF that converts any functor into a functor that is at the same time pointed and co-pointed.
Answer. F(t) ~> t + t*F(t).
Statement: FFs defined using (a) - (e) preserve (co-)pointedness of functors. For instance, if both F and G are (co-)pointed functors, then F+G, F*G, F∘G are also (co-)pointed functors. Also, F+G preserves co-distributivity and F*G preserves distributivity of functors. Functor composition preserves both distributivity and co-distributivity.
Proof: straightforward calculations.
So far, we have used algebraic operations of functors to construct FFs.
All these operations can be used to define an FF recursively.
For example, F(t) ~> F(t) + F(t) + F(t) + F(t) + ... can be defined recursively as
F(t) ~> S
F = F + S
F.
As a nontrivial and important example, consider the following FF:
F ~> Fix(F)
where Fix(F) = F ∘ Fix(F).
The FF we just denoted by "Fix" is a particularly interesting one: it transforms F into F ∘ F ∘ F ∘ ... - an infinite composition of F with itself. The resulting functor Fix(F) is the solution X of the recursive equation
X = F ∘ X.
Now, if we write what X is,
X(t) = F(X(t)) = F(F(F(F(....)...)
we notice that the argument t has disappeared under infinitely many layers of applying the functor F. Indeed, we might expect that the functor Fix(F)(t) maps all t into a fixed type X, which is the "solution" of the recursive "type equation" X = F(X).
We can use Fix(F) in an interesting way if we suppose that the functor F has another type parameter x. Let us assume that F(t,x) is a bifunctor (i.e. a functor in both t and x), and apply Fix to F with respect to x. Let us denote the result by Fix
x(F(t,x)), which will be a functor of a single argument t:
Fix
x(F(t,x)) = F(t,F(t,F(t,...)...).
In other words, Fix
x(F(t,x)) = G(t) where the G satisfies the recursive equation
G(t) = F(t, G(t)).
We can check straightforwardly that G is a functor, and that G preserves certain properties of the bifunctor F.
We will call this functor G(t) the "x-fixpoint" of the bifunctor F(t,x).
Statement. If F(t,x) is a bifunctor then G(t) = Fix
x(F(t,x)) is a functor in t. If F(t,x) is (co-)pointed in t then so is G(t).
Proof. By definition, G(t) = F(t,
G(t)), where the boldface
G denotes the recursive case for which we already have proved that it is a functor. Given a morphism t -> s, we can lift that morphism into the functor F and also into the functor
G, and so we can map F(t,
G(t)) -> F(s,
G(s)), as required.
Now, if F(t,x) is pointed in t then we have t ~> F(t,x) for any x. In particular, we have t ~> F(t,
G(t)). So, G(t) is also pointed. Similarly for the case of co-pointed F(t,x).
Q.E.D.
What if F(t,x) is pointed or co-pointed in x and not in t? It turns out that its x-fixpoint G(t) is then also pointed or co-pointed in t. However, this property may be unusable in practice, because the inductive proof has no base case and simply keeps descending down the recursive application of F. So the result of the morphism t -> G(t) might be an infinite type.
Statement. If F(t,x) is (co-)pointed in x, its x-fixpoint G(t) = Fix
x(F(t,x)) is (co-)pointed in t.
Proof. Assuming that we have x -> F(t,x), we are required to find a morphism t -> G(t) = F(t,
G(t)). By inductive assumption, we already have a morphism x -> F(t,x) for any x. Setting x =
G(t), we get a morphism
G(t) -> F(t,
G(t)) as required.
Q.E.D.
However, this property may be unusable
in practice, because the inductive proof has no base case; so the result of the morphism t -> G(t) might turn out to be an infinite
type that has no finite values and cannot be used in programming. Here is an example when this happens: Consider F(t,x) = x*(1+t). This bifunctor is both pointed and co-pointed in x (but not in t). Its fixpoint is the infinite product functor G(t) = (1+t)*(1+t)*... The result of injecting t -> G(t) using the construction in the proof above would be a value of type (0+t)*(0+t)*..., which is an infinite product type.
For certain functors F(t,x), the x-fixpoint functor G(t) = Fix
x(F(t,x)) has additional properties. In particular, we are interested in functors F(t,x) for which the x-fixpoint could be a monad. For that, we need G to be pointed and pre-monadic.
Theorem: If F(t,x) is a bifunctor of the form F(t,x) = A(x) + t*B(t,x) for some functor A and bifunctor B, then G(t) = Fix
xF(t,x) is pre-monadic as a functor of t. That is, there exists a natural transformation G(G(t)) ~> G(t).
Proof: We will omit the specific arguments of B(...) for brevity, since we will not need to use them in the proof. We have G(G(t)) = F(G(t),
G(G(t))) = A(
G(G(t))) + G(t)*B(...), and we are required to map this to G(t) = A(G(t)) + t*B(...). Thus we are required to map A(
G(G(t))) ~> G(t) and G(t)*B(...) ~> G(t) separately. We assume that we already have a morphism
G(G(t)) ~> G(t) by the inductive assumption. Lifting this morphism into the functor A, we get A(
G(G(t))) -> A(G(t)). The latter type is the left variant of G(t). It remains to map G(t)*B(...) -> G(t), which is the left projection from pair.
Q.E.D.
The significance of this theorem is that we can construct a large class of pre-monadic functors simply by taking x-fixpoints of bifunctors of the form F(t,x) = A(x) + t*B(t,x). If F(t,x) is of this form and also is t-pointed, its x-fixpoint will be a monad. For F(t,x) to be t-pointed, we need either A(x) or B(t,x) to be t-pointed. Simplest examples of bifunctors F(t,x) that satisfy these conditions and yield nontrivial monads are
F(t,x) = 1 + t*1 (the x-fixpoint of this is equal to F(t) and is the "Option" monad)
F(t,x) = 1 + t*x (the x-fixpoint of this is the familiar "List" monad)
F(t,x) = 0 + t*(1+x) (the x-fixpoint of this is the
non-empty list)
F(t,x) = x*x + t*1 (the x-fixpoint of this is a binary tree)
F(t,x) = A(x) + t (the x-fixpoint of this is the free A-monad)
Now, we obtain a corollary that I was struggling to prove by more elementary methods:
Corollary. All recursive polynomial functors are pre-monadic.
Proof. Recursive polynomial functors are defined as x-fixpoints of polynomial bifunctors F(t,x), which always have the form A(x)+t*B(t,x).
Exercise 1: Functors A, F, G are such that there exist natural transformations A ~> F and A ~> G. Show that there exist natural transformations A ~> F+G, A ~> F*G, A ~> F∘G.
Proof for A ~> F∘G: We first lift A ~> G into the functor F and obtain F(A(t)) ~> F(G(t)). Now we are trying to produce A(t) -> F(A(t)). This is done by first making A(t) -> F(t) by assumption, and then using the chain of the following two morphisms: A(t)*F(t) -> F(A(t)*t) -> F(A(t)). This chain is obtained by lifting into the functor F of the composition of morphisms t -> A(t)*t (with the given A(t)) and A(t)*t -> A(t) (projection from pair).
Q.E.D.
Exercise 2: Given functors F, G, M such that M is pre-monadic and there exist natural transformations F ~> M and G ~> M, show that there exist natural transformations F + G ~> M, F * G ~> M, and F ∘ G ~> M.
Exercise 3: Show that N(t) = Fix
x(t*P(x)) is a comonad for any functor P.
Proof: N(t) is co-pointed since t*P(x) is t-co-pointed. It remains to construct a morphism N(t) -> N(N(t)), which is the same as N(t) = t*P(
N(t)) -> N(t)*P(
N(N(t)). So, we need to construct two separate morphisms
t*P(
N(t)) -> N(t) (this is identity since both sides are equal to N(t))
and
t*P(
N(t)) -> P(
N(N(t)).
Here we will ignore the factor t.
The morphism
N(t) ->
N(N(t)) exists by inductive assumption, and we lift it to the functor P and obtain P(
N(t)) -> N(t)*P(
N(N(t)) as required.
Q.E.D.
Questions: Is N(t) from Exercise 3 a "free P-comonad"? How to derive free monads and free comonads systematically, rather than by trial and error? What is a way to derive Id + F as a "free pointed functor" or Id * F as a "free co-pointed functor" systematically? Is there a way of constructing a "free distributive functor" without making a pointed functor first?