# Natural Number

We can use the `datatype` keyword to define new `datatype`s.
We take natural number as the first `datatype` example.
After the definition, `Nat` is a `Type`.
And we can use `Nat`'s constructors to construct `Nat`.
We define some common natural numbers, and use them to write tests in the following code.
We can use the `recursion` keyword to define functions that operates over `Nat`.
`add` is one of the most basic function, it adds two `Nat`s togather.
Note that,
• We did not recursively call `add(prev)`, but use `almost.prev` to get the result of the recursive call,
• i.e. `almost.prev` is the same as `add(prev)`.
• i.e. `recursive` is like pattern matching, but an extra argument called `almost` is given to the caller, in which we can get the results of recursive calls.
• We often add a `_` prefix for a name taken from pattern matching, but not used in the following code.
• `_prev` is a example of this situation.
Let's write some tests.
Applying a function that takes two arguments to only one argument, will return another function that takes one argument.
This is called currying.
We often use `same_as_chart` to write test.
By using `recursion`, we are defining function using recursive combinator.
If we view `recursion` over `Nat` as a function, it roughly has the following definition.
The `induction` keyword is like `recursion`, but the return type can depend on the `target`, we use a function to specify the return type, and we call this function `motive`.
If we view `induction` over `Nat` as a function, it roughly has the following definition.
After understood the definition of `add`, we naturally want to define `mul`.
Let write some tests, we use `{ ...; return ... }` to make the name `twelve` only visible inside the following `{ ... }`.
Next we define power function.
`power_of(x, y)` means `y` raised to the power of `x`.
We swap the argument to get a more natural reading of the function.
`power(base, n)` means `base` raised to the power of `n`.
• We define `power_of` first, because its definition is similar to that of `add` and `mul`.
Some tests.
In primary school after the young Gauss misbehaved, his teacher gave him a task: adding the numbers from 1 to 100.
`gauss(x)` calculates `0 + 1 + 2 + ... + x`,
• Thanks, Carl Friedrich Gauss (1777 - 1855), you are the prince of mathematics!
`factorial(n)` calculates `n!`.
For example, `5! = 5 * 4 * 3 * 2 * 1 = 120`.
Let's end this chapter with this famous function.
Actually, before we end this chapter, let's define another very famous function -- the Fibonacci function.
``````F(0) = 0
F(1) = 1
F(n) = F(n-1) + F(n-2)
``````
012345678910
011235813213455
We use an iterative process for computing the Fibonacci numbers. The idea is to use a pair of integers `current` and `next`, initialized `F(0) = 1` and `F(0) = 0`, and to repeatedly apply the simultaneous transformations:
``````current <- next
next <- current + next
``````
First, we define a helper function -- `fibonacci_iter`, for the iterative process.
Then we can define the `fibonacci` using `fibonacci_iter`.