# Computer Science

\(\newcommand{\R}{\mathbb{R}}\) \(\newcommand{\RR}{\mathbb{R}}\) \(\newcommand{\C}{\mathbb{C}}\) \(\newcommand{\Z}{\mathbb{Z}}\)

\(\newcommand{\N}{\mathbb{N}}\)

## Types¶

Every mathematical object has a type[^1]. For instance, the integer \(5\) has type \(\Z\), and the function \(x \mapsto x + 4\) has type \(\Z \to \Z\) (or perhaps \((\R \to \R)\) depending on how we interpret \(4\)).

[^1: There are other ways of looking at things, but this kind of statement is fine at the level of detail we're concerned with.]

The pair \((4,5)\) has type \((\Z, \Z)\), while the pair \(((x \mapsto x + 4), 5)\) has type \(((\Z \to \Z), \Z)\).

Conventionally, we write \(4 : \Z\) to mean \(4\) is an object with type \(\Z\).

It is often very convenient to clarify the types of a function by writing e.g. \(\phi(x : A) : B\), which should be understood to mean: \(\phi\) is a function evaluated at \(x\) of type \(A\), and returns a value \(\phi(x)\) of type \(B\). From this we infer that \(\phi\) has type \(A \to B\).

## Quantifiers¶

The function \(x \mapsto x\) really has type \((\forall a, (a \to a))\), in other words, for any *type* a, take a value of that type and return it.

## Higher order functions¶

The function \(f(x)=x^2\) has type \(\mathbb{R} \to \mathbb{R}\); it takes a number as argument. However, there are situations where we are interested in functions which take functions are arguments, or return functions as output.

For example, the function \(map\) takes a function \(f\) and a list \(l\), and applies \(f\) to each element of the list. So \(map : \forall a, b: (a \to b) \to List(a) \to List(b)\), where if \(C\) is a type, \(List(C)\) is the type whose values are lists whose elements all have type \(C\).

### Currying¶

A function can also return a function, for instance \(f := x \mapsto (y \mapsto y + x)\) is a function which takes a number and returns a function which takes a second number and adds the first number to it. So \(f(4)\) is an "add 4" function, so that \((f(4))(5)=9\). It has type \(f : \Z \to (\Z \to \Z)\).

When we write \(f(4)\), we say that we have "partially applied" \(f\) to \(4\).

We could also define a function \(g := (x,y) \mapsto x+y : (\Z, \Z) \to \Z\).

\(f\) and \(g\) are isomorphic (in the category SET) and the functions mapping from \(f\) to \(g\) and back are known as uncurrying and currying respectively.