If a type is an object and a function is a morphism. How to interpret a value in programming?

Question

I've been reading Bartoz's "Category Theory for Programmers", and one question came to mind. In programming, types are objects and functions are morphisms. A functor is then a way to construct types from other types (e.g. $F(Int) = String$) together with an $fmap$ which is just a function that takes a function $f:A\to B$ and an element of $FA$ and returns $FB$, i.e. $fmap(f,\_) = Ff$.

Good enough. Now, the thing is, the examples of how to create a functor usually are something like this:

struct F{T}
  x::T
  y::T
end
F(T::Type) = F{T}

fmap(f::Function, A::F{T}) = F(f(A.x),f(A.y))
F(f) = A->fmap(f,A)

This code above is Julia, but it's fairly easy to understand. The struct F{T} is describing a new parametric type that contains two values of type T. For example, one can think of F{Int} as a Tuple{Int,Int}, meaning, a tuple of two integers.

Now, in the code above, I haven't defined how to generate "values" of type F{T}. This is actually done implicitly by Julia. Meaning, if I write F(1,2), Julia will return a value of type F{int}.

My question is what is this "value" constructor for types F{T}. My guess is that this is a natural transformation... Is that right? And if so, is it a natural transformation between which functors?

Answer 1

$\require{AMScd}$ $\DeclareMathOperator\apply{apply}$ $\DeclareMathOperator\fmap{fmap}$ $\DeclareMathOperator\Tuple{Tuple}$

The fields x and y of the struct can be interpreted as functions x :: F{T} -> T and y :: F{T} -> T. These function symbols witness that $F T$ is isomorphic in the category $\text{Types}$ of types to the product $T \times T$, with projections $x$ and $y$.

In general a struct $F\{T_1,\ldots,T_m\}$ with fields $a_1,\ldots,a_n$, where $a_i: F\{T_1,\ldots,T_m\} \to T_i$ witnesses the type $F\{T_1,\ldots,T_m\}$ as the product $T_1 \times \ldots \times T_n$ (where we may have repeated objects in this product). The value constructor is the inverse of this isomorphism: $F: T_1 \times \ldots \times T_n \to F\{T_1, \ldots, T_m\}$.

Since the $T_i$ are type variables, we could think of $T_1 \times \ldots \times T_n$ as a functor $\Tuple: \text{Types} \times \ldots \times \text{Types} \to \text{Types}$. Then the value constructor looks like the component of a natural transformation $F: \Tuple\{-\} \Rightarrow F\{-\}$. For the struct in your question, this is indeed a natural transformation because the definition of fmap is evaluated "pointwise". However, this is not generally true, even in the 1-ary case, explained below.

Given a 1-ary functor $F: \text{Types} \to \text{Types}$, the constructor is a function $F^{new}_T: T \to F\{T\}$, but in programming languages (like Haskell, and apparently Julia), the notation is simplified, yielding what we typically see for a constructor:

F :: T -> F{T}
-- Or even:
pure :: T -> F T

This looks like the component of a natural transformation $F^{new}: \text{id} \Rightarrow F$ (where $\text{id}: \text{Types} \to \text{Types}$ is the identity functor), but the statement that $F^{new}$ is natural is the statement that the following diagram commutes for any choice of function $f: A \to B$ in the category of $\text{Types}$: $$ \begin{CD} A @>{f}>> B\\ @V{F^{new}_A}VV @VV{F^{new}_B}V\\ F\{A\} @>{\text{fmap}(f)}>> F\{B\} \end{CD} $$ Commutativity of this diagram is the following identity, for any term x :: A.

fmap(f,F(x)) == F(fmap(f,x))

Not all functors satisfy this identity. However, if $F$ does satisfy this identity for any type—in a compatible way—then we say (at least in Haskell) that $F$ is an applicative (functor).

An applicative is a triplet $(F,F^{new},\apply)$ where $F$ is a functor, $F^{new}$ is the constructor, and $\apply: F(Y^X) \to FY^{FX}$ is a collection of arrows, where $Y^X$ is the type of functions $f : X \to Y$. This triplet has to satisfy compatibility conditions, for any terms x :: X, y :: F{X}:

0. $\fmap(f, y) = \apply(F^{new}(f),y)$
1. $\fmap(1_X,y) = y$.
2. $\fmap(f, F^{new}(x)) = F^{new}(f(x))$
3. Compatible with Currying (there is an equation for this)
4. Compatible with function composition (there is an equation for this)

In particular, condition (2) is the statement that $F^{new} : \text{id} \Rightarrow F$ is a natural transformation.

In pure mathematical terminology: the category $\text{Types}$ in a programming language is (modulo side-effects) a Cartesian-Closed category. A functor class in the language corresponds to an endofunctor $F : \text{Types} \to \text{Types}$. If this functor is a strong lax monoidal functor, then $F$ can be given the structure of an applicative functor (c.f. Haskell).