All (recursive) polynomial functors are traversable
Applicative, monadic, and traversable functors are among the most widely used types of functors in functional programming.

A functor A is called applicative if there exist two natural transformations: t ~> A t  ("point") and A s × A t ~> A (s × t) ("apply"). These natural transformations must additionally satisfy the laws of identity and associativity.

A functor T is called traversable if, for any applicative functor A, there exists a natural transformation T(A t) ~> A(T t) called "sequencing". This natural transformation should commute with A's defining natural transformations. For instance, the "point law" must hold, i.e. the A-point injection T t ~> A (T t) must be the same as the T-lifted A-point injection T t ~> T(A t) followed by the "sequencing" transformation T(A t) ~> A (T t).

An equivalent property is the existence of a natural transformation T(A t) × (t -> r) ~> A(T r), called "traversal".

In practice, a traversable functor T is a "parallelizable" data container: an applicative functor A represents a parallelizable computation context, and the traversability means that we can apply that computation context to the data in T in parallel.

A typical example is T = List and A = Future. (The "Future t" type represents a "delayed computation" with result of type t). The traversability property T (A t)  × (t -> r)~> A (T r) means that the "traversal" can trasform  List( Future t) into Future (List r) if we are given a simple transformation function of type t -> r. In other words, we can perform a delayed computation on each element of the list in parallel, and get the final result as a delayed list of transformed elements (of type r).

The reason that the List functor is traversable is that List is a recursive polynomial functor. We will now see that such functors are all traversable. We begin with non-recursive polynomial functors.

Statement 1. All polynomial functors are traversable.

Proof. Any polynomial functor P can be constructed by induction as either a constant functor, or an identity functor, or a product of polynomial functors, or a sum (i.e. co-product) of polynomial functors.  The identity functor is obviously traversable. It is easy to show that the constant functor is traversable:

Constant functor is defined as C t = c where c is a fixed type. The required natural transformation is therefore c ~> A c. This is the "point" transformation of the applicative functor A.

Now it remains to show that if functors P and Q are traversable then so are the functors P × Q and P + Q.
This is equivalent to finding natural transformations
(*) A (P t) × A (Q t) ~> A (P t × Q t)  and
(**) A (P t) + A (Q t) ~> A (P t + Q t).

The n.t. (*) exists due to applicative functor n.t. A a × A b ~> A (a × b) for any types a, b.
The n.t. (**) exists due to the natural transformation A a + A b ~> A (a + b) that holds for any functor A.

Q.E.D.

Thus, functors such as F t = 1 + t (the "maybe" or "option" functor) and G t = t × t (the pair) are traversable.

Example of a non-traversable functor:

Consider the (non-polynomial) functor F t = c -> t where c is a constant, fixed type. This functor is not traversable because the property F (A t) ~> A (F t) means (c -> A t) -> A(c -> t). This property (which I elsewhere called "rigidity") cannot hold for all applicative functors A. For instance, it does not hold even for such a simple applicative functor as A t = 1 + t. It is impossible to transform (c -> (1+t)) into 1 + (c->t) because the function c -> (1+t) could yield either 1 or t for different values of c, and so we cannot extract a total function of type c -> t out of a function of type c -> (1 + t) (we might have some values of c for which we don't have a corresponding value of t). Therefore we are forced to return 1 for all arguments, i.e. the only natural transformation of type (c -> (1+t)) ~> 1 + (c->t)  is actually of type (c -> (1+t)) ~> 1 + 0. In other words, we have lost all information about the mapping c -> t. This does not look right.

This natural transformation is indeed too lossy, -- it does not satisfy the "point law". To see that, we set t = c and consider a function id: c -> c as a value of type T t ( = T c). We can first inject this value directly into A (T t) and get 0 + (c -> c) of type A(T t). Secondly, we can T-lift the A-point injection inRight: c -> 0 + c into (c ->c) -> (c -> 0 + c), which is of type T(A t). We can then use the "sequence" transformation and get 1 + 0 of type A(T t). But this is not the same as what we get when we injected directly into A (T t).

Generally, we can expect that non-polynomial functors are non-traversable, since even the simplest functor c -> t is already not traversable.

For instance, the Future functor is analogous in its features to the non-polynomial functor F t = (t -> 0) -> 0 (the "double negation" functor). So, the Future functor is applicative and monadic, but not traversalble. Again setting A t = 1 + t, it is easy to see that we cannot convert a Future (1 + t) into 1 + Future t. In order to have a value of type 1 + Future t, we need to know at the present time whether we have 1 + 0 or 0 + Future t. However, we are only given a Future (1+t), so we will only know later whether we have the left or the right variant of 1+t.

Let us now consider recursive polynomial functors. These are functors F defined by a fixpoint type equation

F t = G(t, F t),

where G is a polynomial bi-functor. We use the boldface F for the functor that is defined via the inductive assumption.

It is easy to see that polynomial bi-functors are "bi-traversable" in the sense that there exists a natural transformation

G (A t, A x) ~> A(G(t, x)) 

for any applicative functor A. This can be proved by induction, similarly to the proof of Statement 1. A corollary is

Statement 2. All recursive polynomial functors are traversable.

Proof. We need to construct a natural transformation F (A t) ~> A (F t). This is the same as

G(A t, F(A t)) ~> A(G(t, F t)),

where, by the inductive assumption, the "F" in this expression already satisfies the property we are looking for. In other words, we already have a natural transformation F (A t) ~> A (F t). Therefore, we have 

G(A t, F(A t)) ~> G(A t, A(F t)) ~> A(G(t, F t) = A(F t).

Q.E.D.

Traversability seems to be related to the useful "transformability" property of monads: it seems that most polynomial monadic functors have explicit monad transformers. Perhaps, we can show that all polynomial monads have explicit transformers? This is to be investigated in a later installment of this series. (To be continued.)