Functions ========= In ZFC set theory we have sets, which have elements. If :math:`X` and :math:`Y` are sets then a *function* :math:`f:X\to Y` is a rule which takes as input an element :math:`x` of :math:`X` and spits out an element :math:`f(x)` of :math:`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``. .. code-block:: lean 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 :math:`f` is a function from :math:`\mathbb{N}` to :math:`\mathbb{N}`. The ``λ`` is the type theory way of writing :math:`\mapsto`. A mathematician might write that :math:`f` is defined as :math:`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: .. code-block:: lean 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 .. code-block:: lean 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``: .. code-block:: lean definition f : bool → ℕ := λ b, 59 or .. code-block:: lean 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. .. code-block:: lean 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 :math:`g : \mathbb{N}^2\to\mathbb{N}` defined by :math:`g(x,y)=x+3y`. In Lean there is a slightly strange twist when defining this function using lambdas: .. code-block:: lean definition g : ℕ → (ℕ → ℕ) := λ x y, x + 3 * y The lambda term looks unsurprising, but what is its type? Rather than introducing the product :math:`\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 :math:`\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 .. code-block:: lean 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 .. code-block:: lean definition g (x : ℕ) : (ℕ → ℕ) := λ y, x + 3 * y and .. code-block:: lean definition g (x : ℕ) (y : ℕ) : ℕ := x + 3 * y and even .. code-block:: lean definition g (x y : ℕ) : ℕ := x + 3 * y work, as does .. code-block:: lean 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``: .. code-block:: lean 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 :math:`A` and `B` are finite types with sizes `a` and `b`, then show that the number of functions from `A` to `B` is :math:`b^a`. (2) Show that if furthermore `C` has size `c`, then the type ``(A → B) → C`` has size :math:`c^{(b^a)}` and the type ``A → (B → C)`` has size :math:`(c^b)^a`. Find explicit examples of natural numbers `a,b,c` such that :math:`c^{(b^a)}\not=(c^b)^a`. (3) Conclude that the types ``(A → B) → C`` and ``A → (B → C)`` cannot in general be identified in any natural way. Because :math:`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 .. code-block:: lean 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.