Natural Transformation in a Programming Language? I'm trying to solve some exercises about category theory, more specifically covering functors, natural transformations and monads. I'm stuck at one that goes as follows:
Ex.: Suppose you have a Programming Language P, and the category $P^C$: the category where objects are types of P and morphisms functions between these types. Now, consider the Functor $List: P^C \to P^C$, that maps a type $A$ to the lists of type $A$ ($List\ A$). Also, consider the identity functor $Id_{P^C}: P^C \to P^C$.
Question: Is it possible to define a natural transformation $\theta: List \to id_{P^C}$ ?
As far as I understand, the commutative diagram for that transformation is given by the one below:
$$
\newcommand{\ra}[1]{\!\!\!\!\!\!\!\!\!\!\!\!\xrightarrow{\quad#1\quad}\!\!\!\!\!\!\!\!}
\newcommand{\da}[1]{\left\downarrow{\scriptstyle#1}\vphantom{\displaystyle\int_0^1}\right.}
%
\begin{array}{lll}
List\ A\ & \ra{\theta_A} & A \\
\da{fmap\ f} & & \da{f} \\
List\ B\ & \ra{\theta_B} & B \\
\end{array}
$$
Now, if I take type $A$ to be Integers, and type $B$ to be Booleans, I could define a function $f$ "isEven" that, given an integer $n$, returns "true" if $n$ is even, and "false" otherwise. Applying that through $fmap\ f$ would give me a $List Boolean$. Applying the natural transformation $head$, that takes the first element of a $List$ would make the diagram commute for the given example, if the list is not empty. But if it is empty, the diagram wouldn't commute, right?
Moreover, would it be a valid natural transformation? 
Could you give me any help in finding a valid one?
 A: There is no natural transformation $\theta\colon \mathrm{List}\to \mathrm{id}_{P^C}$. As suggested by the diagram in your question, the reason comes down to empty lists. For every type $A$, we need a component of the natural transformation $\theta_A\colon \mathrm{List}(A)\to A$, and in particular $\theta_A$ needs to map the empty list to some element of $A$.
If your programming language includes an empty type $\emptyset$, then we're already sunk: the type $\mathrm{List}(\emptyset)$ is nonempty, since it includes the empty list, but there can be no function from a nonempty type to an empty type (there's no possible value of $\theta_\emptyset(\{\})$.
But even if your programming language doesn't include an empty type, there's still an issue with "naturally" picking an element $\theta_A(\{\})$ of every type $A$. Indeed, consider the type $\mathrm{Bool}$ and the "not" function $\lnot\colon \mathrm{Bool}\to \mathrm{Bool}$ defined by $\lnot(\top) = \bot$ and $\lnot(\bot) = \top$. We want the following diagram to commute:
$$
\newcommand{\ra}[1]{\!\!\!\!\!\!\!\!\!\!\!\!\xrightarrow{\quad#1\quad}\!\!\!\!\!\!\!\!}
\newcommand{\da}[1]{\left\downarrow{\scriptstyle#1}\vphantom{\displaystyle\int_0^1}\right.}
%
\begin{array}{lll}
\mathrm{List}(\mathrm{Bool}) & \ra{\theta_\mathrm{Bool}} & \mathrm{Bool} \\
\da{\mathrm{map}(\lnot)} & & \da{\lnot} \\
\mathrm{List}(\mathrm{Bool}) & \ra{\theta_\mathrm{Bool}} & \mathrm{Bool} \\
\end{array}
$$
But $(\mathrm{map}(\lnot))(\{\}) = \{\}$, so commutativity of the diagram says that $$ \lnot\theta_{\mathrm{Bool}}(\{\}) = \theta_\mathrm{Bool}((\mathrm{map}(\lnot))(\{\})) = \theta_\mathrm{Bool}(\{\}),$$
i.e. $\top = \bot$, which is a contradiction.
I used $\mathrm{Bool}$ here for simplicity. But actually the same argument works as long as you have any type $A$ in your language such that for every $a\in A$ there is some function $f\colon A\to A$ such that $f(a) \neq a$. If your programming language allows for constant functions, then all you need is to have a type with at least $2$ elements in it, since for every $a\in A$ you can use the function $f(x) = b$ for some $b\neq a$.
A: Consider Vecₙ to be the type of lists/vectors of length n.
Let _‼ₙ_ be the indexing operation on Vecₙ; that is, if
xs : Vecₙ A is a vector of n elements of type A and
i ≤ n, then xs ‼ₙ i is an element of A, namely the i-th component of
the vector.
Observe that for any pair i, n with i ≤ n, we have a natural transformation
(‼ₙ i) : Vecₙ ⟶ Id

Indeed, for let f : A → B be any old plain
function, then the commutativity condition amounts to 
map f xs ‼ₙ i = f (xs ‼ₙ i)

i.e., transforming all elements by f then getting the i-th element is the same
as getting the i-th element and transforming it by f.
We avoided having to worry about non-empty lists or having default values
---which means we can only consider functions that "preserve" default values---
by using dependent types. That is, for any n, we have a type-former Vecₙ.
Yet, Vec itself can be construed as a "dependent type" since it depends on
a value, not a type, n. Dependently-typed programming languages are gaining popularity; Agda for example.
