# The three kinds of types

This is some background on Lean’s type theory.

## Introduction

Recall that every expression in Lean lives at one of three “levels” – it is either a universe, a type or a term. The universes are easy to understand; as far as this course is concerned, there are only two, namely `Type` and `Prop`. This document is about the next level down – types. It turns out that at the end of the day there are only three kinds of ways that you can make types; there are function types, inductive types and quotient types. I will go through these three kinds of types in this section, explaining abstractly how to make the type, how to make terms of that type, and how to make functions whose domain is the type.

[A technical footnote about the “meaning” of this section. You might be wondering about the sets and theorem statements you know in mathematics (recall that in Lean the type plays the role of both), and asking yourself which kind of type each of these things is. However such a question is not really mathematically meaningful; for example the type of group homomorphisms between two groups can be made either as an inductive type or a function type, and the quotient of a group by a subgroup can be made as either an inductive type or a quotient type. In fact, it is not completely clear to me that mathematicians need to know the ins and outs of these constructions if all they want to do is to prove theorems, but here is a brief overview anyway. For more detailed information, read Lean’s type theory bible, Theorem Proving In Lean (sections 2, 3, 7 and 11.4).]

[A technical footnote about universes. if you look in the source code of `mathlib` TODO add web link to github) you will find more general Type universes called `Type u` (our `Type` is just `Type 0`), and you might even see `Sort u`, which means “either `Type u` or `Prop`. These “higher universes” are a consequence of the fact that eveyrthing in Lean has to have a type, so `Type` has to have a type, and this type is called `Type 1`, which has type `Type 2` etc etc. We’re not doing any category theory in this course, so we will ignore these higher universes.]

## Function types (a.k.a. Pi types)

Set-theoretically, if `X` and `Y` are sets, we can consider the set `Hom(X,Y)` of maps from `X` to `Y`. In Lean the corresponding type is called `X → Y` so you can think of the `→` symbol as “the way to make this type”.

We make terms of this type using something called `λ`. In maths it’s quite common for `λ` to denote a real number, but `λ` is a reserved symbol in Lean – it means one thing, and one thing only: it’s the `λ` in “lambda-calculus”, if you’ve ever heard of that. If you want to make the function `f(x)` from the reals to the reals sending `x` to `x^2+3` then in Lean the definition of `f` looks like this:

```def f : ℝ → ℝ := λ x, x^2+3
```

If you have understood the “mapsto” symbol `↦` in mathematics you might have seen this function defined as `x ↦ x^2+3`. Computer scientists use “prefix notation” for this construction rather than “infix notation”, i.e. they put the symbol indicating that we’re making a function before the input and output, instead of between the input and output.

In fact Lean has a slightly more general kind of function type. The idea (expressed set-theoretically) is that if we have infinitely many sets `Y₀`, `Y₁`, `Y₂`,… then we can make the type of functions from the natural numbers to the union of the `Yₙ`, but with the condition that the natural number `i` is sent to an element of `Yᵢ`. More generally (and switching back to type-theoretic language), say `I` is some index type, and for each `i : I` we have a type `Y i`. Then Lean will let you make the type of “generalised functions” which take as input a term `i` of type `I` and which spit out a term of type `Y i` – so the type of the output depends on the term which is input. Lean’s notation for the type of these functions is `Π (i : I), Y i`. If `f` is such a function, then the fact that the type of the output of `f` depends on the term `i` which is input means that `f` is called a “dependent function”, and the type `Π (i : I), Y i` of `f` is called a “dependent type”, or a “Pi type”. Not all theorem provers have dependent types – for example the Isabelle/HOL theorem prover uses a logic called Higher Order Logic, which does not have dependent types.

Dependent types in the `Type` universe started showing up in mathematics in the middle of the 20th century. Those of you who have done some differential geometry might have seen this sort of thing before (if you haven’t then perhaps ignore this paragraph!). The tangent space `Tₓ` of a manifold at a point `x` is a vector space, and these tangent spaces “glue together” to make a tangent bundle, the union of the tangent spaces; a section `s` of the tangent bundle is a function from the manifold to the union of the tangent spaces with the extra hypothesis that `s(x)` is an element of `Tₓ` for all `x`. So a section of the tangent bundle is a term of type `Π (x : X), T x`. They also show up in algebraic geometry when you start doing scheme theory (for example Hartshorne’s definition of the structure sheaf on an affine scheme involves the dependent type of functions sending a prime ideal of a commutative ring to an element of the localisation of the ring at this prime ideal).

If the simplest examples I can come up with in mathematics are some fancy differential geometry and algebraic geometry examples, you might wonder whether we need to think about Pi types at all in this course. But in fact in the `Prop` universe they show up all the time! Let’s consider a proof by induction. We have infinitely many true-false statements `P(0)`, `P(1)`, `P(2)`,…, and we want to prove them all. In other words, we want to prove the proposition `∀ n, P(n)`. This proposition, like all propositions, is a type (in the `Prop` universe) and in fact it is a Pi type, because to give a term of this type, we need to come up with a function which takes as input a natural number `n` and gives as output a proof of `P(n)`, that is, a term of type `P(n)`. So different input terms give terms in different output types. In short, whilst you can do a lot of mathematics without dependent types, we see dependent propositions everywhere. In fact the statement of Fermat’s Last Theorem is a dependent type, because the type `x ^ n + y ^ n = z ^ n` depends on the terms `x`, `y`, `z` and `n`. Of course it’s possible to state Fermat’s Last Theorem in Isabelle/HOL or another HOL system, however the lack of dependent types might make doing modern algebraic geometry in such a system far more inconvenient.

## Inductive types

Inductive types are an extremely flexible kind of type; you make them by basically listing the rules which you will allow to make terms of this type. For example, if you want Lean’s version of “a set `X` with three elements `a`, `b`, and `c`” then you can make it like this:

```inductive X : Type
| a : X
| b : X
| c : X
```

We now have a new type `X` in the system, with three terms `X.a : X`, `X.b : X` and `X.c : X`.

So that’s now to make an inductive type, and how to make terms of this type. The remaining question is how to define functions from this type, or equivalently how to use terms of this type. If you want to make a function from this type, then instead of using `λ` you can use Lean’s “equation compiler”. Here’s how to define the function from `X` to the naturals sending `X.a` to `37`, `X.b` to `42` and `X.c` to 0:

```def f : X → ℕ
| X.a := 37
| X.b := 42
| X.c := 0
```

Note that if you `open X` then you don’t have to keep putting `X.` everywhere.

You might think that this kind of construction can only make finite types, but in fact the theory of inductive types is far more powerful than this, and in particular we can make many infinite types with them. For example the definition of the natural numbers in Lean looks like this:

```inductive nat : Type
| zero : nat
| succ : nat → nat
```

(Peano observed that these two construtions were enough to define all natural numbers) and then we set up the notation `ℕ` for `nat` immediately afterwards. If you’ve played the natural number game you’ll know that we can define addition and multiplication on the natural numbers, and once one has these set up one can define functions from the naturals to the naturals or other types using `λ`, for example `λ (n : ℕ), 2*n+3` defines a function from `ℕ` to `ℕ`. However we can also use the equation compiler to inductively define (or more precisely, recursively define) functions from the naturals. For example the sequence defined by `a(0)=3` and `a(n+1)=a(n)^2+37` could be defined like this:

```def a : ℕ →  ℕ
| nat.zero := 3
| nat.succ n := (a n)^2 + 37
```

You can make inductive propositions too. For example here are the definitions of `true` and `false` in Lean:

```inductive true : Prop
| intro : true

inductive false : Prop
```

The inductive type `true` has one constructor (called `true.intro`); the inductive type `false` has no constructors. Remember that we model truth and falsehood of propositions in Lean by whether the corresponding type has a term or not. Faced with a goal of `⊢ true` you can prove it with `exact true.intro`. You cannot make a term of type `false` “absolutely” – the only time it can happen is if you are in a “relative” situation where you have hypotheses, some of which are contradictory.

If `P` and `Q` are Propositions, then you can use inductive types to make the propositions `and P Q` and `or P Q`, with notations `P ∧ Q` and `P ∨ Q`. Here are their definitions:

```variables (P Q : Prop)

inductive and : Prop
| intro (hp : P) (hq : Q) : and

inductive or : Prop
| intro_left (hP : P) : or
| intro_right (hQ : Q) : or
```

If you do `cases h` with `h : P ∧ Q` then, because `and` has one constructor (`and.intro`), you end up with one goal. If you do `cases h` with `h : P ∨ Q` then you end up with two goals, because `or` has two constructors (`or.intro_left` and `or.intro_right`). If you do `cases h` with `h : false` then you end up with no goals, because `false` has no constructors. When Lean sees that there are no goals left, it prints `Goals accomplished`; if you have no goals left, you’ve proved the result you were trying to prove. It took me some time to recalibrate my thinking to this “inductive” way of thinking about logic.

We say “let `G` be a group” in Lean using inductive types, but the types involved are very simple inductive types with only one constructor. The type `group G` is the type of group structures on `G`. There is only way to make a term of type `group G` – you have to give a multiplication on `G`, an identity and an inverse function, and then check that it satisfies the group axioms. So the inductive type `group G` has just one constructor which takes all of this data as input and then outputs a term of type `group G`. We will talk more about how to make the inductive type `group G` when we get on to groups in section 3 or so.

## Quotient types

The third kind of type which you can make in Lean is a quotient type, which I mention here only for completeness. Lean does not actually need this kind of type – it is possible to make quotient types explicitly using inductive types. However for technical reasons (which mathematicians don’t need to worry about) they are a distinct primitive kind of type in Lean. The basic set-up is that you have a type `X` and an equivalence relation `R` on `X` (for some reason this is referred to as a term of type `setoid X` in Lean), and you want to make the quotient of `X` by `R`. This is the type which mathematicians would typically refer to as “the set of equivalence classes of `R`”. In Lean it’s called `quotient R`, and the map from `X` to `quotient R` is called `quotient.mk : X → quotient R`. In particular you can make terms of type `quotient R` by applying `quotient.mk` to terms of type `X` (this is just the construction sending an element of `X` to its equivalence class). To define a function from `quotient R` we use the `quotient.lift` function; more on this later, when we construct some quotient types familiar to mathematicians.