# Datatypes and Patterns

Structures enable multiple independent pieces of data to be combined into a coherent whole that is represented by a brand new type.
Types such as structures that group together a collection of values are called *product types*.
Many domain concepts, however, can't be naturally represented as structures.
For instance, an application might need to track user permissions, where some users are document owners, some may edit documents, and others may only read them.
A calculator has a number of binary operators, such as addition, subtraction, and multiplication.
Structures do not provide an easy way to encode multiple choices.

Similarly, while a structure is an excellent way to keep track of a fixed set of fields, many applications require data that may contain an arbitrary number of elements. Most classic data structures, such as trees and lists, have a recursive structure, where the tail of a list is itself a list, or where the left and right branches of a binary tree are themselves binary trees. In the aforementioned calculator, the structure of expressions themselves is recursive. The summands in an addition expression may themselves be multiplication expressions, for instance.

Datatypes that allow choices are called *sum types* and datatypes that can include instances of themselves are called *recursive datatypes*.
Recursive sum types are called *inductive datatypes*, because mathematical induction may be used to prove statements about them.
When programming, inductive datatypes are consumed through pattern matching and recursive functions.

Many of the built-in types are actually inductive datatypes in the standard library.
For instance, `Bool`

is an inductive datatype:

```
inductive Bool where
| false : Bool
| true : Bool
```

This definition has two main parts.
The first line provides the name of the new type (`Bool`

), while the remaining lines each describe a constructor.
As with constructors of structures, constructors of inductive datatypes are mere inert receivers of and containers for other data, rather than places to insert arbitrary initialization and validation code.
Unlike structures, inductive datatypes may have multiple constructors.
Here, there are two constructors, `true`

and `false`

, and neither takes any arguments.
Just as a structure declaration places its names in a namespace named after the declared type, an inductive datatype places the names of its constructors in a namespace.
In the Lean standard library, `true`

and `false`

are re-exported from this namespace so that they can be written alone, rather than as `Bool.true`

and `Bool.false`

, respectively.

From a data modeling perspective, inductive datatypes are used in many of the same contexts where a sealed abstract class might be used in other languages.
In languages like C# or Java, one might write a similar definition of `Bool`

:

```
abstract class Bool {}
class True : Bool {}
class False : Bool {}
```

However, the specifics of these representations are fairly different. In particular, each non-abstract class creates both a new type and new ways of allocating data. In the object-oriented example, `True`

and `False`

are both types that are more specific than `Bool`

, while the Lean definition introduces only the new type `Bool`

.

The type `Nat`

of non-negative integers is an inductive datatype:

```
inductive Nat where
| zero : Nat
| succ (n : Nat) : Nat
```

Here, `zero`

represents 0, while `succ`

represents the successor of some other number.
The `Nat`

mentioned in `succ`

's declaration is the very type `Nat`

that is in the process of being defined.
*Successor* means "one greater than", so the successor of five is six and the successor of 32,185 is 32,186.
Using this definition, `4`

is represented as `Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))`

.
This definition is almost like the definition of `Bool`

with slightly different names.
The only real difference is that `succ`

is followed by `(n : Nat)`

, which specifies that the constructor `succ`

takes an argument of type `Nat`

which happens to be named `n`

.
The names `zero`

and `succ`

are in a namespace named after their type, so they must be referred to as `Nat.zero`

and `Nat.succ`

, respectively.

Argument names, such as `n`

, may occur in Lean's error messages and in feedback provided when writing mathematical proofs.
Lean also has an optional syntax for providing arguments by name.
Generally, however, the choice of argument name is less important than the choice of a structure field name, as it does not form as large a part of the API.

In C# or Java, `Nat`

could be defined as follows:

```
abstract class Nat {}
class Zero : Nat {}
class Succ : Nat {
public Nat n;
public Succ(Nat pred) {
n = pred;
}
}
```

Just as in the `Bool`

example above, this defines more types than the Lean equivalent.
Additionally, this example highlights how Lean datatype constructors are much more like subclasses of an abstract class than they are like constructors in C# or Java, as the constructor shown here contains initialization code to be executed.

Sum types are also similar to using a string tag to encode discriminated unions in TypeScript.
In TypeScript, `Nat`

could be defined as follows:

```
interface Zero {
tag: "zero";
}
interface Succ {
tag: "succ";
predecessor: Nat;
}
type Nat = Zero | Succ;
```

Just like C# and Java, this encoding ends up with more types than in Lean, because `Zero`

and `Succ`

are each a type on their own.
It also illustrates that Lean constructors correspond to objects in JavaScript or TypeScript that include a tag that identifies the contents.

## Pattern Matching

In many languages, these kinds of data are consumed by first using an instance-of operator to check which subclass has been received and then reading the values of the fields that are available in the given subclass.
The instance-of check determines which code to run, ensuring that the data needed by this code is available, while the fields themselves provide the data.
In Lean, both of these purposes are simultaneously served by *pattern matching*.

An example of a function that uses pattern matching is `isZero`

, which is a function that returns `true`

when its argument is `Nat.zero`

, or false otherwise.

```
def isZero (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => false
```

The `match`

expression is provided the function's argument `n`

for destructuring.
If `n`

was constructed by `Nat.zero`

, then the first branch of the pattern match is taken, and the result is `true`

.
If `n`

was constructed by `Nat.succ`

, then the second branch is taken, and the result is `false`

.

Step-by-step, evaluation of `isZero Nat.zero`

proceeds as follows:

```
isZero Nat.zero
===>
match Nat.zero with
| Nat.zero => true
| Nat.succ k => false
===>
true
```

Evaluation of `isZero 5`

proceeds similarly:

```
isZero 5
===>
isZero (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))))
===>
match Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero)))) with
| Nat.zero => true
| Nat.succ k => false
===>
false
```

The `k`

in the second branch of the pattern in `isZero`

is not decorative.
It makes the `Nat`

that is the argument to `succ`

visible, with the provided name.
That smaller number can then be used to compute the final result of the expression.

Just as the successor of some number \( n \) is one greater than \( n \) (that is, \( n + 1\)), the predecessor of a number is one less than it.
If `pred`

is a function that finds the predecessor of a `Nat`

, then it should be the case that the following examples find the expected result:

```
#eval pred 5
```

```
4
```

```
#eval pred 839
```

```
838
```

Because `Nat`

cannot represent negative numbers, `0`

is a bit of a conundrum.
Usually, when working with `Nat`

, operators that would ordinarily produce a negative number are redefined to produce `0`

itself:

```
#eval pred 0
```

```
0
```

To find the predecessor of a `Nat`

, the first step is to check which constructor was used to create it.
If it was `Nat.zero`

, then the result is `Nat.zero`

.
If it was `Nat.succ`

, then the name `k`

is used to refer to the `Nat`

underneath it.
And this `Nat`

is the desired predecessor, so the result of the `Nat.succ`

branch is `k`

.

```
def pred (n : Nat) : Nat :=
match n with
| Nat.zero => Nat.zero
| Nat.succ k => k
```

Applying this function to `5`

yields the following steps:

```
pred 5
===>
pred (Nat.succ 4)
===>
match Nat.succ 4 with
| Nat.zero => Nat.zero
| Nat.succ k => k
===>
4
```

Pattern matching can be used with structures as well as with sum types.
For instance, a function that extracts the third dimension from a `Point3D`

can be written as follows:

```
def depth (p : Point3D) : Float :=
match p with
| { x:= h, y := w, z := d } => d
```

In this case, it would have been much simpler to just use the `z`

accessor, but structure patterns are occasionally the simplest way to write a function.

## Recursive Functions

Definitions that refer to the name being defined are called *recursive definitions*.
Inductive datatypes are allowed to be recursive; indeed, `Nat`

is an example of such a datatype because `succ`

demands another `Nat`

.
Recursive datatypes can represent arbitrarily large data, limited only by technical factors like available memory.
Just as it would be impossible to write down one constructor for each natural number in the datatype definition, it is also impossible to write down a pattern match case for each possibility.

Recursive datatypes are nicely complemented by recursive functions.
A simple recursive function over `Nat`

checks whether its argument is even.
In this case, `zero`

is even.
Non-recursive branches of the code like this one are called *base cases*.
The successor of an odd number is even, and the successor of an even number is odd.
This means that a number built with `succ`

is even if and only if its argument is not even.

```
def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
```

This pattern of thought is typical for writing recursive functions on `Nat`

.
First, identify what to do for `zero`

.
Then, determine how to transform a result for an arbitrary `Nat`

into a result for its successor, and apply this transformation to the result of the recursive call.
This pattern is called *structural recursion*.

Unlike many languages, Lean ensures by default that every recursive function will eventually reach a base case.
From a programming perspective, this rules out accidental infinite loops.
But this feature is especially important when proving theorems, where infinite loops cause major difficulties.
A consequence of this is that Lean will not accept a version of `even`

that attempts to invoke itself recursively on the original number:

```
def evenLoops (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (evenLoops n)
```

The important part of the error message is that Lean could not determine that the recursive function always reaches a base case (because it doesn't).

```
fail to show termination for
evenLoops
with errors
structural recursion cannot be used
well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments
```

Even though addition takes two arguments, only one of them needs to be inspected. To add zero to a number \( n \), just return \( n \). To add the successor of \( k \) to \( n \), take the successor of the result of adding \( k \) to \( n \).

```
def plus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k' => Nat.succ (plus n k')
```

In the definition of `plus`

, the name `k'`

is chosen to indicate that it is connected to, but not identical with, the argument `k`

.
For instance, walking through the evaluation of `plus 3 2`

yields the following steps:

```
plus 3 2
===>
plus 3 (Nat.succ (Nat.succ Nat.zero))
===>
match Nat.succ (Nat.succ Nat.zero) with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')
===>
Nat.succ (plus 3 (Nat.succ Nat.zero))
===>
Nat.succ (match Nat.succ Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k'))
===>
Nat.succ (Nat.succ (plus 3 Nat.zero))
===>
Nat.succ (Nat.succ (match Nat.zero with
| Nat.zero => 3
| Nat.succ k' => Nat.succ (plus 3 k')))
===>
Nat.succ (Nat.succ 3)
===>
5
```

One way to think about addition is that \( n + k \) applies `Nat.succ`

\( k \) times to \( n \).
Similarly, multiplication \( n × k \) adds \( n \) to itself \( k \) times and subtraction \( n - k \) takes \( n \)'s predecessor \( k \) times.

```
def times (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => Nat.zero
| Nat.succ k' => plus n (times n k')
def minus (n : Nat) (k : Nat) : Nat :=
match k with
| Nat.zero => n
| Nat.succ k' => pred (minus n k')
```

Not every function can be easily written using structural recursion.
The understanding of addition as iterated `Nat.succ`

, multiplication as iterated addition, and subtraction as iterated predecessor suggests an implementation of division as iterated subtraction.
In this case, if the numerator is less than the divisor, the result is zero.
Otherwise, the result is the successor of dividing the numerator minus the divisor by the divisor.

```
def div (n : Nat) (k : Nat) : Nat :=
if n < k then
0
else Nat.succ (div (n - k) k)
```

As long as the second argument is not `0`

, this program terminates, as it always makes progress towards the base case.
However, it is not structurally recursive, because it doesn't follow the pattern of finding a result for zero and transforming a result for a smaller `Nat`

into a result for its successor.
In particular, the recursive invocation of the function is applied to the result of another function call, rather than to an input constructor's argument.
Thus, Lean rejects it with the following message:

```
fail to show termination for
div
with errors
argument #1 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k
argument #2 was not used for structural recursion
failed to eliminate recursive application
div (n - k) k
structural recursion cannot be used
failed to prove termination, use `termination_by` to specify a well-founded relation
```

This message means that `div`

requires a manual proof of termination.
This topic is explored in the final chapter.