Editing System F (section)

==System F structures==

System F allows recursive constructions to be embedded in a natural manner, related to that in [[Martin-Löf's type theory]]. Abstract structures ({{mvar|S}}) are created using ''constructors''. These are functions typed as:
:<math>K_1\rightarrow K_2\rightarrow\dots\rightarrow S</math>.

Recursivity is manifested when {{mvar|S}} itself appears within one of the types <math>K_i</math>. If you have {{mvar|m}} of these constructors, you can define the type of {{mvar|S}} as:
:<math>\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha</math>

For instance, the natural numbers can be defined as an inductive datatype {{mvar|N}} with constructors
: <math>\begin{align}
\mathit{zero} &: \mathrm{N}\\
\mathit{succ} &: \mathrm{N} \rightarrow \mathrm{N}
\end{align}</math>
The System F type corresponding to this structure is
<math>\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha</math>.  The terms of this type comprise a typed version of the [[Church numeral]]s, the first few of which are:
: <math>\begin{align}
0 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x\\
1 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x\\
2 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)\\
3 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))
\end{align}</math>

If we reverse the order of the curried arguments (''i.e.,'' <math>\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha</math>), then the Church numeral for {{mvar|n}} is a function that takes a function {{mvar|f}} as argument and returns the {{mvar|n}}<sup>th</sup> power of {{mvar|f}}. That is to say, a Church numeral is a [[higher-order function]] – it takes a single-argument function {{mvar|f}}, and returns another single-argument function.