$$\DeclareMathOperator{\prj}{prj}$$ $$\DeclareMathOperator{\aprj}{aprj}$$ $$\DeclareMathOperator{\tprj}{tprj}$$ $$\DeclareMathOperator{\gprj}{gprj}$$

# 6.1 Arrays

An array $$A$$ of length $$n$$ is just a tuple of $$n$$ components of the same type $$T$$: $A = T^n = \underbrace{T \times T \times T \times \ldots \times T}_\text{n times}$ A special property of arrays is that all the projection functions have the same type: $A\rightarrow T$ This means we can have a generalised projection function called an array projection instead: $\aprj_A : {\Bbb Z}_n \rightarrow (A \rightarrow T)$ where $i \mapsto \prj_{A,i}$

However, even more general is a generalised tuple projection shown here for a pair: $\tprj_{T_0\times T_1} : {\Bbb Z}_2 \rightarrow (T_0 \times T_1 \rightarrow T_0 + T_1)$ which suggests a more general form for an individual projection: $\gprj_{T_0\times T_1,i}:T_0 \times T_1 \rightarrow T_0 + T_1$ for $$i \in \lbrace 0,1\rbrace$$. In simple terms, the generalised projection returns the tuple index along with the value.

We also have the codiagonal function. For a sum: $S = \underbrace{T + T + T + \ldots + T}_\text{n times}$

$\nabla_S : S \rightarrow T$ which simply forgets the case index.