Functions

In ZFC set theory we have sets, which have elements. If \(X\) and \(Y\) are sets then a function \(f:X\to Y\) is a rule which takes as input an element \(x\) of \(X\) and spits out an element \(f(x)\) of \(Y\).

The analogous notation in dependent type theory is pretty much the same, but with types and terms rather than sets and elements. If X and Y are types, then a function f : X → Y is a rule which takes as input a term a of type X (which can be written a : X) and returns a term f a : Y. Note that we don’t need the brackets in dependent type theory for basic evaluation of a function. Just as in mathematics, the “rule” defining a function could be an algorithm, or it could be non-constructive.

Let’s take a look at a definition of a function from ℕ to ℕ which sends a to a+7.

definition f : ℕ → ℕ := λ a, a + 7
#eval f 2 -- lean prints 9

The colon after the f in type theory indicates that the thing on the left has type the thing on the right, so here f : ℕ → ℕ indicates that f is a term whose type is the function type ℕ → ℕ, which is type theory’s way of expressing that \(f\) is a function from \(\mathbb{N}\) to \(\mathbb{N}\). The λ is the type theory way of writing \(\mapsto\). A mathematician might write that \(f\) is defined as \(x\mapsto x+7\); type theory’s λ (written before the x and with a comma after) means the same thing.

An alternative to the λ notation is to move the input variables to the left of the colon like this:

definition f (a : ℕ) : ℕ := a + 7
#eval f 2 -- lean prints 9

This is not any different to the λ approach – Lean’s parser turns the second definition into the first. Lean knows that if a is a natural then a+7 is too, so this function can even be written

definition f (a : ℕ) := a + 7
#eval f 2 -- lean prints 9

Functions can of course go from one type to a different one. For example bool is a type with two terms, tt (true) and ff (false), and we could define a function from bool to nat sending everything to 59:

definition f : bool → ℕ := λ b, 59

or

definition f (b : bool) : ℕ := 59

But how do we define a function which sends tt to 59 and ff to 79? The easiest way is via “pattern matching”. Because bool is an inductive type, and tt and ff are the two constructors, to define a function on bool we just need to say where each of the constructors should be sent.

definition g : bool → ℕ
| tt := 59
| ff := 79
#eval g tt
-- Lean prints 59

Note that there’s no := on the first line. Note also that bool → ℕ is a type, and g is a term of that type.

Functions of more than one variable

Functions can take more than one variable as input. For example in mathematics one might consider \(g : \mathbb{N}^2\to\mathbb{N}\) defined by \(g(x,y)=x+3y\). In Lean there is a slightly strange twist when defining this function using lambdas:

definition g : ℕ → (ℕ → ℕ) := λ x y, x + 3 * y

The lambda term looks unsurprising, but what is its type? Rather than introducing the product \(\mathbb{N}^2=\mathbb{N}\times\mathbb{N}\), Lean uses a trick called “currying”; the idea is that if g(x,y)=x+3y then if we give x a value (for example 12) but do not specify y, we are left with the function g(12,y)=12+3y, which is now a function of one variable y only. So g can be thought of as a function which eats a natural number x and then spits out a function \(\mathbb{N}\to\mathbb{N}\) sending y to x+3y. This explains the type of g. Writing out the definition of g thought of this way, using lambda notation, would look like

definition g : ℕ → (ℕ → ℕ) := λ x, (λ y, x + 3 * y)

and the shortened variant λ x y, x + 3 * y means the same thing.

One can move terms to the left of the colon as in the one variable case: both

definition g (x : ℕ) : (ℕ → ℕ) := λ y, x + 3 * y

and

definition g (x : ℕ) (y : ℕ) : ℕ := x + 3 * y

and even

definition g (x y : ℕ) : ℕ := x + 3 * y

work, as does

definition g (x y : ℕ) := x + 3 * y

which now looks very familiar to a mathematician. Again Lean does not to be told the type of g x y – it can guess it because it knows the type of x and of y.

One can also use pattern matching to define g:

definition g : ℕ → ℕ → ℕ
| x y := x + 3 * y

Here we see another strange twist – what is this ℕ → ℕ → ℕ? It is not hard to convince yourself that (A → B) → C and A → (B → C) are different types in general. A term of the first type is a function which eats a function from A to B and spits out a term of type C, and a term of the second type eats a term of type A and spits out a function from B to C.

Exercise (1) : If \(A\) and B are finite types with sizes a and b, then show that the number of functions from A to B is \(b^a\).

  1. Show that if furthermore C has size c, then the type (A → B) → C has size \(c^{(b^a)}\) and the type A → (B → C) has size \((c^b)^a\). Find explicit examples of natural numbers a,b,c such that \(c^{(b^a)}\not=(c^b)^a\).

  2. Conclude that the types (A → B) → C and A → (B → C) cannot in general be identified in any natural way.

    Because \(c^{(b^a)}\not=(c^b)^a\) in general (otherwise known as “exponentiation is not associative”), mathematicians need a convention to determine what c^{b^a} means (exercise: which one did they choose?). Similarly, because (A → B) → C and A → (B → C) are different types, if type theorists decide to write A → B → C they have to decide what it will mean, and they decided to let it mean A → (B → C) because via the “currying” trick above, a term of this type can be regarded as a function A × B → C.

Let us now take a look at how addition is defined on the natural numbers in Lean. The names of basic functions like this follow a convention. The usual notation for the natural numbers ℕ is just notation; to see what it the notation means one can type #print notation ℕ and see that the actual type is called nat. Addition on nat will hence be called nat.add. Typing #check nat.add in Lean will show that it has type ℕ → ℕ → ℕ, which is hopefully not a surprise. Furthermore, left-clicking and then right-clicking on nat.add in VS Code and selecting “peek definition” shows that its definition looks something like

def nat.add : nat → nat → nat
| a  zero     := a
| a  (succ b) := succ (add a b)

This is a definition by pattern matching; our two input variables are ...

Pi types

{} brackets

[] brackets

Show them id.

Show them add.

How do we prove f(1,1)=6?

Every nat is by definition succ succ zero.