Natural Transformation in a Programming Language?

Question

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?

Answer 1

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$.

Answer 2

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.